Metamath Proof Explorer

Theorem fdc

Description: Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010)

Ref Expression
Hypotheses fdc.1 
|- A e. _V
fdc.2 
|- M e. ZZ
fdc.3 
|- Z = ( ZZ>= ` M )
fdc.4 
|- N = ( M + 1 )
fdc.5 
|- ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )
fdc.6 
|- ( b = ( f ` k ) -> ( ps <-> ch ) )
fdc.7 
|- ( a = ( f ` n ) -> ( th <-> ta ) )
fdc.8 
|- ( et -> C e. A )
fdc.9 
|- ( et -> R Fr A )
fdc.10 
|- ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )
fdc.11 
|- ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )
Assertion fdc 
|- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )

Proof

Step Hyp Ref Expression
1 fdc.1 
 |-  A e. _V
2 fdc.2 
 |-  M e. ZZ
3 fdc.3 
 |-  Z = ( ZZ>= ` M )
4 fdc.4 
 |-  N = ( M + 1 )
5 fdc.5 
 |-  ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )
6 fdc.6 
 |-  ( b = ( f ` k ) -> ( ps <-> ch ) )
7 fdc.7 
 |-  ( a = ( f ` n ) -> ( th <-> ta ) )
8 fdc.8 
 |-  ( et -> C e. A )
9 fdc.9 
 |-  ( et -> R Fr A )
10 fdc.10 
 |-  ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )
11 fdc.11 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )
12 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
13 2 12 ax-mp 
 |-  M e. ( ZZ>= ` M )
14 13 3 eleqtrri 
 |-  M e. Z
15 eqid 
 |-  { <. M , a >. } = { <. M , a >. }
16 2 elexi 
 |-  M e. _V
17 vex 
 |-  a e. _V
18 16 17 fsn 
 |-  ( { <. M , a >. } : { M } --> { a } <-> { <. M , a >. } = { <. M , a >. } )
19 15 18 mpbir 
 |-  { <. M , a >. } : { M } --> { a }
20 snssi 
 |-  ( a e. A -> { a } C_ A )
21 fss 
 |-  ( ( { <. M , a >. } : { M } --> { a } /\ { a } C_ A ) -> { <. M , a >. } : { M } --> A )
22 19 20 21 sylancr 
 |-  ( a e. A -> { <. M , a >. } : { M } --> A )
23 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
24 2 23 ax-mp 
 |-  ( M ... M ) = { M }
25 24 feq2i 
 |-  ( { <. M , a >. } : ( M ... M ) --> A <-> { <. M , a >. } : { M } --> A )
26 22 25 sylibr 
 |-  ( a e. A -> { <. M , a >. } : ( M ... M ) --> A )
27 26 adantr 
 |-  ( ( a e. A /\ th ) -> { <. M , a >. } : ( M ... M ) --> A )
28 16 17 fvsn 
 |-  ( { <. M , a >. } ` M ) = a
29 28 a1i 
 |-  ( ( a e. A /\ th ) -> ( { <. M , a >. } ` M ) = a )
30 simpr 
 |-  ( ( a e. A /\ th ) -> th )
31 snex 
 |-  { <. M , a >. } e. _V
32 feq1 
 |-  ( f = { <. M , a >. } -> ( f : ( M ... M ) --> A <-> { <. M , a >. } : ( M ... M ) --> A ) )
33 fveq1 
 |-  ( f = { <. M , a >. } -> ( f ` M ) = ( { <. M , a >. } ` M ) )
34 33 eqeq1d 
 |-  ( f = { <. M , a >. } -> ( ( f ` M ) = a <-> ( { <. M , a >. } ` M ) = a ) )
35 33 28 eqtrdi 
 |-  ( f = { <. M , a >. } -> ( f ` M ) = a )
36 sbceq2a 
 |-  ( ( f ` M ) = a -> ( [. ( f ` M ) / a ]. th <-> th ) )
37 35 36 syl 
 |-  ( f = { <. M , a >. } -> ( [. ( f ` M ) / a ]. th <-> th ) )
38 34 37 anbi12d 
 |-  ( f = { <. M , a >. } -> ( ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) <-> ( ( { <. M , a >. } ` M ) = a /\ th ) ) )
39 32 38 anbi12d 
 |-  ( f = { <. M , a >. } -> ( ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) <-> ( { <. M , a >. } : ( M ... M ) --> A /\ ( ( { <. M , a >. } ` M ) = a /\ th ) ) ) )
40 31 39 spcev 
 |-  ( ( { <. M , a >. } : ( M ... M ) --> A /\ ( ( { <. M , a >. } ` M ) = a /\ th ) ) -> E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
41 27 29 30 40 syl12anc 
 |-  ( ( a e. A /\ th ) -> E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
42 oveq2 
 |-  ( n = M -> ( M ... n ) = ( M ... M ) )
43 42 feq2d 
 |-  ( n = M -> ( f : ( M ... n ) --> A <-> f : ( M ... M ) --> A ) )
44 fvex 
 |-  ( f ` n ) e. _V
45 44 7 sbcie 
 |-  ( [. ( f ` n ) / a ]. th <-> ta )
46 fveq2 
 |-  ( n = M -> ( f ` n ) = ( f ` M ) )
47 46 sbceq1d 
 |-  ( n = M -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` M ) / a ]. th ) )
48 45 47 bitr3id 
 |-  ( n = M -> ( ta <-> [. ( f ` M ) / a ]. th ) )
