Metamath Proof Explorer

Theorem card2on

Description: The alternate definition of the cardinal of a set given in cardval2 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013)

Ref Expression
Assertion card2on 
|- { 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 domsdomtr 
 |-  ( ( 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 hartogs 
 |-  ( A e. _V -> { x e. On | x ~<_ A } e. On )
29 sdomdom 
 |-  ( x ~< A -> x ~<_ A )
30 29 a1i 
 |-  ( x e. On -> ( x ~< A -> x ~<_ A ) )
31 30 ss2rabi 
 |-  { x e. On | x ~< A } C_ { x e. On | x ~<_ A }
32 ssexg 
 |-  ( ( { x e. On | x ~< A } C_ { x e. On | x ~<_ A } /\ { x e. On | x ~<_ A } e. On ) -> { x e. On | x ~< A } e. _V )
33 31 32 mpan 
 |-  ( { x e. On | x ~<_ A } e. On -> { x e. On | x ~< A } e. _V )
34 elong 
 |-  ( { x e. On | x ~< A } e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) )
35 28 33 34 3syl 
 |-  ( A e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) )
36 27 35 mpbiri 
 |-  ( A e. _V -> { x e. On | x ~< A } e. On )
37 0elon 
 |-  (/) e. On
38 eleq1 
 |-  ( { x e. On | x ~< A } = (/) -> ( { x e. On | x ~< A } e. On <-> (/) e. On ) )
39 37 38 mpbiri 
 |-  ( { x e. On | x ~< A } = (/) -> { x e. On | x ~< A } e. On )
40 df-ne 
 |-  ( { x e. On | x ~< A } =/= (/) <-> -. { x e. On | x ~< A } = (/) )
41 rabn0 
 |-  ( { x e. On | x ~< A } =/= (/) <-> E. x e. On x ~< A )
42 40 41 bitr3i 
 |-  ( -. { x e. On | x ~< A } = (/) <-> E. x e. On x ~< A )
43 relsdom 
 |-  Rel ~<
44 43 brrelex2i 
 |-  ( x ~< A -> A e. _V )
45 44 rexlimivw 
 |-  ( E. x e. On x ~< A -> A e. _V )
46 42 45 sylbi 
 |-  ( -. { x e. On | x ~< A } = (/) -> A e. _V )
47 39 46 nsyl4 
 |-  ( -. A e. _V -> { x e. On | x ~< A } e. On )
48 36 47 pm2.61i 
 |-  { x e. On | x ~< A } e. On