Theorem canthp1

Description: A slightly stronger form of Cantor's theorem: For 1 < n , n + 1 < 2 ^ n . Corollary 1.6 of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	canthp1	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1sdom2	⊢ 1o ≺ 2o
2		sdomdom	⊢ ( 1o ≺ 2o → 1o ≼ 2o )
3	1 2	ax-mp	⊢ 1o ≼ 2o
4		relsdom	⊢ Rel ≺
5	4	brrelex2i	⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
6		djudom2	⊢ ( ( 1o ≼ 2o ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 1o ) ≼ ( 𝐴 ⊔ 2o ) )
7	3 5 6	sylancr	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≼ ( 𝐴 ⊔ 2o ) )
8		canthp1lem1	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
9		domtr	⊢ ( ( ( 𝐴 ⊔ 1o ) ≼ ( 𝐴 ⊔ 2o ) ∧ ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 1o ) ≼ 𝒫 𝐴 )
10	7 8 9	syl2anc	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≼ 𝒫 𝐴 )
11		fal	⊢ ¬ ⊥
12		ensym	⊢ ( ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
13		bren	⊢ ( 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1o ) ↔ ∃ 𝑓 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) )
14	12 13	sylib	⊢ ( ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 → ∃ 𝑓 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) )
15		f1of	⊢ ( 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) → 𝑓 : 𝒫 𝐴 ⟶ ( 𝐴 ⊔ 1o ) )
16		pwidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
17	5 16	syl	⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ 𝒫 𝐴 )
18		ffvelrn	⊢ ( ( 𝑓 : 𝒫 𝐴 ⟶ ( 𝐴 ⊔ 1o ) ∧ 𝐴 ∈ 𝒫 𝐴 ) → ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐴 ⊔ 1o ) )
19	15 17 18	syl2anr	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐴 ⊔ 1o ) )
20		dju1dif	⊢ ( ( 𝐴 ∈ V ∧ ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ 𝐴 )
21	5 19 20	syl2an2r	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ 𝐴 )
22		bren	⊢ ( ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ 𝐴 ↔ ∃ 𝑔 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
23	21 22	sylib	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) → ∃ 𝑔 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
24		simpll	⊢ ( ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) ∧ 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 ) → 1o ≺ 𝐴 )
25		simplr	⊢ ( ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) ∧ 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 ) → 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) )
26		simpr	⊢ ( ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) ∧ 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 ) → 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
27		eqeq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝐴 ↔ 𝑥 = 𝐴 ) )
28		id	⊢ ( 𝑤 = 𝑥 → 𝑤 = 𝑥 )
29	27 28	ifbieq2d	⊢ ( 𝑤 = 𝑥 → if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) = if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) )
30	29	cbvmptv	⊢ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) )
31	30	coeq2i	⊢ ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) = ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) )
32		eqid	⊢ { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) }
33	32	fpwwecbv	⊢ { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
34		eqid	⊢ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) } = ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( ( ( 𝑔 ∘ 𝑓 ) ∘ ( 𝑤 ∈ 𝒫 𝐴 ↦ if ( 𝑤 = 𝐴 , ∅ , 𝑤 ) ) ) ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) }
35	24 25 26 31 33 34	canthp1lem2	⊢ ¬ ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) ∧ 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
36	35	pm2.21i	⊢ ( ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) ∧ 𝑔 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 ) → ⊥ )
37	23 36	exlimddv	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) ) → ⊥ )
38	37	ex	⊢ ( 1o ≺ 𝐴 → ( 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) → ⊥ ) )
39	38	exlimdv	⊢ ( 1o ≺ 𝐴 → ( ∃ 𝑓 𝑓 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1o ) → ⊥ ) )
40	14 39	syl5	⊢ ( 1o ≺ 𝐴 → ( ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 → ⊥ ) )
41	11 40	mtoi	⊢ ( 1o ≺ 𝐴 → ¬ ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
42		brsdom	⊢ ( ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ↔ ( ( 𝐴 ⊔ 1o ) ≼ 𝒫 𝐴 ∧ ¬ ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 ) )
43	10 41 42	sylanbrc	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )