Metamath Proof Explorer

Theorem ondomon

Description: The class of ordinals dominated by a given set is an ordinal. Theorem 56 of Suppes p. 227. This theorem can be proved without the axiom of choice, see hartogs . (Contributed by NM, 7-Nov-2003) (Proof modification is discouraged.) Use hartogs instead. (New usage is discouraged.)

Ref Expression
Assertion ondomon 
|- ( 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 elex 
 |-  ( A e. V -> A e. _V )
29 canth2g 
 |-  ( A e. _V -> A ~< ~P A )
30 domsdomtr 
 |-  ( ( x ~<_ A /\ A ~< ~P A ) -> x ~< ~P A )
31 29 30 sylan2 
 |-  ( ( x ~<_ A /\ A e. _V ) -> x ~< ~P A )
32 31 expcom 
 |-  ( A e. _V -> ( x ~<_ A -> x ~< ~P A ) )
33 32 ralrimivw 
 |-  ( A e. _V -> A. x e. On ( x ~<_ A -> x ~< ~P A ) )
34 28 33 syl 
 |-  ( A e. V -> A. x e. On ( x ~<_ A -> x ~< ~P A ) )
35 ss2rab 
 |-  ( { x e. On | x ~<_ A } C_ { x e. On | x ~< ~P A } <-> A. x e. On ( x ~<_ A -> x ~< ~P A ) )
36 34 35 sylibr 
 |-  ( A e. V -> { x e. On | x ~<_ A } C_ { x e. On | x ~< ~P A } )
37 pwexg 
 |-  ( A e. V -> ~P A e. _V )
38 numth3 
 |-  ( ~P A e. _V -> ~P A e. dom card )
39 cardval2 
 |-  ( ~P A e. dom card -> ( card ` ~P A ) = { x e. On | x ~< ~P A } )
40 37 38 39 3syl 
 |-  ( A e. V -> ( card ` ~P A ) = { x e. On | x ~< ~P A } )
41 fvex 
 |-  ( card ` ~P A ) e. _V
42 40 41 eqeltrrdi 
 |-  ( A e. V -> { x e. On | x ~< ~P A } e. _V )
43 ssexg 
 |-  ( ( { x e. On | x ~<_ A } C_ { x e. On | x ~< ~P A } /\ { x e. On | x ~< ~P A } e. _V ) -> { x e. On | x ~<_ A } e. _V )
44 36 42 43 syl2anc 
 |-  ( A e. V -> { x e. On | x ~<_ A } e. _V )
45 elong 
 |-  ( { x e. On | x ~<_ A } e. _V -> ( { x e. On | x ~<_ A } e. On <-> Ord { x e. On | x ~<_ A } ) )
46 44 45 syl 
 |-  ( A e. V -> ( { x e. On | x ~<_ A } e. On <-> Ord { x e. On | x ~<_ A } ) )
47 27 46 mpbiri 
 |-  ( A e. V -> { x e. On | x ~<_ A } e. On )