This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onintrab

Description: The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion onintrab 
|- ( |^| { x e. On | ph } e. _V <-> |^| { x e. On | ph } e. On )

Proof

Step Hyp Ref Expression
1 intex 
 |-  ( { x e. On | ph } =/= (/) <-> |^| { x e. On | ph } e. _V )
2 ssrab2 
 |-  { x e. On | ph } C_ On
3 oninton 
 |-  ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. On )
4 2 3 mpan 
 |-  ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. On )
5 1 4 sylbir 
 |-  ( |^| { x e. On | ph } e. _V -> |^| { x e. On | ph } e. On )
6 elex 
 |-  ( |^| { x e. On | ph } e. On -> |^| { x e. On | ph } e. _V )
7 5 6 impbii 
 |-  ( |^| { x e. On | ph } e. _V <-> |^| { x e. On | ph } e. On )