49 48 anbi2d 
 |-  ( n = M -> ( ( ( f ` M ) = a /\ ta ) <-> ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
50 oveq2 
 |-  ( n = M -> ( N ... n ) = ( N ... M ) )
51 4 oveq1i 
 |-  ( N ... M ) = ( ( M + 1 ) ... M )
52 2 zrei 
 |-  M e. RR
53 52 ltp1i 
 |-  M < ( M + 1 )
54 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
55 2 54 ax-mp 
 |-  ( M + 1 ) e. ZZ
56 fzn 
 |-  ( ( ( M + 1 ) e. ZZ /\ M e. ZZ ) -> ( M < ( M + 1 ) <-> ( ( M + 1 ) ... M ) = (/) ) )
57 55 2 56 mp2an 
 |-  ( M < ( M + 1 ) <-> ( ( M + 1 ) ... M ) = (/) )
58 53 57 mpbi 
 |-  ( ( M + 1 ) ... M ) = (/)
59 51 58 eqtri 
 |-  ( N ... M ) = (/)
60 50 59 eqtrdi 
 |-  ( n = M -> ( N ... n ) = (/) )
61 60 raleqdv 
 |-  ( n = M -> ( A. k e. ( N ... n ) ch <-> A. k e. (/) ch ) )
62 43 49 61 3anbi123d 
 |-  ( n = M -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) /\ A. k e. (/) ch ) ) )
63 ral0 
 |-  A. k e. (/) ch
64 df-3an 
 |-  ( ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) /\ A. k e. (/) ch ) <-> ( ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) /\ A. k e. (/) ch ) )
65 63 64 mpbiran2 
 |-  ( ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) /\ A. k e. (/) ch ) <-> ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
66 62 65 bitrdi 
 |-  ( n = M -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) ) )
67 66 exbidv 
 |-  ( n = M -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) ) )
68 67 rspcev 
 |-  ( ( M e. Z /\ E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
69 14 41 68 sylancr 
 |-  ( ( a e. A /\ th ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
70 69 adantll 
 |-  ( ( ( et /\ a e. A ) /\ th ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
71 70 a1d 
 |-  ( ( ( et /\ a e. A ) /\ th ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
72 breq1 
 |-  ( d = b -> ( d R a <-> b R a ) )
73 72 rspcev 
 |-  ( ( b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) /\ b R a ) -> E. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) d R a )
74 73 expcom 
 |-  ( b R a -> ( b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> E. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) d R a ) )
75 11 74 syl 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> E. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) d R a ) )
76 dfrex2 
 |-  ( E. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) d R a <-> -. A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a )
77 75 76 imbitrdi 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> -. A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a ) )
78 77 con2d 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> -. b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) )
79 eldif 
 |-  ( b e. ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) <-> ( b e. A /\ -. b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) )
80 79 simplbi2 
 |-  ( b e. A -> ( -. b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> b e. ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) ) )
81 ssrab2 
 |-  { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } C_ A
82 dfss4 
 |-  ( { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } C_ A <-> ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) = { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } )
83 81 82 mpbi 
 |-  ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) = { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) }
84 83 eleq2i 
 |-  ( b e. ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) <-> b e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } )
85 eqeq2 
 |-  ( c = b -> ( ( f ` M ) = c <-> ( f ` M ) = b ) )
86 85 anbi1d 
 |-  ( c = b -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = b /\ ta ) ) )
87 86 3anbi2d 
 |-  ( c = b -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
88 87 exbidv 
 |-  ( c = b -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
89 88 rexbidv 
 |-  ( c = b -> ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
90 89 elrab3 
 |-  ( b e. A -> ( b e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
91 84 90 bitrid 
 |-  ( b e. A -> ( b e. ( A \ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
92 80 91 sylibd 
 |-  ( b e. A -> ( -. b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
93 92 ad2antll 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( -. b e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
94 oveq2 
 |-  ( n = m -> ( M ... n ) = ( M ... m ) )
95 94 feq2d 
 |-  ( n = m -> ( f : ( M ... n ) --> A <-> f : ( M ... m ) --> A ) )
96 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
97 96 sbceq1d 
 |-  ( n = m -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` m ) / a ]. th ) )
98 45 97 bitr3id 
 |-  ( n = m -> ( ta <-> [. ( f ` m ) / a ]. th ) )
99 98 anbi2d 
 |-  ( n = m -> ( ( ( f ` M ) = b /\ ta ) <-> ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) ) )
100 oveq2 
 |-  ( n = m -> ( N ... n ) = ( N ... m ) )
101 100 raleqdv 
 |-  ( n = m -> ( A. k e. ( N ... n ) ch <-> A. k e. ( N ... m ) ch ) )
102 95 99 101 3anbi123d 
 |-  ( n = m -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) ) )
103 102 exbidv 
 |-  ( n = m -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) ) )
104 103 cbvrexvw 
 |-  ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. m e. Z E. f ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) )
105 feq1 
 |-  ( f = g -> ( f : ( M ... m ) --> A <-> g : ( M ... m ) --> A ) )
106 fveq1 
 |-  ( f = g -> ( f ` M ) = ( g ` M ) )
107 106 eqeq1d 
 |-  ( f = g -> ( ( f ` M ) = b <-> ( g ` M ) = b ) )
108 fveq1 
 |-  ( f = g -> ( f ` m ) = ( g ` m ) )
109 108 sbceq1d 
 |-  ( f = g -> ( [. ( f ` m ) / a ]. th <-> [. ( g ` m ) / a ]. th ) )
