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

Metamath Proof Explorer

Theorem canthwdom

Description: Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 , equivalent to canth ). (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion canthwdom ⊢ ¬ 𝒫 A ≼ * A

Proof

Step Hyp Ref Expression
1 0elpw ⊢ ∅ ∈ 𝒫 A
2 ne0i ⊢ ∅ ∈ 𝒫 A → 𝒫 A ≠ ∅
3 1 2 mp1i ⊢ 𝒫 A ≼ * A → 𝒫 A ≠ ∅
4 brwdomn0 ⊢ 𝒫 A ≠ ∅ → 𝒫 A ≼ * A ↔ ∃ f f : A ⟶ onto 𝒫 A
5 3 4 syl ⊢ 𝒫 A ≼ * A → 𝒫 A ≼ * A ↔ ∃ f f : A ⟶ onto 𝒫 A
6 5 ibi ⊢ 𝒫 A ≼ * A → ∃ f f : A ⟶ onto 𝒫 A
7 relwdom ⊢ Rel ⁡ ≼ *
8 7 brrelex2i ⊢ 𝒫 A ≼ * A → A ∈ V
9 foeq2 ⊢ x = A → f : x ⟶ onto 𝒫 x ↔ f : A ⟶ onto 𝒫 x
10 pweq ⊢ x = A → 𝒫 x = 𝒫 A
11 foeq3 ⊢ 𝒫 x = 𝒫 A → f : A ⟶ onto 𝒫 x ↔ f : A ⟶ onto 𝒫 A
12 10 11 syl ⊢ x = A → f : A ⟶ onto 𝒫 x ↔ f : A ⟶ onto 𝒫 A
13 9 12 bitrd ⊢ x = A → f : x ⟶ onto 𝒫 x ↔ f : A ⟶ onto 𝒫 A
14 13 notbid ⊢ x = A → ¬ f : x ⟶ onto 𝒫 x ↔ ¬ f : A ⟶ onto 𝒫 A
15 vex ⊢ x ∈ V
16 15 canth ⊢ ¬ f : x ⟶ onto 𝒫 x
17 14 16 vtoclg ⊢ A ∈ V → ¬ f : A ⟶ onto 𝒫 A
18 8 17 syl ⊢ 𝒫 A ≼ * A → ¬ f : A ⟶ onto 𝒫 A
19 18 nexdv ⊢ 𝒫 A ≼ * A → ¬ ∃ f f : A ⟶ onto 𝒫 A
20 6 19 pm2.65i ⊢ ¬ 𝒫 A ≼ * A