Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fdc Structured version   Visualization version   Unicode version
Theorem fdc 33541
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.)
Hypotheses
Ref Expression
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
Ref Expression
fdc |- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )
Distinct variable groups:   C, f, n   A, a, b, f, n   M, a, b, f, k, n   Z, a, b, n   N, a, b, f, k, n   R, a, b   ph, f, k   ps, a   ch, a, b, n   th, f, n   ta, a, b   et, a, b
Allowed substitution hints:   ph( n, a, b)   ps( f, k, n, b)   ch( f, k)   th( k, a, b)   ta( f, k, n)   et( f, k, n)   A( k)   C( k, a, b)   R( f, k, n)   Z( f, k)
Proof of Theorem fdc
Dummy variables c d g m x j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fdc.8 . 2 |- ( et -> C e. A )
2 fdc.2 . . . . . . . . . . . . . . . . . . 19 |- M e. ZZ
3 uzid 11702 . . . . . . . . . . . . . . . . . . 19 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- M e. ( ZZ>= ` M )
5 fdc.3 . . . . . . . . . . . . . . . . . 18 |- Z = ( ZZ>= ` M )
64, 5eleqtrri 2700 . . . . . . . . . . . . . . . . 17 |- M e. Z
7 eqid 2622 . . . . . . . . . . . . . . . . . . . . . 22 |- { <. M , a >. } = { <. M , a >. }
82elexi 3213 . . . . . . . . . . . . . . . . . . . . . . 23 |- M e. _V
9 vex 3203 . . . . . . . . . . . . . . . . . . . . . . 23 |- a e. _V
108, 9fsn 6402 . . . . . . . . . . . . . . . . . . . . . 22 |- ( { <. M , a >. } : { M } --> { a } <-> { <. M , a >. } = { <. M , a >. } )
117, 10mpbir 221 . . . . . . . . . . . . . . . . . . . . 21 |- { <. M , a >. } : { M } --> { a }
12 snssi 4339 . . . . . . . . . . . . . . . . . . . . 21 |- ( a e. A -> { a } C_ A )
13 fss 6056 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( { <. M , a >. } : { M } --> { a } /\ { a } C_ A ) -> { <. M , a >. } : { M } --> A )
1411, 12, 13sylancr 695 . . . . . . . . . . . . . . . . . . . 20 |- ( a e. A -> { <. M , a >. } : { M } --> A )
15 fzsn 12383 . . . . . . . . . . . . . . . . . . . . . 22 |- ( M e. ZZ -> ( M ... M ) = { M } )
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 |- ( M ... M ) = { M }
1716feq2i 6037 . . . . . . . . . . . . . . . . . . . 20 |- ( { <. M , a >. } : ( M ... M ) --> A <-> { <. M , a >. } : { M } --> A )
1814, 17sylibr 224 . . . . . . . . . . . . . . . . . . 19 |- ( a e. A -> { <. M , a >. } : ( M ... M ) --> A )
1918adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( a e. A /\ th ) -> { <. M , a >. } : ( M ... M ) --> A )
208, 9fvsn 6446 . . . . . . . . . . . . . . . . . . 19 |- ( { <. M , a >. } ` M ) = a
2120a1i 11 . . . . . . . . . . . . . . . . . 18 |- ( ( a e. A /\ th ) -> ( { <. M , a >. } ` M ) = a )
22 simpr 477 . . . . . . . . . . . . . . . . . 18 |- ( ( a e. A /\ th ) -> th )
23 snex 4908 . . . . . . . . . . . . . . . . . . 19 |- { <. M , a >. } e. _V
24 feq1 6026 . . . . . . . . . . . . . . . . . . . 20 |- ( f = { <. M , a >. } -> ( f : ( M ... M ) --> A <-> { <. M , a >. } : ( M ... M ) --> A ) )
25 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . 22 |- ( f = { <. M , a >. } -> ( f ` M ) = ( { <. M , a >. } ` M ) )
2625eqeq1d 2624 . . . . . . . . . . . . . . . . . . . . 21 |- ( f = { <. M , a >. } -> ( ( f ` M ) = a <-> ( { <. M , a >. } ` M ) = a ) )
2725, 20syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . 22 |- ( f = { <. M , a >. } -> ( f ` M ) = a )
28 sbceq2a 3447 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( f ` M ) = a -> ( [. ( f ` M ) / a ]. th <-> th ) )
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 |- ( f = { <. M , a >. } -> ( [. ( f ` M ) / a ]. th <-> th ) )
3026, 29anbi12d 747 . . . . . . . . . . . . . . . . . . . 20 |- ( f = { <. M , a >. } -> ( ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) <-> ( ( { <. M , a >. } ` M ) = a /\ th ) ) )
3124, 30anbi12d 747 . . . . . . . . . . . . . . . . . . 19 |- ( f = { <. M , a >. } -> ( ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) <-> ( { <. M , a >. } : ( M ... M ) --> A /\ ( ( { <. M , a >. } ` M ) = a /\ th ) ) ) )
3223, 31spcev 3300 . . . . . . . . . . . . . . . . . 18 |- ( ( { <. M , a >. } : ( M ... M ) --> A /\ ( ( { <. M , a >. } ` M ) = a /\ th ) ) -> E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
3319, 21, 22, 32syl12anc 1324 . . . . . . . . . . . . . . . . 17 |- ( ( a e. A /\ th ) -> E. f ( f : ( M ... M ) --> A /\ ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
34 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . 22 |- ( n = M -> ( M ... n ) = ( M ... M ) )
3534feq2d 6031 . . . . . . . . . . . . . . . . . . . . 21 |- ( n = M -> ( f : ( M ... n ) --> A <-> f : ( M ... M ) --> A ) )
36 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f ` n ) e. _V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = ( f ` n ) -> ( th <-> ta ) )
3836, 37sbcie 3470 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( [. ( f ` n ) / a ]. th <-> ta )
39 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = M -> ( f ` n ) = ( f ` M ) )
4039sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = M -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` M ) / a ]. th ) )
4138, 40syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . 22 |- ( n = M -> ( ta <-> [. ( f ` M ) / a ]. th ) )
4241anbi2d 740 . . . . . . . . . . . . . . . . . . . . 21 |- ( n = M -> ( ( ( f ` M ) = a /\ ta ) <-> ( ( f ` M ) = a /\ [. ( f ` M ) / a ]. th ) ) )
43 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = M -> ( N ... n ) = ( N ... M ) )
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- N = ( M + 1 )
4544oveq1i 6660 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N ... M ) = ( ( M + 1 ) ... M )
462zrei 11383 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- M e. RR
4746ltp1i 10927 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- M < ( M + 1 )
48 peano2z 11418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( M e. ZZ -> ( M + 1 ) e. ZZ )
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( M + 1 ) e. ZZ
50 fzn 12357 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( M + 1 ) e. ZZ /\ M e. ZZ ) -> ( M < ( M + 1 ) <-> ( ( M + 1 ) ... M ) = (/) ) )
5149, 2, 50mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M < ( M + 1 ) <-> ( ( M + 1 ) ... M ) = (/) )
5247, 51mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( M + 1 ) ... M ) = (/)
5345, 52eqtri 2644 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( N ... M ) = (/)
5443, 53syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . 22 |- ( n = M -> ( N ... n ) = (/) )
5554raleqdv 3144 . . . . . . . . . . . . . . . . . . . . 21 |- ( n = M -> ( A. k e. ( N ... n ) ch <-> A. k e. (/) ch ) )
5635, 42, 553anbi123d 1399 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) )
57 ral0 4076 . . . . . . . . . . . . . . . . . . . . 21 |- A. k e. (/) ch
58 df-3an 1039 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) )
5957, 58mpbiran2 954 . . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) )
6056, 59syl6bb 276 . . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) )
6160exbidv 1850 . . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) )
6261rspcev 3309 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) )
636, 33, 62sylancr 695 . . . . . . . . . . . . . . . 16 |- ( ( a e. A /\ th ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = a /\ ta ) /\ A. k e. ( N ... n ) ch ) )
6463adantll 750 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
6564a1d 25 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )
67 breq1 4656 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( d = b -> ( d R a <-> b R a ) )
6867rspcev 3309 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
6968expcom 451 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) )
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) )
71 dfrex2 2996 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 )
7270, 71syl6ib 241 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
7372con2d 129 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) } ) ) )
74 eldif 3584 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) } ) ) )
7574simplbi2 655 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) } ) ) ) )
76 ssrab2 3687 . . . . . . . . . . . . . . . . . . . . . . 23 |- { 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
77 dfss4 3858 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( { 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 ) } )
7876, 77mpbi 220 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) }
7978eleq2i 2693 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) } )
80 eqeq2 2633 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( c = b -> ( ( f ` M ) = c <-> ( f ` M ) = b ) )
8180anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c = b -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = b /\ ta ) ) )
82813anbi2d 1404 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) )
8382exbidv 1850 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) )
8483rexbidv 3052 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
8584elrab3 3364 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
8679, 85syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) )
8775, 86sylibd 229 . . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
8887ad2antll 765 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
89 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = m -> ( M ... n ) = ( M ... m ) )
9089feq2d 6031 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = m -> ( f : ( M ... n ) --> A <-> f : ( M ... m ) --> A ) )
91 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = m -> ( f ` n ) = ( f ` m ) )
9291sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = m -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` m ) / a ]. th ) )
9338, 92syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = m -> ( ta <-> [. ( f ` m ) / a ]. th ) )
9493anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = m -> ( ( ( f ` M ) = b /\ ta ) <-> ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) ) )
95 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = m -> ( N ... n ) = ( N ... m ) )
9695raleqdv 3144 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = m -> ( A. k e. ( N ... n ) ch <-> A. k e. ( N ... m ) ch ) )
9790, 94, 963anbi123d 1399 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
9897exbidv 1850 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
9998cbvrexv 3172 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) )
100 feq1 6026 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( f = g -> ( f : ( M ... m ) --> A <-> g : ( M ... m ) --> A ) )
101 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f = g -> ( f ` M ) = ( g ` M ) )
102101eqeq1d 2624 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f = g -> ( ( f ` M ) = b <-> ( g ` M ) = b ) )
103 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f = g -> ( f ` m ) = ( g ` m ) )
104103sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f = g -> ( [. ( f ` m ) / a ]. th <-> [. ( g ` m ) / a ]. th ) )
105102, 104anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( f = g -> ( ( ( f ` M ) = b /\ [. ( f ` m ) / a ]. th ) <-> ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) ) )
106 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` ( k - 1 ) ) e. _V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )
108107sbcbidv 3490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( a = ( f ` ( k - 1 ) ) -> ( [. ( f ` k ) / b ]. ph <-> [. ( f ` k ) / b ]. ps ) )
109106, 108sbcie 3470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> [. ( f ` k ) / b ]. ps )
110 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` k ) e. _V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( b = ( f ` k ) -> ( ps <-> ch ) )
112110, 111sbcie 3470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( [. ( f ` k ) / b ]. ps <-> ch )
113109, 112bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> ch )
114 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f = g -> ( f ` ( k - 1 ) ) = ( g ` ( k - 1 ) ) )
115 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f = g -> ( f ` k ) = ( g ` k ) )
116115sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f = g -> ( [. ( f ` k ) / b ]. ph <-> [. ( g ` k ) / b ]. ph ) )
117114, 116sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f = g -> ( [. ( f ` ( k - 1 ) ) / a ]. [. ( f ` k ) / b ]. ph <-> [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
118113, 117syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f = g -> ( ch <-> [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
119118ralbidv 2986 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( f = g -> ( A. k e. ( N ... m ) ch <-> A. k e. ( N ... m ) [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph ) )
120100, 105, 1193anbi123d 1399 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
121120cbvexv 2275 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) )
122121rexbii 3041 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) )
12399, 122bitri 264 . . . . . . . . . . . . . . . . . . 19 |- ( 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 ) )
1245peano2uzs 11742 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. Z -> ( m + 1 ) e. Z )
125124ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( 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 )
126 sbceq2a 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( d = b -> ( [. d / b ]. ph <-> ph ) )
127126anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( d = b -> ( ( [. d / b ]. ph /\ a e. A ) <-> ( ph /\ a e. A ) ) )
128127anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( d = b -> ( ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) <-> ( ( ph /\ a e. A ) /\ m e. Z ) ) )
129 eqeq2 2633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( d = b -> ( ( g ` M ) = d <-> ( g ` M ) = b ) )
130129anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( d = b -> ( ( ( g ` M ) = d /\ [. ( g ` m ) / a ]. th ) <-> ( ( g ` M ) = b /\ [. ( g ` m ) / a ]. th ) ) )
1311303anbi2d 1404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( 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 ) ) )
132131imbi1d 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 ) ) ) )
133128, 132imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 ) ) ) ) )
134 sbceq2a 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( c = a -> ( [. c / a ]. [. d / b ]. ph <-> [. d / b ]. ph ) )
135 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( c = a -> ( c e. A <-> a e. A ) )
136134, 135anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( c = a -> ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) <-> ( [. d / b ]. ph /\ a e. A ) ) )
137136anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( c = a -> ( ( ( [. c / a ]. [. d / b ]. ph /\ c e. A ) /\ m e. Z ) <-> ( ( [. d / b ]. ph /\ a e. A ) /\ m e. Z ) ) )
138 eqeq2 2633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( c = a -> ( ( f ` M ) = c <-> ( f ` M ) = a ) )
139138anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( c = a -> ( ( ( f ` M ) = c /\ [. ( f ` ( m + 1 ) ) / a ]. th ) <-> ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) ) )
1401393anbi2d 1404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 ) ) )
141140exbidv 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 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 ) ) )
142141imbi2d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( 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 ) ) ) )
143137, 142imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 ) ) ) ) )
144 peano2uz 11741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( ZZ>= ` M ) )
145144, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` M ) )
146 elfzp12 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( m + 1 ) e. ( ZZ>= ` M ) -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( m e. Z -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
148147ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) <-> ( x = M \/ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) )
149 iftrue 4092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = c )
150149eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( x = M -> ( if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A <-> c e. A ) )
151150biimprcd 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c e. A -> ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
152151ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x = M -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
153 1re 10039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- 1 e. RR
15446, 153readdcli 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( M + 1 ) e. RR
15546, 154ltnlei 10158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M )
15647, 155mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- -. ( M + 1 ) <_ M
157 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( x = M -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) <-> M e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
158 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( M e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( M + 1 ) <_ M )
159157, 158syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( x = M -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( M + 1 ) <_ M ) )
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x = M -> ( M + 1 ) <_ M ) )
161156, 160mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> -. x = M )
162161adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> -. x = M )
163162iffalsed 4097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = ( g ` ( x - 1 ) ) )
164 elfzelz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> x e. ZZ )
165164adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> x e. ZZ )
166 eluzelz 11697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( m e. ( ZZ>= ` M ) -> m e. ZZ )
167166, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( m e. Z -> m e. ZZ )
168167peano2zd 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( m e. Z -> ( m + 1 ) e. ZZ )
169 1z 11407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- 1 e. ZZ
170 fzsubel 12377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ( ( 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 ) ) ) )
171170biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ( ( 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 ) ) ) )
172169, 171mpanr2 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ( ( 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 ) ) ) )
17349, 172mpanl1 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ( m + 1 ) e. ZZ /\ x e. ZZ ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
174173ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( m + 1 ) e. ZZ -> ( x e. ZZ -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
175168, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( m e. Z -> ( x e. ZZ -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
176175com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> ( x e. ZZ -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
177176imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x e. ZZ -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
178165, 177mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) )
17946recni 10052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- M e. CC
180 ax-1cn 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- 1 e. CC
181179, 180pncan3oi 10297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( M + 1 ) - 1 ) = M
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( ( M + 1 ) - 1 ) = M )
183167zcnd 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( m e. Z -> m e. CC )
184 pncan 10287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
185183, 180, 184sylancl 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( ( m + 1 ) - 1 ) = m )
186182, 185oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( m e. Z -> ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( M ... m ) )
187186adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( ( ( M + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( M ... m ) )
188178, 187eleqtrd 2703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( x - 1 ) e. ( M ... m ) )
189 ffvelrn 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( g : ( M ... m ) --> A /\ ( x - 1 ) e. ( M ... m ) ) -> ( g ` ( x - 1 ) ) e. A )
190188, 189sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( g : ( M ... m ) --> A /\ ( m e. Z /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) ) -> ( g ` ( x - 1 ) ) e. A )
191190anassrs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( g : ( M ... m ) --> A /\ m e. Z ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( g ` ( x - 1 ) ) e. A )
192191ancom1s 847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> ( g ` ( x - 1 ) ) e. A )
193163, 192eqeltrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( m e. Z /\ g : ( M ... m ) --> A ) /\ x e. ( ( M + 1 ) ... ( m + 1 ) ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A )
194193ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( m e. Z /\ g : ( M ... m ) --> A ) -> ( x e. ( ( M + 1 ) ... ( m + 1 ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
195194adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( 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 ) )
196152, 195jaod 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( 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 ) )
197148, 196sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( c e. A /\ m e. Z ) /\ g : ( M ... m ) --> A ) -> ( x e. ( M ... ( m + 1 ) ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) e. A ) )
198197ralrimiv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( 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 )
199 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) = ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) )
200199fmpt 6381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 )
201198, 200sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( 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 )
202201adantlll 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( [. 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 )
2032023ad2antr1 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( [. 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 )
204 eluzfz1 12348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( m + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( m + 1 ) ) )
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( m e. ( ZZ>= ` M ) -> M e. ( M ... ( m + 1 ) ) )
206205, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( m e. Z -> M e. ( M ... ( m + 1 ) ) )
207 vex 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- c e. _V
208149, 199, 207fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( M e. ( M ... ( m + 1 ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
210209ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( [. 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 )
211 eluzfz2 12349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( m + 1 ) e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
213212, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( m e. Z -> ( m + 1 ) e. ( M ... ( m + 1 ) ) )
214 eqeq1 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( x = ( m + 1 ) -> ( x = M <-> ( m + 1 ) = M ) )
215 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( x = ( m + 1 ) -> ( x - 1 ) = ( ( m + 1 ) - 1 ) )
216215fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( x = ( m + 1 ) -> ( g ` ( x - 1 ) ) = ( g ` ( ( m + 1 ) - 1 ) ) )
217214, 216ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( x = ( m + 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) )
218 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( g ` ( ( m + 1 ) - 1 ) ) e. _V
219207, 218ifex 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) e. _V
220217, 199, 219fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( 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 ) ) ) )
221213, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 ) ) ) )
222 eluzle 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( m e. ( ZZ>= ` M ) -> M <_ m )
223222, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( m e. Z -> M <_ m )
224 zleltp1 11428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( M e. ZZ /\ m e. ZZ ) -> ( M <_ m <-> M < ( m + 1 ) ) )
2252, 167, 224sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( m e. Z -> ( M <_ m <-> M < ( m + 1 ) ) )
226223, 225mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( m e. Z -> M < ( m + 1 ) )
227 ltne 10134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( M e. RR /\ M < ( m + 1 ) ) -> ( m + 1 ) =/= M )
22846, 226, 227sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( m e. Z -> ( m + 1 ) =/= M )
229228neneqd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( m e. Z -> -. ( m + 1 ) = M )
230229iffalsed 4097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( m e. Z -> if ( ( m + 1 ) = M , c , ( g ` ( ( m + 1 ) - 1 ) ) ) = ( g ` ( ( m + 1 ) - 1 ) ) )
231185fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( m e. Z -> ( g ` ( ( m + 1 ) - 1 ) ) = ( g ` m ) )
232221, 230, 2313eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) = ( g ` m ) )
233232sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( m e. Z -> ( [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th <-> [. ( g ` m ) / a ]. th ) )
234233biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( m e. Z /\ [. ( g ` m ) / a ]. th ) -> [. ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( m + 1 ) ) / a ]. th )
235234ad2ant2l 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( [. 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 )
2362353ad2antr2 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( [. 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 )
237 eluzp1p1 11713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( m e. ( ZZ>= ` M ) -> ( m + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
238237, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
23944fveq2i 6194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ZZ>= ` N ) = ( ZZ>= ` ( M + 1 ) )
240238, 239syl6eleqr 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( m e. Z -> ( m + 1 ) e. ( ZZ>= ` N ) )
241 elfzp12 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( m + 1 ) e. ( ZZ>= ` N ) -> ( j e. ( N ... ( m + 1 ) ) <-> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) ) )
242240, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( m e. Z -> ( j e. ( N ... ( m + 1 ) ) <-> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) ) )
243242biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( m e. Z /\ j e. ( N ... ( m + 1 ) ) ) -> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
244243adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( [. c / a ]. [. d / b ]. ph /\ m e. Z ) /\ j e. ( N ... ( m + 1 ) ) ) -> ( j = N \/ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
245244adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( [. 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 ) ) ) )
246 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( j = N -> ( j - 1 ) = ( N - 1 ) )
24744oveq1i 6660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( N - 1 ) = ( ( M + 1 ) - 1 )
248247, 181eqtri 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( N - 1 ) = M
249246, 248syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( j = N -> ( j - 1 ) = M )
250249fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( 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 ) )
251250ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( 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 ) )
252209adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` M ) = c )
253251, 252eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( j - 1 ) ) = c )
25444eqeq2i 2634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( j = N <-> j = ( M + 1 ) )
255 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( 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 ) ) )
256254, 255sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( 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 ) ) )
257256ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( 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 ) ) )
25846, 154, 47ltleii 10160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- M <_ ( M + 1 )
259 eluz2 11693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( M + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( M + 1 ) e. ZZ /\ M <_ ( M + 1 ) ) )
2602, 49, 258, 259mpbir3an 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( M + 1 ) e. ( ZZ>= ` M )
261 fzss1 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( ( M + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( M + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
263 eluzfz1 12348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( m e. ( ZZ>= ` M ) -> M e. ( M ... m ) )
264263, 5eleq2s 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( m e. Z -> M e. ( M ... m ) )
265 fzaddel 12375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ( M e. ZZ /\ m e. ZZ ) /\ ( M e. ZZ /\ 1 e. ZZ ) ) -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
2662, 169, 265mpanr12 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( M e. ZZ /\ m e. ZZ ) -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
2672, 167, 266sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( m e. Z -> ( M e. ( M ... m ) <-> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) ) )
268264, 267mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( m e. Z -> ( M + 1 ) e. ( ( M + 1 ) ... ( m + 1 ) ) )
269262, 268sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( m e. Z -> ( M + 1 ) e. ( M ... ( m + 1 ) ) )
270 eqeq1 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( x = ( M + 1 ) -> ( x = M <-> ( M + 1 ) = M ) )
271 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( x = ( M + 1 ) -> ( x - 1 ) = ( ( M + 1 ) - 1 ) )
272271, 181syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( x = ( M + 1 ) -> ( x - 1 ) = M )
273272fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( x = ( M + 1 ) -> ( g ` ( x - 1 ) ) = ( g ` M ) )
274270, 273ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( x = ( M + 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( M + 1 ) = M , c , ( g ` M ) ) )
275 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( g ` M ) e. _V
276207, 275ifex 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- if ( ( M + 1 ) = M , c , ( g ` M ) ) e. _V
277274, 199, 276fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( 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 ) ) )
278269, 277syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = if ( ( M + 1 ) = M , c , ( g ` M ) ) )
27946, 47gtneii 10149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( M + 1 ) =/= M
280 ifnefalse 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( M + 1 ) =/= M -> if ( ( M + 1 ) = M , c , ( g ` M ) ) = ( g ` M ) )
281279, 280ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- if ( ( M + 1 ) = M , c , ( g ` M ) ) = ( g ` M )
282278, 281syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = ( g ` M ) )
283282adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` ( M + 1 ) ) = ( g ` M ) )
284 simprl 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( g ` M ) = d )
285257, 283, 2843eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ ( ( g ` M ) = d /\ j = N ) ) -> ( ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) ` j ) = d )
286285sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( 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 ) )
287253, 286sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( 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 ) )
288287biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( [. 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 )
289288anassrs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( [. 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 )
290289anassrs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( [. 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 )
291290adantlrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( [. 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 )
292 elfzelz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> j e. ZZ )
293292adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ZZ )
29444, 49eqeltri 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- N e. ZZ
295 peano2z 11418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( N e. ZZ -> ( N + 1 ) e. ZZ )
296294, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( N + 1 ) e. ZZ
297 fzsubel 12377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ( ( 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 ) ) ) )
298297biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ( ( 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 ) ) ) )
299169, 298mpanr2 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ( ( 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 ) ) ) )
300299ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ( 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 ) ) ) ) )
301296, 168, 300sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( m e. Z -> ( j e. ZZ -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
302301com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j e. ZZ -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) ) )
303302imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j e. ZZ -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) ) )
304293, 303mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) )
305294zrei 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- N e. RR
306305recni 10052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- N e. CC
307306, 180pncan3oi 10297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( N + 1 ) - 1 ) = N
308307a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( m e. Z -> ( ( N + 1 ) - 1 ) = N )
309308, 185oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( m e. Z -> ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( N ... m ) )
310309adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( ( ( N + 1 ) - 1 ) ... ( ( m + 1 ) - 1 ) ) = ( N ... m ) )
311304, 310eleqtrd 2703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( N ... m ) )
312 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( k = ( j - 1 ) -> ( k - 1 ) = ( ( j - 1 ) - 1 ) )
313312fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( k = ( j - 1 ) -> ( g ` ( k - 1 ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
314 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( k = ( j - 1 ) -> ( g ` k ) = ( g ` ( j - 1 ) ) )
315314sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( k = ( j - 1 ) -> ( [. ( g ` k ) / b ]. ph <-> [. ( g ` ( j - 1 ) ) / b ]. ph ) )
316313, 315sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( k = ( j - 1 ) -> ( [. ( g ` ( k - 1 ) ) / a ]. [. ( g ` k ) / b ]. ph <-> [. ( g ` ( ( j - 1 ) - 1 ) ) / a ]. [. ( g ` ( j - 1 ) ) / b ]. ph ) )
317316rspcva 3307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( 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 )
318311, 317sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( 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 )
31944, 260eqeltri 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- N e. ( ZZ>= ` M )
320 fzss1 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( N e. ( ZZ>= ` M ) -> ( N ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
321319, 320ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( N ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
322 fzssp1 12384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( N ... m ) C_ ( N ... ( m + 1 ) )
323322, 311sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( N ... ( m + 1 ) ) )
324321, 323sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> ( j - 1 ) e. ( M ... ( m + 1 ) ) )
325 eqeq1 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( x = ( j - 1 ) -> ( x = M <-> ( j - 1 ) = M ) )
326 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( x = ( j - 1 ) -> ( x - 1 ) = ( ( j - 1 ) - 1 ) )
327326fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( x = ( j - 1 ) -> ( g ` ( x - 1 ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
328325, 327ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( x = ( j - 1 ) -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) )
329 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( g ` ( ( j - 1 ) - 1 ) ) e. _V
330207, 329ifex 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) e. _V
331328, 199, 330fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( 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 ) ) ) )
332324, 331syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( 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 ) ) ) )
333154ltp1i 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( M + 1 ) < ( ( M + 1 ) + 1 )
33444oveq1i 6660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( N + 1 ) = ( ( M + 1 ) + 1 )
335333, 334breqtrri 4680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( M + 1 ) < ( N + 1 )
336305, 153readdcli 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( N + 1 ) e. RR
337154, 336ltnlei 10158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( M + 1 ) < ( N + 1 ) <-> -. ( N + 1 ) <_ ( M + 1 ) )
338335, 337mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- -. ( N + 1 ) <_ ( M + 1 )
339292zcnd 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> j e. CC )
340 subadd 10284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( j e. CC /\ 1 e. CC /\ M e. CC ) -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
341180, 179, 340mp3an23 1416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( j e. CC -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
342339, 341syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( j - 1 ) = M <-> ( 1 + M ) = j ) )
343 eqcom 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( 1 + M ) = j <-> j = ( 1 + M ) )
344180, 179addcomi 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( 1 + M ) = ( M + 1 )
345344eqeq2i 2634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( j = ( 1 + M ) <-> j = ( M + 1 ) )
346343, 345bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( 1 + M ) = j <-> j = ( M + 1 ) )
347 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( j = ( M + 1 ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) <-> ( M + 1 ) e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
348 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( M + 1 ) e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ ( M + 1 ) )
349347, 348syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( j = ( M + 1 ) -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ ( M + 1 ) ) )
350349com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j = ( M + 1 ) -> ( N + 1 ) <_ ( M + 1 ) ) )
351346, 350syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( 1 + M ) = j -> ( N + 1 ) <_ ( M + 1 ) ) )
352342, 351sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( ( j - 1 ) = M -> ( N + 1 ) <_ ( M + 1 ) ) )
353338, 352mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> -. ( j - 1 ) = M )
354353adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> -. ( j - 1 ) = M )
355354iffalsed 4097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> if ( ( j - 1 ) = M , c , ( g ` ( ( j - 1 ) - 1 ) ) ) = ( g ` ( ( j - 1 ) - 1 ) ) )
356332, 355eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( 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 11741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
358 fzss1 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ( N + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) ) )
359319, 357, 358mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( N + 1 ) ... ( m + 1 ) ) C_ ( M ... ( m + 1 ) )
360 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ( ( N + 1 ) ... ( m + 1 ) ) )
361359, 360sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> j e. ( M ... ( m + 1 ) ) )
362 eqeq1 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( x = j -> ( x = M <-> j = M ) )
363 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( x = j -> ( x - 1 ) = ( j - 1 ) )
364363fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( x = j -> ( g ` ( x - 1 ) ) = ( g ` ( j - 1 ) ) )
365362, 364ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( x = j -> if ( x = M , c , ( g ` ( x - 1 ) ) ) = if ( j = M , c , ( g ` ( j - 1 ) ) ) )
366 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( g ` ( j - 1 ) ) e. _V
367207, 366ifex 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- if ( j = M , c , ( g ` ( j - 1 ) ) ) e. _V
368365, 199, 367fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( 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 ) ) ) )
369361, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( 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 ) ) ) )
37047, 44breqtrri 4680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- M < N
371305ltp1i 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- N < ( N + 1 )
37246, 305, 336lttri 10163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( M < N /\ N < ( N + 1 ) ) -> M < ( N + 1 ) )
373370, 371, 372mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- M < ( N + 1 )
37446, 336ltnlei 10158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( M < ( N + 1 ) <-> -. ( N + 1 ) <_ M )
375373, 374mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- -. ( N + 1 ) <_ M
376 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( j = M -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) <-> M e. ( ( N + 1 ) ... ( m + 1 ) ) ) )
377 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( M e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ M )
378376, 377syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( j = M -> ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( N + 1 ) <_ M ) )
379378com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> ( j = M -> ( N + 1 ) <_ M ) )
380375, 379mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( j e. ( ( N + 1 ) ... ( m + 1 ) ) -> -. j = M )
381380adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> -. j = M )
382381iffalsed 4097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( m e. Z /\ j e. ( ( N + 1 ) ... ( m + 1 ) ) ) -> if ( j = M , c , ( g ` ( j - 1 ) ) ) = ( g ` ( j - 1 ) ) )
383369, 382eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( 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 ) ) )
384383sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( 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 ) )
385356, 384sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( 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 ) )
386385biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( 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 )
387318, 386syldan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( 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 )
388387an32s 846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( 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 )
389388adantlrl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( 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 )
390389adantlll 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( [. 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 )
391291, 390jaodan 826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( [. 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 )
392245, 391syldan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( [. 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 )
393392ralrimiva 2966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( [. 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 )
394 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( j = k -> ( j - 1 ) = ( k - 1 ) )
395394fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( 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 ) ) )
396 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( 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 ) )
397396sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( 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 ) )
398395, 397sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 ) )
399398cbvralv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 )
400393, 399sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( [. 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 )
401400adantllr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( [. 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 )
402401adantrlr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( [. 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 )
4034023adantr1 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( [. 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 )
404 ovex 6678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( M ... ( m + 1 ) ) e. _V
405404mptex 6486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. ( M ... ( m + 1 ) ) |-> if ( x = M , c , ( g ` ( x - 1 ) ) ) ) e. _V
406 feq1 6026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 ) )
407 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 ) )
408407eqeq1d 2624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 ) )
409 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 ) ) )
410409sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 ) )
411408, 410anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 ) ) )
412 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 ) ) )
413 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( 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 ) )
414413sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 ) )
415412, 414sbceqbid 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 ) )
416113, 415syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 ) )
417416ralbidv 2986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 ) )
418406, 411, 4173anbi123d 1399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 ) ) )
419405, 418spcev 3300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 ) )
420203, 210, 236, 403, 419syl121anc 1331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( [. 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 ) )
421420ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( [. 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 ) ) )
422143, 421chvarv 2263 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( [. 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 ) ) )
423133, 422chvarv 2263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 ) ) )
424423adantlrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) )
425424adantlll 754 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) )
426425imp 445 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( 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 ) )
427 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = ( m + 1 ) -> ( M ... n ) = ( M ... ( m + 1 ) ) )
428427feq2d 6031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = ( m + 1 ) -> ( f : ( M ... n ) --> A <-> f : ( M ... ( m + 1 ) ) --> A ) )
429 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = ( m + 1 ) -> ( f ` n ) = ( f ` ( m + 1 ) ) )
430429sbceq1d 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( n = ( m + 1 ) -> ( [. ( f ` n ) / a ]. th <-> [. ( f ` ( m + 1 ) ) / a ]. th ) )
43138, 430syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = ( m + 1 ) -> ( ta <-> [. ( f ` ( m + 1 ) ) / a ]. th ) )
432431anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = ( m + 1 ) -> ( ( ( f ` M ) = a /\ ta ) <-> ( ( f ` M ) = a /\ [. ( f ` ( m + 1 ) ) / a ]. th ) ) )
433 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = ( m + 1 ) -> ( N ... n ) = ( N ... ( m + 1 ) ) )
434433raleqdv 3144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = ( m + 1 ) -> ( A. k e. ( N ... n ) ch <-> A. k e. ( N ... ( m + 1 ) ) ch ) )
435428, 432, 4343anbi123d 1399 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 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 ) ) )
436435exbidv 1850 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) )
437436rspcev 3309 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) )
438125, 426, 437syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 ) )
439438ex 450 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) )
440439exlimdv 1861 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) )
441440rexlimdva 3031 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
442123, 441syl5bi 232 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
44373, 88, 4423syld 60 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
444443an42s 870 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
445444rexlimdvaa 3032 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
446445imp 445 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
447 fdc.10 . . . . . . . . . . . . . 14 |- ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )
44865, 446, 447mpjaodan 827 . . . . . . . . . . . . 13 |- ( ( 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 ) ) )
449138anbi1d 741 . . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = a /\ ta ) ) )
4504493anbi2d 1404 . . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
451450exbidv 1850 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
452451rexbidv 3052 . . . . . . . . . . . . . . 15 |- ( 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 ) ) )
453452elrab3 3364 . . . . . . . . . . . . . 14 |- ( 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 ) ) )
454453adantl 482 . . . . . . . . . . . . 13 |- ( ( 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 ) ) )
455448, 454sylibrd 249 . . . . . . . . . . . 12 |- ( ( 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 ) } ) )
456455ex 450 . . . . . . . . . . 11 |- ( 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 ) } ) ) )
457456com23 86 . . . . . . . . . 10 |- ( 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 ) } ) ) )
458 eldif 3584 . . . . . . . . . . . 12 |- ( 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 ) } ) )
459458notbii 310 . . . . . . . . . . 11 |- ( -. 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 ) } ) )
460 iman 440 . . . . . . . . . . 11 |- ( ( 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 ) } ) )
461459, 460bitr4i 267 . . . . . . . . . 10 |- ( -. 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 ) } ) )
462457, 461syl6ibr 242 . . . . . . . . 9 |- ( 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 ) } ) ) )
463462con2d 129 . . . . . . . 8 |- ( 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 ) )
464463imp 445 . . . . . . 7 |- ( ( 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 )
465464nrexdv 3001 . . . . . 6 |- ( 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 )
466 df-ne 2795 . . . . . . 7 |- ( ( 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 ) } ) = (/) )
467 fdc.9 . . . . . . . 8 |- ( et -> R Fr A )
468 difss 3737 . . . . . . . 8 |- ( 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
469 fdc.1 . . . . . . . . . . 11 |- A e. _V
470 difexg 4808 . . . . . . . . . . 11 |- ( 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 )
471469, 470ax-mp 5 . . . . . . . . . 10 |- ( 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
472 fri 5076 . . . . . . . . . 10 |- ( ( ( ( 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 )
473471, 472mpanl1 716 . . . . . . . . 9 |- ( ( 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 )
474473expr 643 . . . . . . . 8 |- ( ( 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 ) )
475467, 468, 474sylancl 694 . . . . . . 7 |- ( 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 ) )
476466, 475syl5bir 233 . . . . . 6 |- ( 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 ) )
477465, 476mt3d 140 . . . . 5 |- ( 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 ) } ) = (/) )
478 ssdif0 3942 . . . . 5 |- ( 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 ) } ) = (/) )
479477, 478sylibr 224 . . . 4 |- ( 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 ) } )
48076a1i 11 . . . 4 |- ( 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 )
481479, 480eqssd 3620 . . 3 |- ( 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 ) } )
482 rabid2 3118 . . 3 |- ( 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 ) )
483481, 482sylib 208 . 2 |- ( 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 ) )
484 eqeq2 2633 . . . . . . 7 |- ( c = C -> ( ( f ` M ) = c <-> ( f ` M ) = C ) )
485484anbi1d 741 . . . . . 6 |- ( c = C -> ( ( ( f ` M ) = c /\ ta ) <-> ( ( f ` M ) = C /\ ta ) ) )
4864853anbi2d 1404 . . . . 5 |- ( 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 ) ) )
487486exbidv 1850 . . . 4 |- ( 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 ) ) )
488487rexbidv 3052 . . 3 |- ( 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 ) ) )
489488rspcva 3307 . 2 |- ( ( 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 ) )
4901, 483, 489syl2anc 693 1 |- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   \ cdif 3571   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   Fr wfr 5070   -->wf 5884   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   - cmin 10266   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327
This theorem is referenced by:  fdc1  33542
  Copyright terms: Public domain W3C validator