110 107 109 anbi12d 
 |-  ( f = g -> ( ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) <-> ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) ) )
111 fvex 
 |-  ( f ` ( k - 1 ) ) e. _V
112 5 sbcbidv 
 |-  ( a = ( f ` ( k - 1 ) ) -> ( [. ( f ` k ) / b ]. ph <-> [. ( f ` k ) / b ]. ps ) )
113 111 112 sbcie 
 |-  ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> [. ( f ` k ) / b ]. ps )
114 fvex 
 |-  ( f ` k ) e. _V
115 114 6 sbcie 
 |-  ( [. ( f ` k ) / b ]. ps <-> ch )
116 113 115 bitri 
 |-  ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> ch )
117 fveq1 
 |-  ( f = g -> ( f ` ( k - 1 ) ) = ( g ` ( k - 1 ) ) )
118 fveq1 
 |-  ( f = g -> ( f ` k ) = ( g ` k ) )
119 118 sbceq1d 
 |-  ( f = g -> ( [. ( f ` k ) / b ]. ph <-> [. ( g ` k ) / b ]. ph ) )
120 117 119 sbceqbid 
 |-  ( f = g -> ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
121 116 120 bitr3id 
 |-  ( f = g -> ( ch <-> [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
122 121 ralbidv 
 |-  ( f = g -> ( A. k e. ( N ... m ) ch <-> A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
123 105 110 122 3anbi123d 
 |-  ( f = g -> ( ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) <-> ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) )
124 123 cbvexvw 
 |-  ( E. f ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) <-> E. g ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
125 124 rexbii 
 |-  ( E. m e. Z E. f ( f : ( M ... m ) --> A /\ ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) /\ A. k e. ( N ... m ) ch ) <-> E. m e. Z E. g ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
126 104 125 bitri 
 |-  ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. m e. Z E. g ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
127 3 peano2uzs 
 |-  ( m e. Z -> ( m + 1 ) e. Z )
128 127 ad2antlr 
 |-  ( ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> ( m + 1 ) e. Z )
129 sbceq2a 
 |-  ( d = b -> ( [. d / b ]. ph <-> ph ) )
130 129 anbi1d 
 |-  ( d = b -> ( ( [. d / b ]. ph /\ a e. A ) <-> ( ph /\ a e. A ) ) )
131 130 anbi1d 
 |-  ( d = b -> ( ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) <-> ( ( ph /\ a e. A ) /\ m e. Z ) ) )
132 eqeq2 
 |-  ( d = b -> ( ( g ` M ) = d <-> ( g ` M ) = b ) )
133 132 anbi1d 
 |-  ( d = b -> ( ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) <-> ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) ) )
134 133 3anbi2d 
 |-  ( d = b -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) <-> ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) )
135 134 imbi1d 
 |-  ( d = b -> ( ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) <-> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) )
136 131 135 imbi12d 
 |-  ( d = b -> ( ( ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) <-> ( ( ( ph /\ a e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) ) )
137 sbceq2a 
 |-  ( c = a -> ( [. c / a ]. [. d / b ]. ph <-> [. d / b ]. ph ) )
138 eleq1 
 |-  ( c = a -> ( c e. A <-> a e. A ) )
139 137 138 anbi12d 
 |-  ( c = a -> ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) <-> ( [. d / b ]. ph /\ a e. A ) ) )
140 139 anbi1d 
 |-  ( c = a -> ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) <-> ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) ) )
141 eqeq2 
 |-  ( c = a -> ( ( f ` M ) = c <-> ( f ` M ) = a ) )
142 141 anbi1d 
 |-  ( c = a -> ( ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) <-> ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) ) )
143 142 3anbi2d 
 |-  ( c = a -> ( ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) <-> ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
144 143 exbidv 
 |-  ( c = a -> ( E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) <-> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
145 144 imbi2d 
 |-  ( c = a -> ( ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) <-> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) )
146 140 145 imbi12d 
 |-  ( c = a -> ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) <-> ( ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) ) ) )
147 peano2uz 
 |-  ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( ZZ>= ` M ) )
148 147 3 eleq2s 
 |-  ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` M ) )
149 elfzp12 
 |-  ( ( m + 1 ) e. ( ZZ>= ` M ) -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
150 148 149 syl 
 |-  ( m e. Z -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
151 150 ad2antlr 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
152 iftrue 
 |-  ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = c )
153 152 eleq1d 
 |-  ( x = M -> ( if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A <-> c e. A ) )
154 153 biimprcd 
 |-  ( c e. A -> ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
155 154 ad2antrr 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
156 1re 
 |-  1 e. RR
157 52 156 readdcli 
 |-  ( M + 1 ) e. RR
158 52 157 ltnlei 
 |-  ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M )
159 53 158 mpbi 
 |-  -. ( M + 1 ) <_ M
160 eleq1 
 |-  ( x = M -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) <-> M e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
161 elfzle1 
 |-  ( M e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( M + 1 ) <_ M )
162 160 161 biimtrdi 
 |-  ( x = M -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( M + 1 ) <_ M ) )
163 162 com12 
 |-  ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x = M -> ( M + 1 ) <_ M ) )
164 159 163 mtoi 
 |-  ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> -. x = M )
165 164 adantl 
 |-  ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> -. x = M )
166 165 iffalsed 
 |-  ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = ( g ` ( x - 1 ) ) )
167 elfzelz 
 |-  ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> x e. ZZ )
168 167 adantl 
 |-  ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> x e. ZZ )
169 eluzelz 
 |-  ( m e. ( ZZ>= ` M ) -> m e. ZZ )
