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	syl6eqelr	⊢ ( 𝐴 ∈ 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 ‘ 𝐴 ) ≈ 𝐴 )