| Step | Hyp | Ref
| Expression |
| 1 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈
ℕ) |
| 2 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈
ℕ)) |
| 3 | | cnvimass 6100 |
. . . . . . . . 9
⊢ (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 |
| 4 | | isercoll.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶𝑍) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ⟶𝑍) |
| 6 | 3, 5 | fssdm 6755 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) |
| 7 | 6 | sseld 3982 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ∈ ℕ)) |
| 8 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
| 9 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 10 | 8, 9 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
(ℤ≥‘1)) |
| 11 | | ltso 11341 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → < Or
ℝ) |
| 13 | | fzfid 14014 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑀...𝑁) ∈ Fin) |
| 14 | | ffun 6739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺) |
| 15 | | funimacnv 6647 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
| 16 | 5, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
| 17 | | inss1 4237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁) |
| 18 | 16, 17 | eqsstrdi 4028 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁)) |
| 19 | 13, 18 | ssfid 9301 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin) |
| 20 | | ssid 4006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ
⊆ ℕ |
| 21 | | isercoll.z |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 22 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 23 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
| 24 | 21, 22, 4, 23 | isercolllem1 15701 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ℕ ⊆ ℕ)
→ (𝐺 ↾ ℕ)
Isom < , < (ℕ, (𝐺 “ ℕ))) |
| 25 | 20, 24 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “
ℕ))) |
| 26 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ) |
| 27 | | fnresdm 6687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺) |
| 28 | | isoeq1 7337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
| 29 | 4, 26, 27, 28 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
| 30 | 25, 29 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “
ℕ))) |
| 31 | | isof1o 7343 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) →
𝐺:ℕ–1-1-onto→(𝐺 “ ℕ)) |
| 32 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ) |
| 33 | | f1ofun 6850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ◡𝐺) |
| 34 | 30, 31, 32, 33 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun ◡𝐺) |
| 35 | | df-f1 6566 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ◡𝐺)) |
| 36 | 4, 34, 35 | sylanbrc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ–1-1→𝑍) |
| 38 | | nnex 12272 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
| 39 | | ssexg 5323 |
. . . . . . . . . . . . . . . . 17
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ ℕ ∈ V)
→ (◡𝐺 “ (𝑀...𝑁)) ∈ V) |
| 40 | 6, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ∈ V) |
| 41 | | f1imaeng 9054 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ (◡𝐺 “ (𝑀...𝑁)) ∈ V) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≈ (◡𝐺 “ (𝑀...𝑁))) |
| 42 | 37, 6, 40, 41 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≈ (◡𝐺 “ (𝑀...𝑁))) |
| 43 | 42 | ensymd 9045 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) |
| 44 | | enfii 9226 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin ∧ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) → (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) |
| 45 | 19, 43, 44 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) |
| 46 | | 1nn 12277 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ |
| 47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
ℕ) |
| 48 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) →
(𝐺‘1) ∈ 𝑍) |
| 49 | 4, 46, 48 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺‘1) ∈ 𝑍) |
| 50 | 49, 21 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
| 52 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝑁 ∈
(ℤ≥‘(𝐺‘1))) |
| 53 | | elfzuzb 13558 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘1) ∈ (𝑀...𝑁) ↔ ((𝐺‘1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1)))) |
| 54 | 51, 52, 53 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈ (𝑀...𝑁)) |
| 55 | 5 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺 Fn ℕ) |
| 56 | | elpreima 7078 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 Fn ℕ → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
| 58 | 47, 54, 57 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
(◡𝐺 “ (𝑀...𝑁))) |
| 59 | 58 | ne0d 4342 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
| 60 | | nnssre 12270 |
. . . . . . . . . . . . . 14
⊢ ℕ
⊆ ℝ |
| 61 | 6, 60 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ) |
| 62 | | fisupcl 9509 |
. . . . . . . . . . . . 13
⊢ (( <
Or ℝ ∧ ((◡𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ)) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁))) |
| 63 | 12, 45, 59, 61, 62 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁))) |
| 64 | 6, 63 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ) |
| 65 | 64 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℤ) |
| 66 | | elfz5 13556 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘1) ∧ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℤ) →
(𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
| 67 | 10, 65, 66 | syl2anr 597 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
| 68 | | elpreima 7078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn ℕ → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)))) |
| 69 | 55, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)))) |
| 70 | 63, 69 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁))) |
| 71 | | elfzle2 13568 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
| 72 | 70, 71 | simpl2im 503 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
| 74 | | uzssz 12899 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 75 | 21, 74 | eqsstri 4030 |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 ⊆
ℤ |
| 76 | | zssre 12620 |
. . . . . . . . . . . . . . . 16
⊢ ℤ
⊆ ℝ |
| 77 | 75, 76 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 ⊆
ℝ |
| 78 | 5 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍) |
| 79 | 77, 78 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ ℝ) |
| 80 | 5, 64 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍) |
| 82 | 77, 81 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈
ℝ) |
| 83 | | eluzelz 12888 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘(𝐺‘1)) → 𝑁 ∈ ℤ) |
| 84 | 83 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈
ℤ) |
| 85 | 76, 84 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 86 | | letr 11355 |
. . . . . . . . . . . . . 14
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ ℝ ∧
𝑁 ∈ ℝ) →
(((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺‘𝑥) ≤ 𝑁)) |
| 87 | 79, 82, 85, 86 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺‘𝑥) ≤ 𝑁)) |
| 88 | 73, 87 | mpan2d 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → (𝐺‘𝑥) ≤ 𝑁)) |
| 89 | 30 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ,
(𝐺 “
ℕ))) |
| 90 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ
⊆ ℝ) |
| 91 | | ressxr 11305 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* |
| 92 | 90, 91 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ
⊆ ℝ*) |
| 93 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 “ ℕ) ⊆ ran
𝐺 |
| 94 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍) |
| 95 | 94 | frnd 6744 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ran
𝐺 ⊆ 𝑍) |
| 96 | 93, 95 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ 𝑍) |
| 97 | 96, 77 | sstrdi 3996 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ) |
| 98 | 97, 91 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ*) |
| 99 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈
ℕ) |
| 100 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) →
sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ) |
| 101 | | leisorel 14499 |
. . . . . . . . . . . . 13
⊢ ((𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) ∧
(ℕ ⊆ ℝ* ∧ (𝐺 “ ℕ) ⊆
ℝ*) ∧ (𝑥 ∈ ℕ ∧ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ)) →
(𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )))) |
| 102 | 89, 92, 98, 99, 100, 101 | syl122anc 1381 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )))) |
| 103 | 78, 21 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ≥‘𝑀)) |
| 104 | | elfz5 13556 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑥) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...𝑁) ↔ (𝐺‘𝑥) ≤ 𝑁)) |
| 105 | 103, 84, 104 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...𝑁) ↔ (𝐺‘𝑥) ≤ 𝑁)) |
| 106 | 88, 102, 105 | 3imtr4d 294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) → (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
| 107 | | elpreima 7078 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn ℕ → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...𝑁)))) |
| 108 | 107 | baibd 539 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn ℕ ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
| 109 | 55, 108 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
| 110 | 106, 109 | sylibrd 259 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) → 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
| 111 | | fimaxre2 12213 |
. . . . . . . . . . . . 13
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) |
| 112 | 61, 45, 111 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) |
| 113 | | suprub 12229 |
. . . . . . . . . . . . 13
⊢ ((((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) ∧ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁))) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
| 114 | 113 | ex 412 |
. . . . . . . . . . . 12
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
| 115 | 61, 59, 112, 114 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
| 116 | 115 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
| 117 | 110, 116 | impbid 212 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
| 118 | 67, 117 | bitrd 279 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
| 119 | 118 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ ℕ → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁))))) |
| 120 | 2, 7, 119 | pm5.21ndd 379 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
| 121 | 120 | eqrdv 2735 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) = (◡𝐺 “ (𝑀...𝑁))) |
| 122 | 121 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) =
(♯‘(◡𝐺 “ (𝑀...𝑁)))) |
| 123 | 64 | nnnn0d 12587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ0) |
| 124 | | hashfz1 14385 |
. . . . 5
⊢
(sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ0 → (♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
| 125 | 123, 124 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
| 126 | | hashen 14386 |
. . . . . 6
⊢ (((◡𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin) →
((♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
| 127 | 45, 19, 126 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
((♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
| 128 | 43, 127 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
| 129 | 122, 125,
128 | 3eqtr3d 2785 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
| 130 | 129 | oveq2d 7447 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) =
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) |
| 131 | 130, 121 | eqtr3d 2779 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁))) |