170 169 3 eleq2s 
 |-  ( m e. Z -> m e. ZZ )
171 170 peano2zd 
 |-  ( m e. Z -> ( m + 1 ) e. ZZ )
172 1z 
 |-  1 e. ZZ
173 fzsubel 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ ( x e. ZZ /\ 1 e. ZZ ) ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) <-> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
174 173 biimpd 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ ( x e. ZZ /\ 1 e. ZZ ) ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
175 172 174 mpanr2 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ x e. ZZ ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
176 55 175 mpanl1 
 |-  ( ( ( m + 1 ) e. ZZ /\ x e. ZZ ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
177 176 ex 
 |-  ( ( m + 1 ) e. ZZ -> ( x e. ZZ -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
178 171 177 syl 
 |-  ( m e. Z -> ( x e. ZZ -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
179 178 com23 
 |-  ( m e. Z -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x e. ZZ -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
180 179 imp 
 |-  ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x e. ZZ -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
181 168 180 mpd 
 |-  ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) )
182 52 recni 
 |-  M e. CC
183 ax-1cn 
 |-  1 e. CC
184 182 183 pncan3oi 
 |-  ( ( M + 1 ) - 1 ) = M
185 184 a1i 
 |-  ( m e. Z -> ( ( M + 1 ) - 1 ) = M )
186 170 zcnd 
 |-  ( m e. Z -> m e. CC )
187 pncan 
 |-  ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
188 186 183 187 sylancl 
 |-  ( m e. Z -> ( ( m + 1 ) - 1 ) = m )
189 185 188 oveq12d 
 |-  ( m e. Z -> ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( M ... m ) )
190 189 adantr 
 |-  ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( M ... m ) )
191 181 190 eleqtrd 
 |-  ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x - 1 ) e. ( M ... m ) )
192 ffvelcdm 
 |-  ( ( g : ( M ... m ) --> A /\ ( x - 1 ) e. ( M ... m ) ) -> ( g ` ( x - 1 ) ) e. A )
193 191 192 sylan2 
 |-  ( ( g : ( M ... m ) --> A /\ ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) -> ( g ` ( x - 1 ) ) e. A )
194 193 anassrs 
 |-  ( ( ( g : ( M ... m ) --> A /\ m e. Z ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( g ` ( x - 1 ) ) e. A )
195 194 ancom1s 
 |-  ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( g ` ( x - 1 ) ) e. A )
196 166 195 eqeltrd 
 |-  ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A )
197 196 ex 
 |-  ( ( m e. Z /\ g : ( M ... m ) --> A ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
198 197 adantll 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
199 155 198 jaod 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
200 151 199 sylbid 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
201 200 ralrimiv 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> A. x e. ( M ... ( m + 1 ) ) if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A )
202 eqid 
 |-  ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) )
203 202 fmpt 
 |-  ( A. x e. ( M ... ( m + 1 ) ) if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A <-> ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A )
204 201 203 sylib 
 |-  ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A )
205 204 adantlll 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A )
206 205 3ad2antr1 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A )
207 eluzfz1 
 |-  ( ( m + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( m + 1 ) ) )
208 147 207 syl 
 |-  ( m e. ( ZZ>= ` M ) -> M e. ( M ... ( m + 1 ) ) )
209 208 3 eleq2s 
 |-  ( m e. Z -> M e. ( M ... ( m + 1 ) ) )
210 vex 
 |-  c e. _V
211 152 202 210 fvmpt 
 |-  ( M e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
212 209 211 syl 
 |-  ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
213 212 ad2antlr 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
214 eluzfz2 
 |-  ( ( m + 1 ) e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
215 147 214 syl 
 |-  ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
216 215 3 eleq2s 
 |-  ( m e. Z -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
217 eqeq1 
 |-  ( x = ( m + 1 ) -> ( x = M <-> ( m + 1 ) = M ) )
218 fvoveq1 
 |-  ( x = ( m + 1 ) -> ( g ` ( x - 1 ) ) = ( g ` ( ( m + 1 ) - 1 ) ) )
219 217 218 ifbieq2d 
 |-  ( x = ( m + 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) )
220 fvex 
 |-  ( g ` ( ( m + 1 ) - 1 ) ) e. _V
221 210 220 ifex 
 |-  if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) e. _V
222 219 202 221 fvmpt 
 |-  ( ( m + 1 ) e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) = if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) )
223 216 222 syl 
 |-  ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) = if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) )
224 eluzle 
 |-  ( m e. ( ZZ>= ` M ) -> M <_ m )
225 224 3 eleq2s 
 |-  ( m e. Z -> M <_ m )
226 zleltp1 
 |-  ( ( M e. ZZ /\ m e. ZZ ) -> ( M <_ m <-> M < ( m + 1 ) ) )
227 2 170 226 sylancr 
 |-  ( m e. Z -> ( M <_ m <-> M < ( m + 1 ) ) )
228 225 227 mpbid 
 |-  ( m e. Z -> M < ( m + 1 ) )
229 ltne 
 |-  ( ( M e. RR /\ M < ( m + 1 ) ) -> ( m + 1 ) =/= M )
230 52 228 229 sylancr 
 |-  ( m e. Z -> ( m + 1 ) =/= M )
231 230 neneqd 
 |-  ( m e. Z -> -. ( m + 1 ) = M )
232 231 iffalsed 
 |-  ( m e. Z -> if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) = ( g ` ( ( m + 1 ) - 1 ) ) )
