Metamath Proof Explorer

Theorem sdclem1

Description: Lemma for sdc . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses sdc.1 
|- Z = ( ZZ>= ` M )
sdc.2 
|- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
sdc.3 
|- ( n = M -> ( ps <-> ta ) )
sdc.4 
|- ( n = k -> ( ps <-> th ) )
sdc.5 
|- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
sdc.6 
|- ( ph -> A e. V )
sdc.7 
|- ( ph -> M e. ZZ )
sdc.8 
|- ( ph -> E. g ( g : { M } --> A /\ ta ) )
sdc.9 
|- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
sdc.10 
|- J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }
sdc.11 
|- F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
Assertion sdclem1 
|- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )

Proof

Step Hyp Ref Expression
1 sdc.1 
 |-  Z = ( ZZ>= ` M )
2 sdc.2 
 |-  ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
3 sdc.3 
 |-  ( n = M -> ( ps <-> ta ) )
4 sdc.4 
 |-  ( n = k -> ( ps <-> th ) )
5 sdc.5 
 |-  ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
6 sdc.6 
 |-  ( ph -> A e. V )
7 sdc.7 
 |-  ( ph -> M e. ZZ )
8 sdc.8 
 |-  ( ph -> E. g ( g : { M } --> A /\ ta ) )
9 sdc.9 
 |-  ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
10 sdc.10 
 |-  J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }
11 sdc.11 
 |-  F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
12 1 fvexi 
 |-  Z e. _V
13 simpl 
 |-  ( ( g : ( M ... n ) --> A /\ ps ) -> g : ( M ... n ) --> A )
14 ovex 
 |-  ( M ... n ) e. _V
15 elmapg 
 |-  ( ( A e. V /\ ( M ... n ) e. _V ) -> ( g e. ( A ^m ( M ... n ) ) <-> g : ( M ... n ) --> A ) )
16 6 14 15 sylancl 
 |-  ( ph -> ( g e. ( A ^m ( M ... n ) ) <-> g : ( M ... n ) --> A ) )
17 13 16 imbitrrid 
 |-  ( ph -> ( ( g : ( M ... n ) --> A /\ ps ) -> g e. ( A ^m ( M ... n ) ) ) )
18 17 abssdv 
 |-  ( ph -> { g | ( g : ( M ... n ) --> A /\ ps ) } C_ ( A ^m ( M ... n ) ) )
19 ovex 
 |-  ( A ^m ( M ... n ) ) e. _V
20 ssexg 
 |-  ( ( { g | ( g : ( M ... n ) --> A /\ ps ) } C_ ( A ^m ( M ... n ) ) /\ ( A ^m ( M ... n ) ) e. _V ) -> { g | ( g : ( M ... n ) --> A /\ ps ) } e. _V )
21 18 19 20 sylancl 
 |-  ( ph -> { g | ( g : ( M ... n ) --> A /\ ps ) } e. _V )
22 21 ralrimivw 
 |-  ( ph -> A. n e. Z { g | ( g : ( M ... n ) --> A /\ ps ) } e. _V )
23 abrexex2g 
 |-  ( ( Z e. _V /\ A. n e. Z { g | ( g : ( M ... n ) --> A /\ ps ) } e. _V ) -> { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } e. _V )
24 12 22 23 sylancr 
 |-  ( ph -> { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } e. _V )
25 10 24 eqeltrid 
 |-  ( ph -> J e. _V )
