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	$$⊢\mathrm{card}:\mathrm{V}⟶\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		cardf2	$$⊢\mathrm{card}:\left\{x|\exists y\in \mathrm{On}y\approx x\right\}⟶\mathrm{On}$$
2	1	fdmi	$$⊢\mathrm{dom}\mathrm{card}=\left\{x|\exists y\in \mathrm{On}y\approx x\right\}$$
3		cardeqv	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}$$
4	2 3	eqtr3i	$$⊢\left\{x|\exists y\in \mathrm{On}y\approx x\right\}=\mathrm{V}$$
5	4	feq2i	$$⊢\mathrm{card}:\left\{x|\exists y\in \mathrm{On}y\approx x\right\}⟶\mathrm{On}\leftrightarrow \mathrm{card}:\mathrm{V}⟶\mathrm{On}$$
6	1 5	mpbi	$$⊢\mathrm{card}:\mathrm{V}⟶\mathrm{On}$$