Step |
Hyp |
Ref |
Expression |
1 |
|
isercoll.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
isercoll.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
isercoll.g |
⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 ) |
4 |
|
isercoll.i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) |
5 |
|
elfznn |
⊢ ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) → 𝑥 ∈ ℕ ) |
6 |
5
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) → 𝑥 ∈ ℕ ) ) |
7 |
|
cnvimass |
⊢ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ dom 𝐺 |
8 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝐺 : ℕ ⟶ 𝑍 ) |
9 |
7 8
|
fssdm |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℕ ) |
10 |
9
|
sseld |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ ℕ ) ) |
11 |
|
id |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ ) |
12 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
13 |
11 12
|
eleqtrdi |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) |
14 |
|
ltso |
⊢ < Or ℝ |
15 |
14
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → < Or ℝ ) |
16 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑀 ... 𝑁 ) ∈ Fin ) |
17 |
|
ffun |
⊢ ( 𝐺 : ℕ ⟶ 𝑍 → Fun 𝐺 ) |
18 |
|
funimacnv |
⊢ ( Fun 𝐺 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ) |
19 |
8 17 18
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ) |
20 |
|
inss1 |
⊢ ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ⊆ ( 𝑀 ... 𝑁 ) |
21 |
19 20
|
eqsstrdi |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ⊆ ( 𝑀 ... 𝑁 ) ) |
22 |
16 21
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ∈ Fin ) |
23 |
|
ssid |
⊢ ℕ ⊆ ℕ |
24 |
1 2 3 4
|
isercolllem1 |
⊢ ( ( 𝜑 ∧ ℕ ⊆ ℕ ) → ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) |
25 |
23 24
|
mpan2 |
⊢ ( 𝜑 → ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) |
26 |
|
ffn |
⊢ ( 𝐺 : ℕ ⟶ 𝑍 → 𝐺 Fn ℕ ) |
27 |
|
fnresdm |
⊢ ( 𝐺 Fn ℕ → ( 𝐺 ↾ ℕ ) = 𝐺 ) |
28 |
|
isoeq1 |
⊢ ( ( 𝐺 ↾ ℕ ) = 𝐺 → ( ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ↔ 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) ) |
29 |
3 26 27 28
|
4syl |
⊢ ( 𝜑 → ( ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ↔ 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) ) |
30 |
25 29
|
mpbid |
⊢ ( 𝜑 → 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) |
31 |
|
isof1o |
⊢ ( 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) → 𝐺 : ℕ –1-1-onto→ ( 𝐺 “ ℕ ) ) |
32 |
|
f1ocnv |
⊢ ( 𝐺 : ℕ –1-1-onto→ ( 𝐺 “ ℕ ) → ◡ 𝐺 : ( 𝐺 “ ℕ ) –1-1-onto→ ℕ ) |
33 |
|
f1ofun |
⊢ ( ◡ 𝐺 : ( 𝐺 “ ℕ ) –1-1-onto→ ℕ → Fun ◡ 𝐺 ) |
34 |
30 31 32 33
|
4syl |
⊢ ( 𝜑 → Fun ◡ 𝐺 ) |
35 |
|
df-f1 |
⊢ ( 𝐺 : ℕ –1-1→ 𝑍 ↔ ( 𝐺 : ℕ ⟶ 𝑍 ∧ Fun ◡ 𝐺 ) ) |
36 |
3 34 35
|
sylanbrc |
⊢ ( 𝜑 → 𝐺 : ℕ –1-1→ 𝑍 ) |
37 |
36
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝐺 : ℕ –1-1→ 𝑍 ) |
38 |
|
nnex |
⊢ ℕ ∈ V |
39 |
|
ssexg |
⊢ ( ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℕ ∧ ℕ ∈ V ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ V ) |
40 |
9 38 39
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ V ) |
41 |
|
f1imaeng |
⊢ ( ( 𝐺 : ℕ –1-1→ 𝑍 ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℕ ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ V ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
42 |
37 9 40 41
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
43 |
42
|
ensymd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≈ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
44 |
|
enfii |
⊢ ( ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ∈ Fin ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≈ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ Fin ) |
45 |
22 43 44
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ Fin ) |
46 |
|
1nn |
⊢ 1 ∈ ℕ |
47 |
46
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 1 ∈ ℕ ) |
48 |
|
ffvelrn |
⊢ ( ( 𝐺 : ℕ ⟶ 𝑍 ∧ 1 ∈ ℕ ) → ( 𝐺 ‘ 1 ) ∈ 𝑍 ) |
49 |
3 46 48
|
sylancl |
⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ 𝑍 ) |
50 |
49 1
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
51 |
50
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
52 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) |
53 |
|
elfzuzb |
⊢ ( ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ) |
54 |
51 52 53
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ) |
55 |
8
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝐺 Fn ℕ ) |
56 |
|
elpreima |
⊢ ( 𝐺 Fn ℕ → ( 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 1 ∈ ℕ ∧ ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
57 |
55 56
|
syl |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 1 ∈ ℕ ∧ ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
58 |
47 54 57
|
mpbir2and |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
59 |
58
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≠ ∅ ) |
60 |
|
nnssre |
⊢ ℕ ⊆ ℝ |
61 |
9 60
|
sstrdi |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℝ ) |
62 |
|
fisupcl |
⊢ ( ( < Or ℝ ∧ ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ Fin ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≠ ∅ ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℝ ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
63 |
15 45 59 61 62
|
syl13anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
64 |
9 63
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ) |
65 |
64
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℤ ) |
66 |
|
elfz5 |
⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) ∧ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℤ ) → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ↔ 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) |
67 |
13 65 66
|
syl2anr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ↔ 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) |
68 |
|
elpreima |
⊢ ( 𝐺 Fn ℕ → ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
69 |
55 68
|
syl |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
70 |
63 69
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ( 𝑀 ... 𝑁 ) ) ) |
71 |
|
elfzle2 |
⊢ ( ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ≤ 𝑁 ) |
72 |
70 71
|
simpl2im |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ≤ 𝑁 ) |
73 |
72
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ≤ 𝑁 ) |
74 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
75 |
1 74
|
eqsstri |
⊢ 𝑍 ⊆ ℤ |
76 |
|
zssre |
⊢ ℤ ⊆ ℝ |
77 |
75 76
|
sstri |
⊢ 𝑍 ⊆ ℝ |
78 |
8
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑍 ) |
79 |
77 78
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) |
80 |
8 64
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ 𝑍 ) |
81 |
80
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ 𝑍 ) |
82 |
77 81
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ℝ ) |
83 |
|
eluzelz |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) → 𝑁 ∈ ℤ ) |
84 |
83
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℤ ) |
85 |
76 84
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℝ ) |
86 |
|
letr |
⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ≤ 𝑁 ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝑁 ) ) |
87 |
79 82 85 86
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∧ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ≤ 𝑁 ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝑁 ) ) |
88 |
73 87
|
mpan2d |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝑁 ) ) |
89 |
30
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) |
90 |
60
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ℕ ⊆ ℝ ) |
91 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
92 |
90 91
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ℕ ⊆ ℝ* ) |
93 |
|
imassrn |
⊢ ( 𝐺 “ ℕ ) ⊆ ran 𝐺 |
94 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝐺 : ℕ ⟶ 𝑍 ) |
95 |
94
|
frnd |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ran 𝐺 ⊆ 𝑍 ) |
96 |
93 95
|
sstrid |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 “ ℕ ) ⊆ 𝑍 ) |
97 |
96 77
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 “ ℕ ) ⊆ ℝ ) |
98 |
97 91
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 “ ℕ ) ⊆ ℝ* ) |
99 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ ) |
100 |
64
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ) |
101 |
|
leisorel |
⊢ ( ( 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ∧ ( ℕ ⊆ ℝ* ∧ ( 𝐺 “ ℕ ) ⊆ ℝ* ) ∧ ( 𝑥 ∈ ℕ ∧ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ ) ) → ( 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) ) |
102 |
89 92 98 99 100 101
|
syl122anc |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) ) |
103 |
78 1
|
eleqtrdi |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
104 |
|
elfz5 |
⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ 𝑁 ) ) |
105 |
103 84 104
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ 𝑁 ) ) |
106 |
88 102 105
|
3imtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ) ) |
107 |
|
elpreima |
⊢ ( 𝐺 Fn ℕ → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
108 |
107
|
baibd |
⊢ ( ( 𝐺 Fn ℕ ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ) ) |
109 |
55 108
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ) ) |
110 |
106 109
|
sylibrd |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) → 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
111 |
|
fimaxre2 |
⊢ ( ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℝ ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) 𝑦 ≤ 𝑥 ) |
112 |
61 45 111
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) 𝑦 ≤ 𝑥 ) |
113 |
|
suprub |
⊢ ( ( ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℝ ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) → 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) |
114 |
113
|
ex |
⊢ ( ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℝ ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) 𝑦 ≤ 𝑥 ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) → 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) |
115 |
61 59 112 114
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) → 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) |
116 |
115
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) → 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) |
117 |
110 116
|
impbid |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ↔ 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
118 |
67 117
|
bitrd |
⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ↔ 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
119 |
118
|
ex |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑥 ∈ ℕ → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ↔ 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) |
120 |
6 10 119
|
pm5.21ndd |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑥 ∈ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ↔ 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
121 |
120
|
eqrdv |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |
122 |
121
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ♯ ‘ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) = ( ♯ ‘ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) |
123 |
64
|
nnnn0d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ0 ) |
124 |
|
hashfz1 |
⊢ ( sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) = sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) |
125 |
123 124
|
syl |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ♯ ‘ ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ) = sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) |
126 |
|
hashen |
⊢ ( ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ∈ Fin ∧ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ↔ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≈ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) |
127 |
45 22 126
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( ♯ ‘ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ↔ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≈ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) |
128 |
43 127
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ♯ ‘ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) |
129 |
122 125 128
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) |
130 |
129
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ... sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) = ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) |
131 |
130 121
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) |