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

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑓 : 𝒫 𝐴 ⟶ ( 𝐴 ⊔ 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 ) ≺ 𝒫 𝐴 )