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

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 ‘ 𝐴 ) ≈ 𝐴 )