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

Metamath Proof Explorer

Theorem canthwdom

Proof