26 25 adantr 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> J e. _V )
27 7 adantr 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> M e. ZZ )
28 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
29 27 28 syl 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> M e. ( ZZ>= ` M ) )
30 29 1 eleqtrrdi 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> M e. Z )
31 simprl 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> g : { M } --> A )
32 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
33 27 32 syl 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( M ... M ) = { M } )
34 33 feq2d 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( g : ( M ... M ) --> A <-> g : { M } --> A ) )
35 31 34 mpbird 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> g : ( M ... M ) --> A )
36 simprr 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ta )
37 oveq2 
 |-  ( n = M -> ( M ... n ) = ( M ... M ) )
38 37 feq2d 
 |-  ( n = M -> ( g : ( M ... n ) --> A <-> g : ( M ... M ) --> A ) )
39 38 3 anbi12d 
 |-  ( n = M -> ( ( g : ( M ... n ) --> A /\ ps ) <-> ( g : ( M ... M ) --> A /\ ta ) ) )
40 39 rspcev 
 |-  ( ( M e. Z /\ ( g : ( M ... M ) --> A /\ ta ) ) -> E. n e. Z ( g : ( M ... n ) --> A /\ ps ) )
41 30 35 36 40 syl12anc 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> E. n e. Z ( g : ( M ... n ) --> A /\ ps ) )
42 10 eqabri 
 |-  ( g e. J <-> E. n e. Z ( g : ( M ... n ) --> A /\ ps ) )
43 41 42 sylibr 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> g e. J )
44 1 peano2uzs 
 |-  ( k e. Z -> ( k + 1 ) e. Z )
45 44 ad2antlr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> ( k + 1 ) e. Z )
46 simpr1 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> h : ( M ... ( k + 1 ) ) --> A )
47 simpr3 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> si )
48 vex 
 |-  h e. _V
49 ovex 
 |-  ( k + 1 ) e. _V
50 5 a1i 
 |-  ( ph -> ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) ) )
51 48 49 50 sbc2iedv 
 |-  ( ph -> ( [. h / g ]. [. ( k + 1 ) / n ]. ps <-> si ) )
52 51 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> ( [. h / g ]. [. ( k + 1 ) / n ]. ps <-> si ) )
53 47 52 mpbird 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> [. h / g ]. [. ( k + 1 ) / n ]. ps )
54 nfv 
 |-  F/ n h : ( M ... ( k + 1 ) ) --> A
55 nfcv 
 |-  F/_ n h
56 nfsbc1v 
 |-  F/ n [. ( k + 1 ) / n ]. ps
57 55 56 nfsbcw 
 |-  F/ n [. h / g ]. [. ( k + 1 ) / n ]. ps
58 54 57 nfan 
 |-  F/ n ( h : ( M ... ( k + 1 ) ) --> A /\ [. h / g ]. [. ( k + 1 ) / n ]. ps )
59 oveq2 
 |-  ( n = ( k + 1 ) -> ( M ... n ) = ( M ... ( k + 1 ) ) )
60 59 feq2d 
 |-  ( n = ( k + 1 ) -> ( h : ( M ... n ) --> A <-> h : ( M ... ( k + 1 ) ) --> A ) )
61 sbceq1a 
 |-  ( n = ( k + 1 ) -> ( ps <-> [. ( k + 1 ) / n ]. ps ) )
62 61 sbcbidv 
 |-  ( n = ( k + 1 ) -> ( [. h / g ]. ps <-> [. h / g ]. [. ( k + 1 ) / n ]. ps ) )
63 60 62 anbi12d 
 |-  ( n = ( k + 1 ) -> ( ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) <-> ( h : ( M ... ( k + 1 ) ) --> A /\ [. h / g ]. [. ( k + 1 ) / n ]. ps ) ) )
64 58 63 rspce 
 |-  ( ( ( k + 1 ) e. Z /\ ( h : ( M ... ( k + 1 ) ) --> A /\ [. h / g ]. [. ( k + 1 ) / n ]. ps ) ) -> E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) )
65 45 46 53 64 syl12anc 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) )
66 10 eleq2i 
 |-  ( h e. J <-> h e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } )
67 nfcv 
 |-  F/_ g Z
68 nfv 
 |-  F/ g h : ( M ... n ) --> A
69 nfsbc1v 
 |-  F/ g [. h / g ]. ps
70 68 69 nfan 
 |-  F/ g ( h : ( M ... n ) --> A /\ [. h / g ]. ps )
71 67 70 nfrexw 
 |-  F/ g E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps )
72 feq1 
 |-  ( g = h -> ( g : ( M ... n ) --> A <-> h : ( M ... n ) --> A ) )
73 sbceq1a 
 |-  ( g = h -> ( ps <-> [. h / g ]. ps ) )
74 72 73 anbi12d 
 |-  ( g = h -> ( ( g : ( M ... n ) --> A /\ ps ) <-> ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) ) )
75 74 rexbidv 
 |-  ( g = h -> ( E. n e. Z ( g : ( M ... n ) --> A /\ ps ) <-> E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) ) )
76 71 48 75 elabf 
 |-  ( h e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } <-> E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) )
77 66 76 bitri 
 |-  ( h e. J <-> E. n e. Z ( h : ( M ... n ) --> A /\ [. h / g ]. ps ) )
78 65 77 sylibr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) -> h e. J )
79 78 rexlimdva2 
 |-  ( ph -> ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) -> h e. J ) )
80 79 abssdv 
 |-  ( ph -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } C_ J )
81 80 ad2antrr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } C_ J )
82 25 ad2antrr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> J e. _V )
83 elpw2g 
 |-  ( J e. _V -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ~P J <-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } C_ J ) )
84 82 83 syl 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ~P J <-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } C_ J ) )
85 81 84 mpbird 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ~P J )
86 oveq2 
 |-  ( n = k -> ( M ... n ) = ( M ... k ) )
87 86 feq2d 
 |-  ( n = k -> ( g : ( M ... n ) --> A <-> g : ( M ... k ) --> A ) )
88 87 4 anbi12d 
 |-  ( n = k -> ( ( g : ( M ... n ) --> A /\ ps ) <-> ( g : ( M ... k ) --> A /\ th ) ) )
89 88 cbvrexvw 
 |-  ( E. n e. Z ( g : ( M ... n ) --> A /\ ps ) <-> E. k e. Z ( g : ( M ... k ) --> A /\ th ) )
90 9 reximdva 
 |-  ( ph -> ( E. k e. Z ( g : ( M ... k ) --> A /\ th ) -> E. k e. Z E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
91 rexcom4 
 |-  ( E. k e. Z E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) <-> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) )
92 90 91 imbitrdi 
 |-  ( ph -> ( E. k e. Z ( g : ( M ... k ) --> A /\ th ) -> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
93 89 92 biimtrid 
 |-  ( ph -> ( E. n e. Z ( g : ( M ... n ) --> A /\ ps ) -> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
94 93 ss2abdv 
 |-  ( ph -> { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } C_ { g | E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) } )
95 10 94 eqsstrid 
 |-  ( ph -> J C_ { g | E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) } )
96 95 sselda 
 |-  ( ( ph /\ x e. J ) -> x e. { g | E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) } )
97 vex 
 |-  x e. _V
98 eqeq1 
 |-  ( g = x -> ( g = ( h |` ( M ... k ) ) <-> x = ( h |` ( M ... k ) ) ) )
99 98 3anbi2d 
 |-  ( g = x -> ( ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) <-> ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) )
100 99 rexbidv 
 |-  ( g = x -> ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) <-> E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) )
101 100 exbidv 
 |-  ( g = x -> ( E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) <-> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) )
102 97 101 elab 
 |-  ( x e. { g | E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) } <-> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) )
103 96 102 sylib 
 |-  ( ( ph /\ x e. J ) -> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) )
104 abn0 
 |-  ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } =/= (/) <-> E. h E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) )
105 103 104 sylibr 
 |-  ( ( ph /\ x e. J ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } =/= (/) )
106 105 adantlr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } =/= (/) )
107 eldifsn 
 |-  ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ( ~P J \ { (/) } ) <-> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ~P J /\ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } =/= (/) ) )
108 85 106 107 sylanbrc 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ x e. J ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ( ~P J \ { (/) } ) )
109 108 adantrl 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( w e. Z /\ x e. J ) ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ( ~P J \ { (/) } ) )
110 109 ralrimivva 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> A. w e. Z A. x e. J { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ( ~P J \ { (/) } ) )
111 11 fmpo 
 |-  ( A. w e. Z A. x e. J { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. ( ~P J \ { (/) } ) <-> F : ( Z X. J ) --> ( ~P J \ { (/) } ) )
112 110 111 sylib 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> F : ( Z X. J ) --> ( ~P J \ { (/) } ) )
113 7 iftrued 
 |-  ( ph -> if ( M e. ZZ , M , 0 ) = M )
114 113 fveq2d 
 |-  ( ph -> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) = ( ZZ>= ` M ) )
