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 : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On
2	1	fdmi	⊢ dom card = { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 }
3		cardeqv	⊢ dom card = V
4	2 3	eqtr3i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } = V
5	4	feq2i	⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On ↔ card : V ⟶ On )
6	1 5	mpbi	⊢ card : V ⟶ On