233 188 fveq2d 
 |-  ( m e. Z -> ( g ` ( ( m + 1 ) - 1 ) ) = ( g ` m ) )
234 223 232 233 3eqtrd 
 |-  ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) = ( g ` m ) )
235 234 sbceq1d 
 |-  ( m e. Z -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th <-> [. ( g ` m ) / a ]. th ) )
236 235 biimpar 
 |-  ( ( m e. Z /\ [. ( g ` m ) / a ]. th ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th )
237 236 ad2ant2l 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th )
238 237 3ad2antr2 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th )
239 eluzp1p1 
 |-  ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
240 239 3 eleq2s 
 |-  ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
241 4 fveq2i 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` ( M + 1 ) )
242 240 241 eleqtrrdi 
 |-  ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` N ) )
243 elfzp12 
 |-  ( ( m + 1 ) e. ( ZZ>= ` N ) -> ( j e. ( N ... ( m + 1 ) ) <-> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) ) )
244 242 243 syl 
 |-  ( m e. Z -> ( j e. ( N ... ( m + 1 ) ) <-> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) ) )
245 244 biimpa 
 |-  ( ( m e. Z /\ j e. ( N ... ( m + 1 ) ) ) -> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
246 245 adantll 
 |-  ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ j e. ( N ... ( m + 1 ) ) ) -> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
247 246 adantlr 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ j e. ( N ... ( m + 1 ) ) ) -> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
248 oveq1 
 |-  ( j = N -> ( j - 1 ) = ( N - 1 ) )
249 4 oveq1i 
 |-  ( N - 1 ) = ( ( M + 1 ) - 1 )
250 249 184 eqtri 
 |-  ( N - 1 ) = M
251 248 250 eqtrdi 
 |-  ( j = N -> ( j - 1 ) = M )
252 251 fveq2d 
 |-  ( j = N -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) )
253 252 ad2antll 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) )
254 212 adantr 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
255 253 254 eqtrd 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = c )
256 4 eqeq2i 
 |-  ( j = N <-> j = ( M + 1 ) )
257 fveq2 
 |-  ( j = ( M + 1 ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) )
258 256 257 sylbi 
 |-  ( j = N -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) )
259 258 ad2antll 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) )
260 52 157 53 ltleii 
 |-  M <_ ( M + 1 )
261 eluz2 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( M + 1 ) e. ZZ /\ M <_ ( M + 1 ) ) )
262 2 55 260 261 mpbir3an 
 |-  ( M + 1 ) e. ( ZZ>= ` M )
263 fzss1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( ( M + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
264 262 263 ax-mp 
 |-  ( ( M + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
265 eluzfz1 
 |-  ( m e. ( ZZ>= ` M ) -> M e. ( M ... m ) )
266 265 3 eleq2s 
 |-  ( m e. Z -> M e. ( M ... m ) )
267 fzaddel 
 |-  ( ( ( M e. ZZ /\ m e. ZZ ) /\ ( M e. ZZ /\ 1 e. ZZ ) ) -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
268 2 172 267 mpanr12 
 |-  ( ( M e. ZZ /\ m e. ZZ ) -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
269 2 170 268 sylancr 
 |-  ( m e. Z -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
270 266 269 mpbid 
 |-  ( m e. Z -> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) )
271 264 270 sselid 
 |-  ( m e. Z -> ( M + 1 ) e. ( M ... ( m + 1 ) ) )
272 eqeq1 
 |-  ( x = ( M + 1 ) -> ( x = M <-> ( M + 1 ) = M ) )
273 oveq1 
 |-  ( x = ( M + 1 ) -> ( x - 1 ) = ( ( M + 1 ) - 1 ) )
274 273 184 eqtrdi 
 |-  ( x = ( M + 1 ) -> ( x - 1 ) = M )
275 274 fveq2d 
 |-  ( x = ( M + 1 ) -> ( g ` ( x - 1 ) ) = ( g ` M ) )
276 272 275 ifbieq2d 
 |-  ( x = ( M + 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( M + 1 ) = M , c , ( g ` M ) ) )
277 fvex 
 |-  ( g ` M ) e. _V
278 210 277 ifex 
 |-  if ( ( M + 1 ) = M , c , ( g ` M ) ) e. _V
279 276 202 278 fvmpt 
 |-  ( ( M + 1 ) e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = if ( ( M + 1 ) = M , c , ( g ` M ) ) )
280 271 279 syl 
 |-  ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = if ( ( M + 1 ) = M , c , ( g ` M ) ) )
281 52 53 gtneii 
 |-  ( M + 1 ) =/= M
282 ifnefalse 
 |-  ( ( M + 1 ) =/= M -> if ( ( M + 1 ) = M , c , ( g ` M ) ) = ( g ` M ) )
283 281 282 ax-mp 
 |-  if ( ( M + 1 ) = M , c , ( g ` M ) ) = ( g ` M )
284 280 283 eqtrdi 
 |-  ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = ( g ` M ) )
285 284 adantr 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = ( g ` M ) )
286 simprl 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( g ` M ) = d )
287 259 285 286 3eqtrd 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = d )
288 287 sbceq1d 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. d / b ]. ph ) )
289 255 288 sbceqbid 
 |-  ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. c / a ]. [. d / b ]. ph ) )
