# 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`