Metamath Proof Explorer

Theorem hartogs

Description: The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 and hartogslem2 ) proof can be given using the axiom of choice, see ondomon . As its label indicates, this result is used to justify the definition of the Hartogs function df-har . (Contributed by Jeff Hankins, 22-Oct-2009) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion hartogs 
|- ( A e. V -> { x e. On | x ~<_ A } e. On )

Proof

Step Hyp Ref Expression
1 onelon 
 |-  ( ( z e. On /\ y e. z ) -> y e. On )
2 vex 
 |-  z e. _V
3 onelss 
 |-  ( z e. On -> ( y e. z -> y C_ z ) )
4 3 imp 
 |-  ( ( z e. On /\ y e. z ) -> y C_ z )
5 ssdomg 
 |-  ( z e. _V -> ( y C_ z -> y ~<_ z ) )
6 2 4 5 mpsyl 
 |-  ( ( z e. On /\ y e. z ) -> y ~<_ z )
7 1 6 jca 
 |-  ( ( z e. On /\ y e. z ) -> ( y e. On /\ y ~<_ z ) )
8 domtr 
 |-  ( ( y ~<_ z /\ z ~<_ A ) -> y ~<_ A )
9 8 anim2i 
 |-  ( ( y e. On /\ ( y ~<_ z /\ z ~<_ A ) ) -> ( y e. On /\ y ~<_ A ) )
10 9 anassrs 
 |-  ( ( ( y e. On /\ y ~<_ z ) /\ z ~<_ A ) -> ( y e. On /\ y ~<_ A ) )
11 7 10 sylan 
 |-  ( ( ( z e. On /\ y e. z ) /\ z ~<_ A ) -> ( y e. On /\ y ~<_ A ) )
12 11 exp31 
 |-  ( z e. On -> ( y e. z -> ( z ~<_ A -> ( y e. On /\ y ~<_ A ) ) ) )
13 12 com12 
 |-  ( y e. z -> ( z e. On -> ( z ~<_ A -> ( y e. On /\ y ~<_ A ) ) ) )
14 13 impd 
 |-  ( y e. z -> ( ( z e. On /\ z ~<_ A ) -> ( y e. On /\ y ~<_ A ) ) )
15 breq1 
 |-  ( x = z -> ( x ~<_ A <-> z ~<_ A ) )
16 15 elrab 
 |-  ( z e. { x e. On | x ~<_ A } <-> ( z e. On /\ z ~<_ A ) )
17 breq1 
 |-  ( x = y -> ( x ~<_ A <-> y ~<_ A ) )
18 17 elrab 
 |-  ( y e. { x e. On | x ~<_ A } <-> ( y e. On /\ y ~<_ A ) )
19 14 16 18 3imtr4g 
 |-  ( y e. z -> ( z e. { x e. On | x ~<_ A } -> y e. { x e. On | x ~<_ A } ) )
20 19 imp 
 |-  ( ( y e. z /\ z e. { x e. On | x ~<_ A } ) -> y e. { x e. On | x ~<_ A } )
21 20 gen2 
 |-  A. y A. z ( ( y e. z /\ z e. { x e. On | x ~<_ A } ) -> y e. { x e. On | x ~<_ A } )
22 dftr2 
 |-  ( Tr { x e. On | x ~<_ A } <-> A. y A. z ( ( y e. z /\ z e. { x e. On | x ~<_ A } ) -> y e. { x e. On | x ~<_ A } ) )
23 21 22 mpbir 
 |-  Tr { x e. On | x ~<_ A }
24 ssrab2 
 |-  { x e. On | x ~<_ A } C_ On
25 ordon 
 |-  Ord On
26 trssord 
 |-  ( ( Tr { x e. On | x ~<_ A } /\ { x e. On | x ~<_ A } C_ On /\ Ord On ) -> Ord { x e. On | x ~<_ A } )
27 23 24 25 26 mp3an 
 |-  Ord { x e. On | x ~<_ A }
28 eqid 
 |-  { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
29 eqid 
 |-  { <. s , t >. | E. w e. y E. z e. y ( ( s = ( g ` w ) /\ t = ( g ` z ) ) /\ w _E z ) } = { <. s , t >. | E. w e. y E. z e. y ( ( s = ( g ` w ) /\ t = ( g ` z ) ) /\ w _E z ) }
30 28 29 hartogslem2 
 |-  ( A e. V -> { x e. On | x ~<_ A } e. _V )
31 elong 
 |-  ( { x e. On | x ~<_ A } e. _V -> ( { x e. On | x ~<_ A } e. On <-> Ord { x e. On | x ~<_ A } ) )
32 30 31 syl 
 |-  ( A e. V -> ( { x e. On | x ~<_ A } e. On <-> Ord { x e. On | x ~<_ A } ) )
33 27 32 mpbiri 
 |-  ( A e. V -> { x e. On | x ~<_ A } e. On )