290 289 biimparc 
 |-  ( ( [. c / a ]. [. d / b ]. ph /\ ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
291 290 anassrs 
 |-  ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ j = N ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
292 291 anassrs 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( g ` M ) = d ) /\ j = N ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
293 292 adantlrr 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ j = N ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
294 elfzelz 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> j e. ZZ )
295 294 adantl 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ZZ )
296 4 55 eqeltri 
 |-  N e. ZZ
297 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
298 296 297 ax-mp 
 |-  ( N + 1 ) e. ZZ
299 fzsubel 
 |-  ( ( ( ( N + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) <-> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
300 299 biimpd 
 |-  ( ( ( ( N + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
301 172 300 mpanr2 
 |-  ( ( ( ( N + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) /\ j e. ZZ ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
302 301 ex 
 |-  ( ( ( N + 1 ) e. ZZ /\ ( m + 1 ) e. ZZ ) -> ( j e. ZZ -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
303 298 171 302 sylancr 
 |-  ( m e. Z -> ( j e. ZZ -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
304 303 com23 
 |-  ( m e. Z -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j e. ZZ -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
305 304 imp 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j e. ZZ -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
306 295 305 mpd 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) )
307 296 zrei 
 |-  N e. RR
308 307 recni 
 |-  N e. CC
309 308 183 pncan3oi 
 |-  ( ( N + 1 ) - 1 ) = N
310 309 a1i 
 |-  ( m e. Z -> ( ( N + 1 ) - 1 ) = N )
311 310 188 oveq12d 
 |-  ( m e. Z -> ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( N ... m ) )
312 311 adantr 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( N ... m ) )
313 306 312 eleqtrd 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( N ... m ) )
314 fvoveq1 
 |-  ( k = ( j - 1 ) -> ( g ` ( k - 1 ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
315 fveq2 
 |-  ( k = ( j - 1 ) -> ( g ` k ) = ( g ` ( j - 1 ) ) )
316 315 sbceq1d 
 |-  ( k = ( j - 1 ) -> ( [. ( g ` k ) / b ]. ph <-> [. ( g ` ( j - 1 ) ) / b ]. ph ) )
317 314 316 sbceqbid 
 |-  ( k = ( j - 1 ) -> ( [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph <-> [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph ) )
318 317 rspcva 
 |-  ( ( ( j - 1 ) e. ( N ... m ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph )
319 313 318 sylan 
 |-  ( ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph )
320 4 262 eqeltri 
 |-  N e. ( ZZ>= ` M )
321 fzss1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
322 320 321 ax-mp 
 |-  ( N ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
323 fzssp1 
 |-  ( N ... m ) C_ ( N ... ( m + 1 ) )
324 323 313 sselid 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( N ... ( m + 1 ) ) )
325 322 324 sselid 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( M ... ( m + 1 ) ) )
326 eqeq1 
 |-  ( x = ( j - 1 ) -> ( x = M <-> ( j - 1 ) = M ) )
327 fvoveq1 
 |-  ( x = ( j - 1 ) -> ( g ` ( x - 1 ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
328 326 327 ifbieq2d 
 |-  ( x = ( j - 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) )
329 fvex 
 |-  ( g ` ( ( j - 1 ) - 1 ) ) e. _V
330 210 329 ifex 
 |-  if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) e. _V
331 328 202 330 fvmpt 
 |-  ( ( j - 1 ) e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) )
332 325 331 syl 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) )
333 157 ltp1i 
 |-  ( M + 1 ) < ( ( M + 1 ) + 1 )
334 4 oveq1i 
 |-  ( N + 1 ) = ( ( M + 1 ) + 1 )
335 333 334 breqtrri 
 |-  ( M + 1 ) < ( N + 1 )
336 307 156 readdcli 
 |-  ( N + 1 ) e. RR
337 157 336 ltnlei 
 |-  ( ( M + 1 ) < ( N + 1 ) <-> -. ( N + 1 ) <_ ( M + 1 ) )
338 335 337 mpbi 
 |-  -. ( N + 1 ) <_ ( M + 1 )
339 294 zcnd 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> j e. CC )
340 subadd 
 |-  ( ( j e. CC /\ 1 e. CC /\ M e. CC ) -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
341 183 182 340 mp3an23 
 |-  ( j e. CC -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
342 339 341 syl 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
343 eqcom 
 |-  ( ( 1 + M ) = j <-> j = ( 1 + M ) )
344 183 182 addcomi 
 |-  ( 1 + M ) = ( M + 1 )
345 344 eqeq2i 
 |-  ( j = ( 1 + M ) <-> j = ( M + 1 ) )
346 343 345 bitri 
 |-  ( ( 1 + M ) = j <-> j = ( M + 1 ) )
347 eleq1 
 |-  ( j = ( M + 1 ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) <-> ( M + 1 ) e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
348 elfzle1 
 |-  ( ( M + 1 ) e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ ( M + 1 ) )
349 347 348 biimtrdi 
 |-  ( j = ( M + 1 ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ ( M + 1 ) ) )
350 349 com12 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j = ( M + 1 ) -> ( N + 1 ) <_ ( M + 1 ) ) )
351 346 350 biimtrid 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( 1 + M ) = j -> ( N + 1 ) <_ ( M + 1 ) ) )
352 342 351 sylbid 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( j - 1 ) = M -> ( N + 1 ) <_ ( M + 1 ) ) )
353 338 352 mtoi 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> -. ( j - 1 ) = M )
354 353 adantl 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> -. ( j - 1 ) = M )
355 354 iffalsed 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
356 332 355 eqtrd 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
357 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
358 fzss1 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ( N + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
359 320 357 358 mp2b 
 |-  ( ( N + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
360 simpr 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ( ( N + 1 ) ... ( m + 1 ) ) )
361 359 360 sselid 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ( M ... ( m + 1 ) ) )
362 eqeq1 
 |-  ( x = j -> ( x = M <-> j = M ) )
363 fvoveq1 
 |-  ( x = j -> ( g ` ( x - 1 ) ) = ( g ` ( j - 1 ) ) )
364 362 363 ifbieq2d 
 |-  ( x = j -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( j = M , c , ( g ` ( j - 1 ) ) ) )
365 fvex 
 |-  ( g ` ( j - 1 ) ) e. _V
366 210 365 ifex 
 |-  if ( j = M , c , ( g ` ( j - 1 ) ) ) e. _V
367 364 202 366 fvmpt 
 |-  ( j e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = if ( j = M , c , ( g ` ( j - 1 ) ) ) )
368 361 367 syl 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = if ( j = M , c , ( g ` ( j - 1 ) ) ) )
369 53 4 breqtrri 
 |-  M < N
370 307 ltp1i 
 |-  N < ( N + 1 )
371 52 307 336 lttri 
 |-  ( ( M < N /\ N < ( N + 1 ) ) -> M < ( N + 1 ) )
372 369 370 371 mp2an 
 |-  M < ( N + 1 )
373 52 336 ltnlei 
 |-  ( M < ( N + 1 ) <-> -. ( N + 1 ) <_ M )
374 372 373 mpbi 
 |-  -. ( N + 1 ) <_ M
375 eleq1 
 |-  ( j = M -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) <-> M e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
376 elfzle1 
 |-  ( M e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ M )
377 375 376 biimtrdi 
 |-  ( j = M -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ M ) )
378 377 com12 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j = M -> ( N + 1 ) <_ M ) )
379 374 378 mtoi 
 |-  ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> -. j = M )
380 379 adantl 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> -. j = M )
381 380 iffalsed 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> if ( j = M , c , ( g ` ( j - 1 ) ) ) = ( g ` ( j - 1 ) ) )
382 368 381 eqtrd 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = ( g ` ( j - 1 ) ) )
383 382 sbceq1d 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. ( g ` ( j - 1 ) ) / b ]. ph ) )
384 356 383 sbceqbid 
 |-  ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph ) )
