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 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 cardval3 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑦 ∈ On ∣ 𝑦𝐴 } )
2 ssrab2 { 𝑦 ∈ On ∣ 𝑦𝐴 } ⊆ On
3 fvex ( card ‘ 𝐴 ) ∈ V
4 1 3 eqeltrrdi ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦𝐴 } ∈ V )
5 intex ( { 𝑦 ∈ On ∣ 𝑦𝐴 } ≠ ∅ ↔ { 𝑦 ∈ On ∣ 𝑦𝐴 } ∈ V )
6 4 5 sylibr ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦𝐴 } ≠ ∅ )
7 onint ( ( { 𝑦 ∈ On ∣ 𝑦𝐴 } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝑦𝐴 } ≠ ∅ ) → { 𝑦 ∈ On ∣ 𝑦𝐴 } ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } )
8 2 6 7 sylancr ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦𝐴 } ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } )
9 1 8 eqeltrd ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } )
10 breq1 ( 𝑦 = ( card ‘ 𝐴 ) → ( 𝑦𝐴 ↔ ( card ‘ 𝐴 ) ≈ 𝐴 ) )
11 10 elrab ( ( card ‘ 𝐴 ) ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } ↔ ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) )
12 11 simprbi ( ( card ‘ 𝐴 ) ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } → ( card ‘ 𝐴 ) ≈ 𝐴 )
13 9 12 syl ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )