Metamath Proof Explorer


Theorem isercolllem2

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

Ref Expression
Hypotheses isercoll.z
|- Z = ( ZZ>= ` M )
isercoll.m
|- ( ph -> M e. ZZ )
isercoll.g
|- ( ph -> G : NN --> Z )
isercoll.i
|- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
Assertion isercolllem2
|- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )

Proof

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