Theorem cardne

Description: No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 9-Jan-2013)

	Ref	Expression
Assertion	cardne	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐵 ∈ dom card )
2		cardon	⊢ ( card ‘ 𝐵 ) ∈ On
3	2	oneli	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ∈ On )
4		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝐵 ↔ 𝐴 ≈ 𝐵 ) )
5	4	onintss	⊢ ( 𝐴 ∈ On → ( 𝐴 ≈ 𝐵 → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } ⊆ 𝐴 ) )
6	3 5	syl	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ( 𝐴 ≈ 𝐵 → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } ⊆ 𝐴 ) )
7	6	adantl	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( 𝐴 ≈ 𝐵 → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } ⊆ 𝐴 ) )
8		cardval3	⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } )
9	8	sseq1d	⊢ ( 𝐵 ∈ dom card → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } ⊆ 𝐴 ) )
10	9	adantr	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐵 } ⊆ 𝐴 ) )
11	7 10	sylibrd	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐵 ) ⊆ 𝐴 ) )
12		ontri1	⊢ ( ( ( card ‘ 𝐵 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
13	2 3 12	sylancr	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
14	13	adantl	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
15	11 14	sylibd	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( 𝐴 ≈ 𝐵 → ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
16	15	con2d	⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ ( card ‘ 𝐵 ) ) → ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 ) )
17	16	ex	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ∈ ( card ‘ 𝐵 ) → ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 ) ) )
18	17	pm2.43d	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 ) )
19	1 18	mpcom	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )