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 : { 𝑥 ∣ ∃ 𝑦 ∈ 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