115 114 1 eqtr4di 
 |-  ( ph -> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) = Z )
116 115 xpeq1d 
 |-  ( ph -> ( ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) X. J ) = ( Z X. J ) )
117 116 feq2d 
 |-  ( ph -> ( F : ( ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) X. J ) --> ( ~P J \ { (/) } ) <-> F : ( Z X. J ) --> ( ~P J \ { (/) } ) ) )
118 117 biimpar 
 |-  ( ( ph /\ F : ( Z X. J ) --> ( ~P J \ { (/) } ) ) -> F : ( ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) X. J ) --> ( ~P J \ { (/) } ) )
119 112 118 syldan 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> F : ( ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) X. J ) --> ( ~P J \ { (/) } ) )
120 0z 
 |-  0 e. ZZ
121 120 elimel 
 |-  if ( M e. ZZ , M , 0 ) e. ZZ
122 eqid 
 |-  ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) = ( ZZ>= ` if ( M e. ZZ , M , 0 ) )
123 121 122 axdc4uz 
 |-  ( ( J e. _V /\ g e. J /\ F : ( ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) X. J ) --> ( ~P J \ { (/) } ) ) -> E. j ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J /\ ( j ` if ( M e. ZZ , M , 0 ) ) = g /\ A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) )
124 26 43 119 123 syl3anc 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> E. j ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J /\ ( j ` if ( M e. ZZ , M , 0 ) ) = g /\ A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) )
125 27 iftrued 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> if ( M e. ZZ , M , 0 ) = M )
126 125 fveq2d 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) = ( ZZ>= ` M ) )
127 126 1 eqtr4di 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) = Z )
128 127 feq2d 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J <-> j : Z --> J ) )
129 89 abbii 
 |-  { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } = { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) }
