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

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