Metamath Proof Explorer

Theorem cardid2

Description: Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A

Proof

Step Hyp Ref Expression
1 cardval3 ⊢ A ∈ dom ⁡ card → card ⁡ A = ⋂ y ∈ On | y ≈ A
2 ssrab2 ⊢ y ∈ On | y ≈ A ⊆ On
3 fvex ⊢ card ⁡ A ∈ V
4 1 3 eqeltrrdi ⊢ A ∈ dom ⁡ card → ⋂ y ∈ On | y ≈ A ∈ V
5 intex ⊢ y ∈ On | y ≈ A ≠ ∅ ↔ ⋂ y ∈ On | y ≈ A ∈ V
6 4 5 sylibr ⊢ A ∈ dom ⁡ card → y ∈ On | y ≈ A ≠ ∅
7 onint ⊢ y ∈ On | y ≈ A ⊆ On ∧ y ∈ On | y ≈ A ≠ ∅ → ⋂ y ∈ On | y ≈ A ∈ y ∈ On | y ≈ A
8 2 6 7 sylancr ⊢ A ∈ dom ⁡ card → ⋂ y ∈ On | y ≈ A ∈ y ∈ On | y ≈ A
9 1 8 eqeltrd ⊢ A ∈ dom ⁡ card → card ⁡ A ∈ y ∈ On | y ≈ A
10 breq1 ⊢ y = card ⁡ A → y ≈ A ↔ card ⁡ A ≈ A
11 10 elrab ⊢ card ⁡ A ∈ y ∈ On | y ≈ A ↔ card ⁡ A ∈ On ∧ card ⁡ A ≈ A
12 11 simprbi ⊢ card ⁡ A ∈ y ∈ On | y ≈ A → card ⁡ A ≈ A
13 9 12 syl ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A