130 10 129 eqtri 
 |-  J = { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) }
131 feq3 
 |-  ( J = { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } -> ( j : Z --> J <-> j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } ) )
132 130 131 ax-mp 
 |-  ( j : Z --> J <-> j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } )
133 128 132 bitrdi 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J <-> j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } ) )
134 125 fveqeq2d 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ( j ` if ( M e. ZZ , M , 0 ) ) = g <-> ( j ` M ) = g ) )
135 127 raleqdv 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) <-> A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) )
136 133 134 135 3anbi123d 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J /\ ( j ` if ( M e. ZZ , M , 0 ) ) = g /\ A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) <-> ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) )
137 6 ad2antrr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> A e. V )
138 7 ad2antrr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> M e. ZZ )
139 8 ad2antrr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> E. g ( g : { M } --> A /\ ta ) )
140 simpll 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> ph )
141 140 9 sylan 
 |-  ( ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
142 nfv 
 |-  F/ k ( ph /\ ( g : { M } --> A /\ ta ) )
143 nfcv 
 |-  F/_ k j
144 nfcv 
 |-  F/_ k Z
145 nfre1 
 |-  F/ k E. k e. Z ( g : ( M ... k ) --> A /\ th )
146 145 nfab 
 |-  F/_ k { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) }
147 143 144 146 nff 
 |-  F/ k j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) }
148 nfv 
 |-  F/ k ( j ` M ) = g
149 nfcv 
 |-  F/_ k m
150 130 146 nfcxfr 
 |-  F/_ k J
151 nfre1 
 |-  F/ k E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si )
152 151 nfab 
 |-  F/_ k { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) }
153 144 150 152 nfmpo 
 |-  F/_ k ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
154 11 153 nfcxfr 
 |-  F/_ k F
155 nfcv 
 |-  F/_ k ( j ` m )
156 149 154 155 nfov 
 |-  F/_ k ( m F ( j ` m ) )
157 156 nfel2 
 |-  F/ k ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) )
158 144 157 nfralw 
 |-  F/ k A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) )
159 147 148 158 nf3an 
 |-  F/ k ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) )
160 142 159 nfan 
 |-  F/ k ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) )
161 simpr1 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } )
162 161 132 sylibr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> j : Z --> J )
163 31 adantr 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> g : { M } --> A )
164 simpr2 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> ( j ` M ) = g )
165 138 32 syl 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> ( M ... M ) = { M } )
166 164 165 feq12d 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> ( ( j ` M ) : ( M ... M ) --> A <-> g : { M } --> A ) )
167 163 166 mpbird 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> ( j ` M ) : ( M ... M ) --> A )
168 simpr3 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) )
169 fvoveq1 
 |-  ( m = w -> ( j ` ( m + 1 ) ) = ( j ` ( w + 1 ) ) )
170 id 
 |-  ( m = w -> m = w )
171 fveq2 
 |-  ( m = w -> ( j ` m ) = ( j ` w ) )
172 170 171 oveq12d 
 |-  ( m = w -> ( m F ( j ` m ) ) = ( w F ( j ` w ) ) )
173 169 172 eleq12d 
 |-  ( m = w -> ( ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) <-> ( j ` ( w + 1 ) ) e. ( w F ( j ` w ) ) ) )
174 173 rspccva 
 |-  ( ( A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) /\ w e. Z ) -> ( j ` ( w + 1 ) ) e. ( w F ( j ` w ) ) )
175 168 174 sylan 
 |-  ( ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) /\ w e. Z ) -> ( j ` ( w + 1 ) ) e. ( w F ( j ` w ) ) )
176 1 2 3 4 5 137 138 139 141 10 11 160 162 167 175 sdclem2 
 |-  ( ( ( ph /\ ( g : { M } --> A /\ ta ) ) /\ ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
177 176 ex 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ( j : Z --> { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } /\ ( j ` M ) = g /\ A. m e. Z ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) ) )
178 136 177 sylbid 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J /\ ( j ` if ( M e. ZZ , M , 0 ) ) = g /\ A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) ) )
179 178 exlimdv 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> ( E. j ( j : ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) --> J /\ ( j ` if ( M e. ZZ , M , 0 ) ) = g /\ A. m e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ( j ` ( m + 1 ) ) e. ( m F ( j ` m ) ) ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) ) )
180 124 179 mpd 
 |-  ( ( ph /\ ( g : { M } --> A /\ ta ) ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
181 8 180 exlimddv 
 |-  ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )