Metamath Proof Explorer

Theorem erdszelem7

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
erdszelem.k ⊢ 𝐾 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.o ⊢ 𝑂 Or ℝ
erdszelem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑁 ) )
erdszelem7.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
erdszelem7.m ⊢ ( 𝜑 → ¬ ( 𝐾 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) )
Assertion erdszelem7 ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
3 erdszelem.k ⊢ 𝐾 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
4 erdszelem.o ⊢ 𝑂 Or ℝ
5 erdszelem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑁 ) )
6 erdszelem7.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
7 erdszelem7.m ⊢ ( 𝜑 → ¬ ( 𝐾 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) )
8 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
9 ffun ⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → Fun ♯ )
10 8 9 ax-mp ⊢ Fun ♯
11 1 2 3 4 erdszelem5 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
12 5 11 mpdan ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
13 fvelima ⊢ ( ( Fun ♯ ∧ ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ) → ∃ 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) )
14 10 12 13 sylancr ⊢ ( 𝜑 → ∃ 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) )
15 eqid ⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
16 15 erdszelem1 ⊢ ( 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ↔ ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) )
17 simprl1 ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → 𝑠 ⊆ ( 1 ... 𝐴 ) )
18 elfzuz3 ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
19 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
20 5 18 19 3syl ⊢ ( 𝜑 → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
22 17 21 sstrd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → 𝑠 ⊆ ( 1 ... 𝑁 ) )
23 velpw ⊢ ( 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ↔ 𝑠 ⊆ ( 1 ... 𝑁 ) )
24 22 23 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) )
25 1 2 3 4 erdszelem6 ⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) ⟶ ℕ )
26 25 5 ffvelrnd ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐴 ) ∈ ℕ )
27 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
28 26 27 eleqtrdi ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
29 nnz ⊢ ( 𝑅 ∈ ℕ → 𝑅 ∈ ℤ )
30 peano2zm ⊢ ( 𝑅 ∈ ℤ → ( 𝑅 − 1 ) ∈ ℤ )
31 6 29 30 3syl ⊢ ( 𝜑 → ( 𝑅 − 1 ) ∈ ℤ )
32 elfz5 ⊢ ( ( ( 𝐾 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑅 − 1 ) ∈ ℤ ) → ( ( 𝐾 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ↔ ( 𝐾 ‘ 𝐴 ) ≤ ( 𝑅 − 1 ) ) )
33 28 31 32 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ↔ ( 𝐾 ‘ 𝐴 ) ≤ ( 𝑅 − 1 ) ) )
34 nnltlem1 ⊢ ( ( ( 𝐾 ‘ 𝐴 ) ∈ ℕ ∧ 𝑅 ∈ ℕ ) → ( ( 𝐾 ‘ 𝐴 ) < 𝑅 ↔ ( 𝐾 ‘ 𝐴 ) ≤ ( 𝑅 − 1 ) ) )
35 26 6 34 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐴 ) < 𝑅 ↔ ( 𝐾 ‘ 𝐴 ) ≤ ( 𝑅 − 1 ) ) )
36 33 35 bitr4d ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ↔ ( 𝐾 ‘ 𝐴 ) < 𝑅 ) )
37 7 36 mtbid ⊢ ( 𝜑 → ¬ ( 𝐾 ‘ 𝐴 ) < 𝑅 )
38 6 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
39 15 erdszelem2 ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℕ )
40 39 simpri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℕ
41 nnssre ⊢ ℕ ⊆ ℝ
42 40 41 sstri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℝ
43 42 12 sseldi ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐴 ) ∈ ℝ )
44 38 43 lenltd ⊢ ( 𝜑 → ( 𝑅 ≤ ( 𝐾 ‘ 𝐴 ) ↔ ¬ ( 𝐾 ‘ 𝐴 ) < 𝑅 ) )
45 37 44 mpbird ⊢ ( 𝜑 → 𝑅 ≤ ( 𝐾 ‘ 𝐴 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → 𝑅 ≤ ( 𝐾 ‘ 𝐴 ) )
47 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) )
48 46 47 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → 𝑅 ≤ ( ♯ ‘ 𝑠 ) )
49 simprl2 ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) )
50 24 48 49 jca32 ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) ) → ( 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
51 50 expr ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ∧ 𝐴 ∈ 𝑠 ) ) → ( ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) → ( 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ) )
52 16 51 sylan2b ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) → ( ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) → ( 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ) )
53 52 expimpd ⊢ ( 𝜑 → ( ( 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ∧ ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) ) → ( 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ) )
54 53 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑠 ) = ( 𝐾 ‘ 𝐴 ) → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
55 14 54 mpd ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , 𝑂 ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) )