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