385 384 biimpar 
 |-  ( ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) /\ [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
386 319 385 syldan 
 |-  ( ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
387 386 an32s 
 |-  ( ( ( m e. Z /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
388 387 adantlrl 
 |-  ( ( ( m e. Z /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
389 388 adantlll 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
390 293 389 jaodan 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
391 247 390 syldan 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) /\ j e. ( N ... ( m + 1 ) ) ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
392 391 ralrimiva 
 |-  ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> A. j e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph )
393 fvoveq1 
 |-  ( j = k -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) )
394 fveq2 
 |-  ( j = k -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) )
395 394 sbceq1d 
 |-  ( j = k -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
396 393 395 sbceqbid 
 |-  ( j = k -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
397 396 cbvralvw 
 |-  ( A. j e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) / b ]. ph <-> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph )
398 392 397 sylib 
 |-  ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph )
399 398 adantllr 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( ( g ` M ) = d /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph )
400 399 adantrlr 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph )
401 400 3adantr1 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph )
402 ovex 
 |-  ( M ... ( m + 1 ) ) e. _V
403 402 mptex 
 |-  ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) e. _V
404 feq1 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( f : ( M ... ( m + 1 ) ) --> A <-> ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A ) )
405 fveq1 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( f ` M ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) )
406 405 eqeq1d 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( ( f ` M ) = c <-> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c ) )
407 fveq1 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( f ` ( m + 1 ) ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) )
408 407 sbceq1d 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( [. ( f ` ( m + 1 ) ) / a ]. th <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th ) )
409 406 408 anbi12d 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) <-> ( ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c /\ [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th ) ) )
410 fveq1 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( f ` ( k - 1 ) ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) )
411 fveq1 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( f ` k ) = ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) )
412 411 sbceq1d 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( [. ( f ` k ) / b ]. ph <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
413 410 412 sbceqbid 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
414 116 413 bitr3id 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( ch <-> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
415 414 ralbidv 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( A. k e. ( N ... ( m + 1 ) ) ch <-> A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) )
416 404 409 415 3anbi123d 
 |-  ( f = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) -> ( ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) <-> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A /\ ( ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c /\ [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) ) )
417 403 416 spcev 
 |-  ( ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) : ( M ... ( m + 1 ) ) --> A /\ ( ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c /\ [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( k - 1 ) ) / a ]. [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) )
418 206 213 238 401 417 syl121anc 
 |-  ( ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) )
419 418 ex 
 |-  ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
