Step | Hyp | Ref
| Expression |
1 | | elfznn 12664 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈
ℕ) |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → 𝑥 ∈
ℕ)) |
3 | | cnvimass 5727 |
. . . . . . . . 9
⊢ (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 |
4 | | isercoll.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶𝑍) |
5 | 4 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ⟶𝑍) |
6 | 3, 5 | fssdm 6295 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) |
7 | 6 | sseld 3827 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ∈ ℕ)) |
8 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
9 | | nnuz 12006 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | syl6eleq 2917 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
(ℤ≥‘1)) |
11 | | ltso 10438 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → < Or
ℝ) |
13 | | fzfid 13068 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑀...𝑁) ∈ Fin) |
14 | | ffun 6282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺) |
15 | | funimacnv 6204 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
16 | 5, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
17 | | inss1 4058 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁) |
18 | 16, 17 | syl6eqss 3881 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁)) |
19 | | ssfi 8450 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀...𝑁) ∈ Fin ∧ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁)) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin) |
20 | 13, 18, 19 | syl2anc 581 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin) |
21 | | ssid 3849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ
⊆ ℕ |
22 | | isercoll.z |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑍 =
(ℤ≥‘𝑀) |
23 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℤ) |
24 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
25 | 22, 23, 4, 24 | isercolllem1 14773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ℕ ⊆ ℕ)
→ (𝐺 ↾ ℕ)
Isom < , < (ℕ, (𝐺 “ ℕ))) |
26 | 21, 25 | mpan2 684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “
ℕ))) |
27 | | ffn 6279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ) |
28 | | fnresdm 6234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺) |
29 | | isoeq1 6823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
30 | 4, 27, 28, 29 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
31 | 26, 30 | mpbid 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “
ℕ))) |
32 | | isof1o 6829 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) →
𝐺:ℕ–1-1-onto→(𝐺 “ ℕ)) |
33 | | f1ocnv 6391 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ) |
34 | | f1ofun 6381 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ◡𝐺) |
35 | 31, 32, 33, 34 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun ◡𝐺) |
36 | | df-f1 6129 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ◡𝐺)) |
37 | 4, 35, 36 | sylanbrc 580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍) |
38 | 37 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ–1-1→𝑍) |
39 | | nnex 11358 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
40 | | ssexg 5030 |
. . . . . . . . . . . . . . . . 17
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ ℕ ∈ V)
→ (◡𝐺 “ (𝑀...𝑁)) ∈ V) |
41 | 6, 39, 40 | sylancl 582 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ∈ V) |
42 | | f1imaeng 8283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ ∧ (◡𝐺 “ (𝑀...𝑁)) ∈ V) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≈ (◡𝐺 “ (𝑀...𝑁))) |
43 | 38, 6, 41, 42 | syl3anc 1496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≈ (◡𝐺 “ (𝑀...𝑁))) |
44 | 43 | ensymd 8274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) |
45 | | enfii 8447 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin ∧ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) → (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) |
46 | 20, 44, 45 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) |
47 | | 1nn 11364 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
ℕ) |
49 | | ffvelrn 6607 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) →
(𝐺‘1) ∈ 𝑍) |
50 | 4, 47, 49 | sylancl 582 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺‘1) ∈ 𝑍) |
51 | 50, 22 | syl6eleq 2917 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
52 | 51 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
53 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝑁 ∈
(ℤ≥‘(𝐺‘1))) |
54 | | elfzuzb 12630 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘1) ∈ (𝑀...𝑁) ↔ ((𝐺‘1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1)))) |
55 | 52, 53, 54 | sylanbrc 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈ (𝑀...𝑁)) |
56 | 5 | ffnd 6280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺 Fn ℕ) |
57 | | elpreima 6587 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 Fn ℕ → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
59 | 48, 55, 58 | mpbir2and 706 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
(◡𝐺 “ (𝑀...𝑁))) |
60 | 59 | ne0d 4152 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
61 | | nnssre 11355 |
. . . . . . . . . . . . . 14
⊢ ℕ
⊆ ℝ |
62 | 6, 61 | syl6ss 3840 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ) |
63 | | fisupcl 8645 |
. . . . . . . . . . . . 13
⊢ (( <
Or ℝ ∧ ((◡𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ)) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁))) |
64 | 12, 46, 60, 62, 63 | syl13anc 1497 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁))) |
65 | 6, 64 | sseldd 3829 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ) |
66 | 65 | nnzd 11810 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℤ) |
67 | | elfz5 12628 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘1) ∧ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℤ) →
(𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
68 | 10, 66, 67 | syl2anr 592 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
69 | | elpreima 6587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 Fn ℕ → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)))) |
70 | 56, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)))) |
71 | 64, 70 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ ∧
(𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁))) |
72 | 71 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁)) |
73 | | elfzle2 12639 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ (𝑀...𝑁) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
75 | 74 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) |
76 | | uzssz 11989 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
77 | 22, 76 | eqsstri 3861 |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 ⊆
ℤ |
78 | | zssre 11712 |
. . . . . . . . . . . . . . . 16
⊢ ℤ
⊆ ℝ |
79 | 77, 78 | sstri 3837 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 ⊆
ℝ |
80 | 5 | ffvelrnda 6609 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍) |
81 | 79, 80 | sseldi 3826 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ ℝ) |
82 | 5, 65 | ffvelrnd 6610 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍) |
83 | 82 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ 𝑍) |
84 | 79, 83 | sseldi 3826 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈
ℝ) |
85 | | eluzelz 11979 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘(𝐺‘1)) → 𝑁 ∈ ℤ) |
86 | 85 | ad2antlr 720 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈
ℤ) |
87 | 78, 86 | sseldi 3826 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑁 ∈
ℝ) |
88 | | letr 10451 |
. . . . . . . . . . . . . 14
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∈ ℝ ∧
𝑁 ∈ ℝ) →
(((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺‘𝑥) ≤ 𝑁)) |
89 | 81, 84, 87, 88 | syl3anc 1496 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ∧ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ≤ 𝑁) → (𝐺‘𝑥) ≤ 𝑁)) |
90 | 75, 89 | mpan2d 687 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) → (𝐺‘𝑥) ≤ 𝑁)) |
91 | 31 | ad2antrr 719 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ,
(𝐺 “
ℕ))) |
92 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ
⊆ ℝ) |
93 | | ressxr 10401 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* |
94 | 92, 93 | syl6ss 3840 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ℕ
⊆ ℝ*) |
95 | | imassrn 5719 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 “ ℕ) ⊆ ran
𝐺 |
96 | 4 | ad2antrr 719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍) |
97 | 96 | frnd 6286 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ran
𝐺 ⊆ 𝑍) |
98 | 95, 97 | syl5ss 3839 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ 𝑍) |
99 | 98, 79 | syl6ss 3840 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ) |
100 | 99, 93 | syl6ss 3840 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ*) |
101 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈
ℕ) |
102 | 65 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) →
sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ) |
103 | | leisorel 13534 |
. . . . . . . . . . . . 13
⊢ ((𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) ∧
(ℕ ⊆ ℝ* ∧ (𝐺 “ ℕ) ⊆
ℝ*) ∧ (𝑥 ∈ ℕ ∧ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈ ℕ)) →
(𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )))) |
104 | 91, 94, 100, 101, 102, 103 | syl122anc 1504 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ (𝐺‘𝑥) ≤ (𝐺‘sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )))) |
105 | 80, 22 | syl6eleq 2917 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ≥‘𝑀)) |
106 | | elfz5 12628 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑥) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...𝑁) ↔ (𝐺‘𝑥) ≤ 𝑁)) |
107 | 105, 86, 106 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...𝑁) ↔ (𝐺‘𝑥) ≤ 𝑁)) |
108 | 90, 104, 107 | 3imtr4d 286 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) → (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
109 | | elpreima 6587 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn ℕ → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...𝑁)))) |
110 | 109 | baibd 537 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn ℕ ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
111 | 56, 110 | sylan 577 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) ↔ (𝐺‘𝑥) ∈ (𝑀...𝑁))) |
112 | 108, 111 | sylibrd 251 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) → 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
113 | | fimaxre2 11300 |
. . . . . . . . . . . . 13
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) |
114 | 62, 46, 113 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) |
115 | | suprub 11315 |
. . . . . . . . . . . . 13
⊢ ((((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) ∧ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁))) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
116 | 115 | ex 403 |
. . . . . . . . . . . 12
⊢ (((◡𝐺 “ (𝑀...𝑁)) ⊆ ℝ ∧ (◡𝐺 “ (𝑀...𝑁)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (◡𝐺 “ (𝑀...𝑁))𝑦 ≤ 𝑥) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
117 | 62, 60, 114, 116 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
118 | 117 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)) → 𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) |
119 | 112, 118 | impbid 204 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
120 | 68, 119 | bitrd 271 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
121 | 120 | ex 403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ ℕ → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁))))) |
122 | 2, 7, 121 | pm5.21ndd 371 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑥 ∈ (1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) ↔ 𝑥 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
123 | 122 | eqrdv 2824 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) = (◡𝐺 “ (𝑀...𝑁))) |
124 | 123 | fveq2d 6438 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) =
(♯‘(◡𝐺 “ (𝑀...𝑁)))) |
125 | 65 | nnnn0d 11679 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ0) |
126 | | hashfz1 13427 |
. . . . 5
⊢
(sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) ∈
ℕ0 → (♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
127 | 125, 126 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ))) = sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) |
128 | | hashen 13428 |
. . . . . 6
⊢ (((◡𝐺 “ (𝑀...𝑁)) ∈ Fin ∧ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ∈ Fin) →
((♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
129 | 46, 20, 128 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
((♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (◡𝐺 “ (𝑀...𝑁)) ≈ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
130 | 44, 129 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(◡𝐺 “ (𝑀...𝑁))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
131 | 124, 127,
130 | 3eqtr3d 2870 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < ) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
132 | 131 | oveq2d 6922 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...sup((◡𝐺 “ (𝑀...𝑁)), ℝ, < )) =
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) |
133 | 132, 123 | eqtr3d 2864 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁))) |