MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isercolllem2 Structured version   Visualization version   GIF version

Theorem isercolllem2 15016
Description: Lemma for isercoll 15018. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
isercoll.z 𝑍 = (ℤ𝑀)
isercoll.m (𝜑𝑀 ∈ ℤ)
isercoll.g (𝜑𝐺:ℕ⟶𝑍)
isercoll.i ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
Assertion
Ref Expression
isercolllem2 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (1...(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁))))) = (𝐺 “ (𝑀...𝑁)))
Distinct variable groups:   𝑘,𝑁   𝜑,𝑘   𝑘,𝐺   𝑘,𝑀
Allowed substitution hint:   𝑍(𝑘)

Proof of Theorem isercolllem2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfznn 12930 . . . . . . . 8 (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈ ℕ)
21a1i 11 . . . . . . 7 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈ ℕ))
3 cnvimass 5943 . . . . . . . . 9 (𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺
4 isercoll.g . . . . . . . . . 10 (𝜑𝐺:ℕ⟶𝑍)
54adantr 483 . . . . . . . . 9 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 𝐺:ℕ⟶𝑍)
63, 5fssdm 6524 . . . . . . . 8 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ⊆ ℕ)
76sseld 3965 . . . . . . 7 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) → 𝑥 ∈ ℕ))
8 id 22 . . . . . . . . . . 11 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
9 nnuz 12275 . . . . . . . . . . 11 ℕ = (ℤ‘1)
108, 9eleqtrdi 2923 . . . . . . . . . 10 (𝑥 ∈ ℕ → 𝑥 ∈ (ℤ‘1))
11 ltso 10715 . . . . . . . . . . . . . 14 < Or ℝ
1211a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → < Or ℝ)
13 fzfid 13335 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑀...𝑁) ∈ Fin)
14 ffun 6511 . . . . . . . . . . . . . . . . 17 (𝐺:ℕ⟶𝑍 → Fun 𝐺)
15 funimacnv 6429 . . . . . . . . . . . . . . . . 17 (Fun 𝐺 → (𝐺 “ (𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺))
165, 14, 153syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺))
17 inss1 4204 . . . . . . . . . . . . . . . 16 ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁)
1816, 17eqsstrdi 4020 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁))
1913, 18ssfid 8735 . . . . . . . . . . . . . 14 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑁))) ∈ Fin)
20 ssid 3988 . . . . . . . . . . . . . . . . . . . . 21 ℕ ⊆ ℕ
21 isercoll.z . . . . . . . . . . . . . . . . . . . . . 22 𝑍 = (ℤ𝑀)
22 isercoll.m . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℤ)
23 isercoll.i . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
2421, 22, 4, 23isercolllem1 15015 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
2520, 24mpan2 689 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
26 ffn 6508 . . . . . . . . . . . . . . . . . . . . 21 (𝐺:ℕ⟶𝑍𝐺 Fn ℕ)
27 fnresdm 6460 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
28 isoeq1 7064 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
294, 26, 27, 284syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
3025, 29mpbid 234 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
31 isof1o 7070 . . . . . . . . . . . . . . . . . . 19 (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
32 f1ocnv 6621 . . . . . . . . . . . . . . . . . . 19 (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → 𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
33 f1ofun 6611 . . . . . . . . . . . . . . . . . . 19 (𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun 𝐺)
3430, 31, 32, 334syl 19 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝐺)
35 df-f1 6354 . . . . . . . . . . . . . . . . . 18 (𝐺:ℕ–1-1𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun 𝐺))
364, 34, 35sylanbrc 585 . . . . . . . . . . . . . . . . 17 (𝜑𝐺:ℕ–1-1𝑍)
3736adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 𝐺:ℕ–1-1𝑍)
38 nnex 11638 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
39 ssexg 5219 . . . . . . . . . . . . . . . . 17 (((𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ ℕ ∈ V) → (𝐺 “ (𝑀...𝑁)) ∈ V)
406, 38, 39sylancl 588 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ∈ V)
41 f1imaeng 8563 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ–1-1𝑍 ∧ (𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ (𝐺 “ (𝑀...𝑁)) ∈ V) → (𝐺 “ (𝐺 “ (𝑀...𝑁))) ≈ (𝐺 “ (𝑀...𝑁)))
4237, 6, 40, 41syl3anc 1367 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑁))) ≈ (𝐺 “ (𝑀...𝑁)))
4342ensymd 8554 . . . . . . . . . . . . . 14 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (𝐺 “ (𝑀...𝑁))))
44 enfii 8729 . . . . . . . . . . . . . 14 (((𝐺 “ (𝐺 “ (𝑀...𝑁))) ∈ Fin ∧ (𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (𝐺 “ (𝑀...𝑁)))) → (𝐺 “ (𝑀...𝑁)) ∈ Fin)
4519, 43, 44syl2anc 586 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ∈ Fin)
46 1nn 11643 . . . . . . . . . . . . . . . 16 1 ∈ ℕ
4746a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 1 ∈ ℕ)
48 ffvelrn 6843 . . . . . . . . . . . . . . . . . . 19 ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
494, 46, 48sylancl 588 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺‘1) ∈ 𝑍)
5049, 21eleqtrdi 2923 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘1) ∈ (ℤ𝑀))
5150adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘1) ∈ (ℤ𝑀))
52 simpr 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 𝑁 ∈ (ℤ‘(𝐺‘1)))
53 elfzuzb 12896 . . . . . . . . . . . . . . . 16 ((𝐺‘1) ∈ (𝑀...𝑁) ↔ ((𝐺‘1) ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ‘(𝐺‘1))))
5451, 52, 53sylanbrc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘1) ∈ (𝑀...𝑁))
555ffnd 6509 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 𝐺 Fn ℕ)
56 elpreima 6822 . . . . . . . . . . . . . . . 16 (𝐺 Fn ℕ → (1 ∈ (𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁))))
5755, 56syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (1 ∈ (𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁))))
5847, 54, 57mpbir2and 711 . . . . . . . . . . . . . 14 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → 1 ∈ (𝐺 “ (𝑀...𝑁)))
5958ne0d 4300 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ≠ ∅)
60 nnssre 11636 . . . . . . . . . . . . . 14 ℕ ⊆ ℝ
616, 60sstrdi 3978 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝑀...𝑁)) ⊆ ℝ)
62 fisupcl 8927 . . . . . . . . . . . . 13 (( < Or ℝ ∧ ((𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ (𝐺 “ (𝑀...𝑁)) ⊆ ℝ)) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (𝐺 “ (𝑀...𝑁)))
6312, 45, 59, 61, 62syl13anc 1368 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (𝐺 “ (𝑀...𝑁)))
646, 63sseldd 3967 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ)
6564nnzd 12080 . . . . . . . . . 10 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℤ)
66 elfz5 12894 . . . . . . . . . 10 ((𝑥 ∈ (ℤ‘1) ∧ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℤ) → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < )))
6710, 65, 66syl2anr 598 . . . . . . . . 9 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < )))
68 elpreima 6822 . . . . . . . . . . . . . . . . 17 (𝐺 Fn ℕ → (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (𝐺 “ (𝑀...𝑁)) ↔ (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁))))
6955, 68syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (𝐺 “ (𝑀...𝑁)) ↔ (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁))))
7063, 69mpbid 234 . . . . . . . . . . . . . . 15 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)))
71 elfzle2 12905 . . . . . . . . . . . . . . 15 ((𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁)
7270, 71simpl2im 506 . . . . . . . . . . . . . 14 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁)
7372adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁)
74 uzssz 12258 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ⊆ ℤ
7521, 74eqsstri 4000 . . . . . . . . . . . . . . . 16 𝑍 ⊆ ℤ
76 zssre 11982 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℝ
7775, 76sstri 3975 . . . . . . . . . . . . . . 15 𝑍 ⊆ ℝ
785ffvelrnda 6845 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑥) ∈ 𝑍)
7977, 78sseldi 3964 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑥) ∈ ℝ)
805, 64ffvelrnd 6846 . . . . . . . . . . . . . . . 16 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍)
8180adantr 483 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍)
8277, 81sseldi 3964 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ ℝ)
83 eluzelz 12247 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘(𝐺‘1)) → 𝑁 ∈ ℤ)
8483ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈ ℤ)
8576, 84sseldi 3964 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈ ℝ)
86 letr 10728 . . . . . . . . . . . . . 14 (((𝐺𝑥) ∈ ℝ ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐺𝑥) ≤ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺𝑥) ≤ 𝑁))
8779, 82, 85, 86syl3anc 1367 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (((𝐺𝑥) ≤ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺𝑥) ≤ 𝑁))
8873, 87mpan2d 692 . . . . . . . . . . . 12 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺𝑥) ≤ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) → (𝐺𝑥) ≤ 𝑁))
8930ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
9060a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ)
91 ressxr 10679 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ*
9290, 91sstrdi 3978 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ*)
93 imassrn 5934 . . . . . . . . . . . . . . . 16 (𝐺 “ ℕ) ⊆ ran 𝐺
944ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
9594frnd 6515 . . . . . . . . . . . . . . . 16 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺𝑍)
9693, 95sstrid 3977 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ 𝑍)
9796, 77sstrdi 3978 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
9897, 91sstrdi 3978 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ*)
99 simpr 487 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
10064adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ)
101 leisorel 13812 . . . . . . . . . . . . 13 ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ* ∧ (𝐺 “ ℕ) ⊆ ℝ*) ∧ (𝑥 ∈ ℕ ∧ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ)) → (𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺𝑥) ≤ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))))
10289, 92, 98, 99, 100, 101syl122anc 1375 . . . . . . . . . . . 12 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺𝑥) ≤ (𝐺‘sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))))
10378, 21eleqtrdi 2923 . . . . . . . . . . . . 13 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑥) ∈ (ℤ𝑀))
104 elfz5 12894 . . . . . . . . . . . . 13 (((𝐺𝑥) ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → ((𝐺𝑥) ∈ (𝑀...𝑁) ↔ (𝐺𝑥) ≤ 𝑁))
105103, 84, 104syl2anc 586 . . . . . . . . . . . 12 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺𝑥) ∈ (𝑀...𝑁) ↔ (𝐺𝑥) ≤ 𝑁))
10688, 102, 1053imtr4d 296 . . . . . . . . . . 11 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) → (𝐺𝑥) ∈ (𝑀...𝑁)))
107 elpreima 6822 . . . . . . . . . . . . 13 (𝐺 Fn ℕ → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) ↔ (𝑥 ∈ ℕ ∧ (𝐺𝑥) ∈ (𝑀...𝑁))))
108107baibd 542 . . . . . . . . . . . 12 ((𝐺 Fn ℕ ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) ↔ (𝐺𝑥) ∈ (𝑀...𝑁)))
10955, 108sylan 582 . . . . . . . . . . 11 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) ↔ (𝐺𝑥) ∈ (𝑀...𝑁)))
110106, 109sylibrd 261 . . . . . . . . . 10 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) → 𝑥 ∈ (𝐺 “ (𝑀...𝑁))))
111 fimaxre2 11580 . . . . . . . . . . . . 13 (((𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (𝐺 “ (𝑀...𝑁)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐺 “ (𝑀...𝑁))𝑦𝑥)
11261, 45, 111syl2anc 586 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐺 “ (𝑀...𝑁))𝑦𝑥)
113 suprub 11596 . . . . . . . . . . . . 13 ((((𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐺 “ (𝑀...𝑁))𝑦𝑥) ∧ 𝑥 ∈ (𝐺 “ (𝑀...𝑁))) → 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))
114113ex 415 . . . . . . . . . . . 12 (((𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐺 “ (𝑀...𝑁))𝑦𝑥) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < )))
11561, 59, 112, 114syl3anc 1367 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < )))
116115adantr 483 . . . . . . . . . 10 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < )))
117110, 116impbid 214 . . . . . . . . 9 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ 𝑥 ∈ (𝐺 “ (𝑀...𝑁))))
11867, 117bitrd 281 . . . . . . . 8 (((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (𝐺 “ (𝑀...𝑁))))
119118ex 415 . . . . . . 7 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑥 ∈ ℕ → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (𝐺 “ (𝑀...𝑁)))))
1202, 7, 119pm5.21ndd 383 . . . . . 6 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (𝑥 ∈ (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (𝐺 “ (𝑀...𝑁))))
121120eqrdv 2819 . . . . 5 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) = (𝐺 “ (𝑀...𝑁)))
122121fveq2d 6668 . . . 4 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (♯‘(1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))) = (♯‘(𝐺 “ (𝑀...𝑁))))
12364nnnn0d 11949 . . . . 5 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ0)
124 hashfz1 13700 . . . . 5 (sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ0 → (♯‘(1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))
125123, 124syl 17 . . . 4 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (♯‘(1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((𝐺 “ (𝑀...𝑁)), ℝ, < ))
126 hashen 13701 . . . . . 6 (((𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (𝐺 “ (𝐺 “ (𝑀...𝑁))) ∈ Fin) → ((♯‘(𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (𝐺 “ (𝑀...𝑁)))))
12745, 19, 126syl2anc 586 . . . . 5 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → ((♯‘(𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (𝐺 “ (𝑀...𝑁)))))
12843, 127mpbird 259 . . . 4 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (♯‘(𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁)))))
129122, 125, 1283eqtr3d 2864 . . 3 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → sup((𝐺 “ (𝑀...𝑁)), ℝ, < ) = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁)))))
130129oveq2d 7166 . 2 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (1...sup((𝐺 “ (𝑀...𝑁)), ℝ, < )) = (1...(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁))))))
131130, 121eqtr3d 2858 1 ((𝜑𝑁 ∈ (ℤ‘(𝐺‘1))) → (1...(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑁))))) = (𝐺 “ (𝑀...𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1533  wcel 2110  wne 3016  wral 3138  wrex 3139  Vcvv 3494  cin 3934  wss 3935  c0 4290   class class class wbr 5058   Or wor 5467  ccnv 5548  ran crn 5550  cres 5551  cima 5552  Fun wfun 6343   Fn wfn 6344  wf 6345  1-1wf1 6346  1-1-ontowf1o 6348  cfv 6349   Isom wiso 6350  (class class class)co 7150  cen 8500  Fincfn 8503  supcsup 8898  cr 10530  1c1 10532   + caddc 10534  *cxr 10668   < clt 10669  cle 10670  cn 11632  0cn0 11891  cz 11975  cuz 12237  ...cfz 12886  chash 13684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976  df-uz 12238  df-fz 12887  df-hash 13685
This theorem is referenced by:  isercolllem3  15017
  Copyright terms: Public domain W3C validator