420 146 419 chvarvv 
 |-  ( ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
421 136 420 chvarvv 
 |-  ( ( ( ph /\ a e. A ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
422 421 adantlrr 
 |-  ( ( ( ph /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
423 422 adantlll 
 |-  ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
424 423 imp 
 |-  ( ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) )
425 oveq2 
 |-  ( n = ( m + 1 ) -> ( M ... n ) = ( M ... ( m + 1 ) ) )
426 425 feq2d 
 |-  ( n = ( m + 1 ) -> ( f : ( M ... n ) --> A <-> f : ( M ... ( m + 1 ) ) --> A ) )
427 fveq2 
 |-  ( n = ( m + 1 ) -> ( f ` n ) = ( f ` ( m + 1 ) ) )
428 427 sbceq1d 
 |-  ( n = ( m + 1 ) -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` ( m + 1 ) ) / a ]. th ) )
429 45 428 bitr3id 
 |-  ( n = ( m + 1 ) -> ( ta <-> [. ( f ` ( m + 1 ) ) / a ]. th ) )
430 429 anbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ( f ` M ) = a /\ ta ) <-> ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) ) )
431 oveq2 
 |-  ( n = ( m + 1 ) -> ( N ... n ) = ( N ... ( m + 1 ) ) )
432 431 raleqdv 
 |-  ( n = ( m + 1 ) -> ( A. k e. ( N ... n ) ch <-> A. k e. ( N ... ( m + 1 ) ) ch ) )
433 426 430 432 3anbi123d 
 |-  ( n = ( m + 1 ) -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
434 433 exbidv 
 |-  ( n = ( m + 1 ) -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) )
435 434 rspcev 
 |-  ( ( ( m + 1 ) e. Z /\ E. f ( f : ( M ... ( m + 1 ) ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) /\ A. k e. ( N ... ( m + 1 ) ) ch ) ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
436 128 424 435 syl2anc 
 |-  ( ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) /\ ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
437 436 ex 
 |-  ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) -> ( ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
438 437 exlimdv 
 |-  ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) /\ m e. Z ) -> ( E. g ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
439 438 rexlimdva 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( E. m e. Z E. g ( g : ( M ... m ) --> A /\ ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) /\ A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
440 126 439 biimtrid 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = b /\ ta ) /\ A. k e. ( N ... n ) ch ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
441 78 93 440 3syld 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
442 441 an42s 
 |-  ( ( ( et /\ a e. A ) /\ ( b e. A /\ ph ) ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
443 442 rexlimdvaa 
 |-  ( ( et /\ a e. A ) -> ( E. b e. A ph -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) ) )
444 443 imp 
 |-  ( ( ( et /\ a e. A ) /\ E. b e. A ph ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
445 71 444 10 mpjaodan 
 |-  ( ( et /\ a e. A ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
446 141 anbi1d 
 |-  ( c = a -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = a /\ ta ) ) )
447 446 3anbi2d 
 |-  ( c = a -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
448 447 exbidv 
 |-  ( c = a -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
449 448 rexbidv 
 |-  ( c = a -> ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
450 449 elrab3 
 |-  ( a e. A -> ( a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
451 450 adantl 
 |-  ( ( et /\ a e. A ) -> ( a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
452 445 451 sylibrd 
 |-  ( ( et /\ a e. A ) -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) )
453 452 ex 
 |-  ( et -> ( a e. A -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) )
454 453 com23 
 |-  ( et -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> ( a e. A -> a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) )
455 eldif 
 |-  ( a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) <-> ( a e. A /\ -. a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) )
456 455 notbii 
 |-  ( -. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) <-> -. ( a e. A /\ -. a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) )
457 iman 
 |-  ( ( a e. A -> a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) <-> -. ( a e. A /\ -. a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) )
458 456 457 bitr4i 
 |-  ( -. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) <-> ( a e. A -> a e. { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) )
459 454 458 imbitrrdi 
 |-  ( et -> ( A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a -> -. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) )
460 459 con2d 
 |-  ( et -> ( a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -> -. A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a ) )
461 460 imp 
 |-  ( ( et /\ a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) ) -> -. A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a )
462 461 nrexdv 
 |-  ( et -> -. E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a )
463 df-ne 
 |-  ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) =/= (/) <-> -. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) = (/) )
464 difss 
 |-  ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) C_ A
465 difexg 
 |-  ( A e. _V -> ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) e. _V )
466 1 465 ax-mp 
 |-  ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) e. _V
467 fri 
 |-  ( ( ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) e. _V /\ R Fr A ) /\ ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) C_ A /\ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) =/= (/) ) ) -> E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a )
468 466 467 mpanl1 
 |-  ( ( R Fr A /\ ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) C_ A /\ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) =/= (/) ) ) -> E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a )
469 468 expr 
 |-  ( ( R Fr A /\ ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) C_ A ) -> ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) =/= (/) -> E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a ) )
470 9 464 469 sylancl 
 |-  ( et -> ( ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) =/= (/) -> E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a ) )
471 463 470 biimtrrid 
 |-  ( et -> ( -. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) = (/) -> E. a e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) A. d e. ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) -. d R a ) )
472 462 471 mt3d 
 |-  ( et -> ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) = (/) )
473 ssdif0 
 |-  ( A C_ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } <-> ( A \ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } ) = (/) )
474 472 473 sylibr 
 |-  ( et -> A C_ { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } )
475 81 a1i 
 |-  ( et -> { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } C_ A )
476 474 475 eqssd 
 |-  ( et -> A = { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } )
477 rabid2 
 |-  ( A = { c e. A | E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) } <-> A. c e. A E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) )
478 476 477 sylib 
 |-  ( et -> A. c e. A E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) )
479 eqeq2 
 |-  ( c = C -> ( ( f ` M ) = c <-> ( f ` M ) = C ) )
480 479 anbi1d 
 |-  ( c = C -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = C /\ ta ) ) )
481 480 3anbi2d 
 |-  ( c = C -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
482 481 exbidv 
 |-  ( c = C -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
483 482 rexbidv 
 |-  ( c = C -> ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) <-> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
484 483 rspcva 
 |-  ( ( C e. A /\ A. c e. A E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )
485 8 478 484 syl2anc 
 |-  ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )