Metamath Proof Explorer


Theorem cardf

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, 13-Sep-2013)

Ref Expression
Assertion cardf
|- card : _V --> On

Proof

Step Hyp Ref Expression
1 cardf2
 |-  card : { x | E. y e. On y ~~ x } --> On
2 1 fdmi
 |-  dom card = { x | E. y e. On y ~~ x }
3 cardeqv
 |-  dom card = _V
4 2 3 eqtr3i
 |-  { x | E. y e. On y ~~ x } = _V
5 4 feq2i
 |-  ( card : { x | E. y e. On y ~~ x } --> On <-> card : _V --> On )
6 1 5 mpbi
 |-  card : _V --> On