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

Metamath Proof Explorer

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