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 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
80 8 64 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ 𝑍 )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ 𝑍 )
82 77 81 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ sup ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ℝ , < ) ) ∈ ℝ )
83 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) → 𝑁 ∈ ℤ )
84 83 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℤ )
85 76 84 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 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 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )