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 ⊢ A ∈ dom ⁡ card → card ⁡ A = ⋂ x ∈ On | x ≈ A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ dom ⁡ card → A ∈ V
2 isnum2 ⊢ A ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ A
3 rabn0 ⊢ x ∈ On | x ≈ A ≠ ∅ ↔ ∃ x ∈ On x ≈ A
4 intex ⊢ x ∈ On | x ≈ A ≠ ∅ ↔ ⋂ x ∈ On | x ≈ A ∈ V
5 2 3 4 3bitr2i ⊢ A ∈ dom ⁡ card ↔ ⋂ x ∈ On | x ≈ A ∈ V
6 5 biimpi ⊢ A ∈ dom ⁡ card → ⋂ x ∈ On | x ≈ A ∈ V
7 breq2 ⊢ y = A → x ≈ y ↔ x ≈ A
8 7 rabbidv ⊢ y = A → x ∈ On | x ≈ y = x ∈ On | x ≈ A
9 8 inteqd ⊢ y = A → ⋂ x ∈ On | x ≈ y = ⋂ x ∈ On | x ≈ A
10 df-card ⊢ card = y ∈ V ⟼ ⋂ x ∈ On | x ≈ y
11 9 10 fvmptg ⊢ A ∈ V ∧ ⋂ x ∈ On | x ≈ A ∈ V → card ⁡ A = ⋂ x ∈ On | x ≈ A
12 1 6 11 syl2anc ⊢ A ∈ dom ⁡ card → card ⁡ A = ⋂ x ∈ On | x ≈ A