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

Metamath Proof Explorer

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 ∣ 𝑥 ≈ 𝐴 } )