This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cardval

Description: The value of the cardinal number function. Definition 10.4 of TakeutiZaring p. 85. See cardval2 for a simpler version of its value. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypothesis cardval.1 ⊢ A ∈ V
Assertion cardval ⊢ card ⁡ A = ⋂ x ∈ On | x ≈ A

Proof

Step Hyp Ref Expression
1 cardval.1 ⊢ A ∈ V
2 numth3 ⊢ A ∈ V → A ∈ dom ⁡ card
3 cardval3 ⊢ A ∈ dom ⁡ card → card ⁡ A = ⋂ x ∈ On | x ≈ A
4 1 2 3 mp2b ⊢ card ⁡ A = ⋂ x ∈ On | x ≈ A