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