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 ¬ 𝒫 𝐴* 𝐴

Proof

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