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