Theorem cardval3

Description: An alternate definition of the value of ( cardA ) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013) (Revised by Mario Carneiro, 27-Apr-2015)

	Ref	Expression
Assertion	cardval3	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ dom card → 𝐴 ∈ V )
2		isnum2	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
3		rabn0	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
4		intex	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V )
5	2 3 4	3bitr2i	⊢ ( 𝐴 ∈ dom card ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V )
6	5	biimpi	⊢ ( 𝐴 ∈ dom card → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V )
7		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≈ 𝑦 ↔ 𝑥 ≈ 𝐴 ) )
8	7	rabbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } = { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )
9	8	inteqd	⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )
10		df-card	⊢ card = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } )
11	9 10	fvmptg	⊢ ( ( 𝐴 ∈ V ∧ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V ) → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )
12	1 6 11	syl2anc	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )