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	⊢ 𝐴 ∈ V
	Assertion	cardval	⊢ ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		cardval.1	⊢ 𝐴 ∈ V
2		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3		cardval3	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )
4	1 2 3	mp2b	⊢ ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 }