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 ⊢ A ∈ card ⁡ B → ¬ A ≈ B

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ A ∈ card ⁡ B → B ∈ dom ⁡ card
2 cardon ⊢ card ⁡ B ∈ On
3 2 oneli ⊢ A ∈ card ⁡ B → A ∈ On
4 breq1 ⊢ x = A → x ≈ B ↔ A ≈ B
5 4 onintss ⊢ A ∈ On → A ≈ B → ⋂ x ∈ On | x ≈ B ⊆ A
6 3 5 syl ⊢ A ∈ card ⁡ B → A ≈ B → ⋂ x ∈ On | x ≈ B ⊆ A
7 6 adantl ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → A ≈ B → ⋂ x ∈ On | x ≈ B ⊆ A
8 cardval3 ⊢ B ∈ dom ⁡ card → card ⁡ B = ⋂ x ∈ On | x ≈ B
9 8 sseq1d ⊢ B ∈ dom ⁡ card → card ⁡ B ⊆ A ↔ ⋂ x ∈ On | x ≈ B ⊆ A
10 9 adantr ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → card ⁡ B ⊆ A ↔ ⋂ x ∈ On | x ≈ B ⊆ A
11 7 10 sylibrd ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → A ≈ B → card ⁡ B ⊆ A
12 ontri1 ⊢ card ⁡ B ∈ On ∧ A ∈ On → card ⁡ B ⊆ A ↔ ¬ A ∈ card ⁡ B
13 2 3 12 sylancr ⊢ A ∈ card ⁡ B → card ⁡ B ⊆ A ↔ ¬ A ∈ card ⁡ B
14 13 adantl ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → card ⁡ B ⊆ A ↔ ¬ A ∈ card ⁡ B
15 11 14 sylibd ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → A ≈ B → ¬ A ∈ card ⁡ B
16 15 con2d ⊢ B ∈ dom ⁡ card ∧ A ∈ card ⁡ B → A ∈ card ⁡ B → ¬ A ≈ B
17 16 ex ⊢ B ∈ dom ⁡ card → A ∈ card ⁡ B → A ∈ card ⁡ B → ¬ A ≈ B
18 17 pm2.43d ⊢ B ∈ dom ⁡ card → A ∈ card ⁡ B → ¬ A ≈ B
19 1 18 mpcom ⊢ A ∈ card ⁡ B → ¬ A ≈ B