Metamath Proof Explorer


Theorem isercolllem2

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z 𝑍 = ( ℤ𝑀 )
isercoll.m ( 𝜑𝑀 ∈ ℤ )
isercoll.g ( 𝜑𝐺 : ℕ ⟶ 𝑍 )
isercoll.i ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐺𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
Assertion isercolllem2 ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ... ( ♯ ‘ ( 𝐺 “ ( 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( 𝐺 “ ( 𝑀 ... 𝑁 ) ) )

Proof

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 ... ( ♯ ‘ ( 𝐺 “ ( 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( 𝐺 “ ( 𝑀 ... 𝑁 ) ) )