Metamath Proof Explorer

Theorem cardf2

Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion cardf2 
|- card : { x | E. y e. On y ~~ x } --> On

Proof

Step Hyp Ref Expression
1 df-card 
 |-  card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
2 1 funmpt2 
 |-  Fun card
3 rabab 
 |-  { x e. _V | |^| { y e. On | y ~~ x } e. _V } = { x | |^| { y e. On | y ~~ x } e. _V }
4 1 dmmpt 
 |-  dom card = { x e. _V | |^| { y e. On | y ~~ x } e. _V }
5 intexrab 
 |-  ( E. y e. On y ~~ x <-> |^| { y e. On | y ~~ x } e. _V )
6 5 abbii 
 |-  { x | E. y e. On y ~~ x } = { x | |^| { y e. On | y ~~ x } e. _V }
7 3 4 6 3eqtr4i 
 |-  dom card = { x | E. y e. On y ~~ x }
8 df-fn 
 |-  ( card Fn { x | E. y e. On y ~~ x } <-> ( Fun card /\ dom card = { x | E. y e. On y ~~ x } ) )
9 2 7 8 mpbir2an 
 |-  card Fn { x | E. y e. On y ~~ x }
10 simpr 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> w = |^| { y e. On | y ~~ z } )
11 vex 
 |-  w e. _V
12 10 11 eqeltrrdi 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> |^| { y e. On | y ~~ z } e. _V )
13 intex 
 |-  ( { y e. On | y ~~ z } =/= (/) <-> |^| { y e. On | y ~~ z } e. _V )
14 12 13 sylibr 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> { y e. On | y ~~ z } =/= (/) )
15 rabn0 
 |-  ( { y e. On | y ~~ z } =/= (/) <-> E. y e. On y ~~ z )
16 14 15 sylib 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> E. y e. On y ~~ z )
17 vex 
 |-  z e. _V
18 breq2 
 |-  ( x = z -> ( y ~~ x <-> y ~~ z ) )
19 18 rexbidv 
 |-  ( x = z -> ( E. y e. On y ~~ x <-> E. y e. On y ~~ z ) )
20 17 19 elab 
 |-  ( z e. { x | E. y e. On y ~~ x } <-> E. y e. On y ~~ z )
21 16 20 sylibr 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> z e. { x | E. y e. On y ~~ x } )
22 ssrab2 
 |-  { y e. On | y ~~ z } C_ On
23 oninton 
 |-  ( ( { y e. On | y ~~ z } C_ On /\ { y e. On | y ~~ z } =/= (/) ) -> |^| { y e. On | y ~~ z } e. On )
24 22 14 23 sylancr 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> |^| { y e. On | y ~~ z } e. On )
25 10 24 eqeltrd 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> w e. On )
26 21 25 jca 
 |-  ( ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) -> ( z e. { x | E. y e. On y ~~ x } /\ w e. On ) )
27 26 ssopab2i 
 |-  { <. z , w >. | ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) } C_ { <. z , w >. | ( z e. { x | E. y e. On y ~~ x } /\ w e. On ) }
28 df-card 
 |-  card = ( z e. _V |-> |^| { y e. On | y ~~ z } )
29 df-mpt 
 |-  ( z e. _V |-> |^| { y e. On | y ~~ z } ) = { <. z , w >. | ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) }
30 28 29 eqtri 
 |-  card = { <. z , w >. | ( z e. _V /\ w = |^| { y e. On | y ~~ z } ) }
31 df-xp 
 |-  ( { x | E. y e. On y ~~ x } X. On ) = { <. z , w >. | ( z e. { x | E. y e. On y ~~ x } /\ w e. On ) }
32 27 30 31 3sstr4i 
 |-  card C_ ( { x | E. y e. On y ~~ x } X. On )
33 dff2 
 |-  ( card : { x | E. y e. On y ~~ x } --> On <-> ( card Fn { x | E. y e. On y ~~ x } /\ card C_ ( { x | E. y e. On y ~~ x } X. On ) ) )
34 9 32 33 mpbir2an 
 |-  card : { x | E. y e. On y ~~ x } --> On