Metamath Proof Explorer

Theorem iccelpart

Description: An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion iccelpart 
|- ( M e. NN -> A. p e. ( RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = 1 -> ( RePart ` x ) = ( RePart ` 1 ) )
2 fveq2 
 |-  ( x = 1 -> ( p ` x ) = ( p ` 1 ) )
3 2 oveq2d 
 |-  ( x = 1 -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
4 3 eleq2d 
 |-  ( x = 1 -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
5 oveq2 
 |-  ( x = 1 -> ( 0 ..^ x ) = ( 0 ..^ 1 ) )
6 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
7 5 6 eqtrdi 
 |-  ( x = 1 -> ( 0 ..^ x ) = { 0 } )
8 7 rexeqdv 
 |-  ( x = 1 -> ( E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
9 4 8 imbi12d 
 |-  ( x = 1 -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
10 1 9 raleqbidv 
 |-  ( x = 1 -> ( A. p e. ( RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. ( RePart ` 1 ) ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
11 fveq2 
 |-  ( x = y -> ( RePart ` x ) = ( RePart ` y ) )
12 fveq2 
 |-  ( x = y -> ( p ` x ) = ( p ` y ) )
13 12 oveq2d 
 |-  ( x = y -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` y ) ) )
14 13 eleq2d 
 |-  ( x = y -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
15 oveq2 
 |-  ( x = y -> ( 0 ..^ x ) = ( 0 ..^ y ) )
16 15 rexeqdv 
 |-  ( x = y -> ( E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
17 14 16 imbi12d 
 |-  ( x = y -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
18 11 17 raleqbidv 
 |-  ( x = y -> ( A. p e. ( RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
19 fveq2 
 |-  ( x = ( y + 1 ) -> ( RePart ` x ) = ( RePart ` ( y + 1 ) ) )
20 fveq2 
 |-  ( x = ( y + 1 ) -> ( p ` x ) = ( p ` ( y + 1 ) ) )
21 20 oveq2d 
 |-  ( x = ( y + 1 ) -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) )
22 21 eleq2d 
 |-  ( x = ( y + 1 ) -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) )
23 oveq2 
 |-  ( x = ( y + 1 ) -> ( 0 ..^ x ) = ( 0 ..^ ( y + 1 ) ) )
24 23 rexeqdv 
 |-  ( x = ( y + 1 ) -> ( E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
25 22 24 imbi12d 
 |-  ( x = ( y + 1 ) -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
26 19 25 raleqbidv 
 |-  ( x = ( y + 1 ) -> ( A. p e. ( RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. ( RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
27 fveq2 
 |-  ( x = M -> ( RePart ` x ) = ( RePart ` M ) )
28 fveq2 
 |-  ( x = M -> ( p ` x ) = ( p ` M ) )
29 28 oveq2d 
 |-  ( x = M -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` M ) ) )
30 29 eleq2d 
 |-  ( x = M -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` M ) ) ) )
31 oveq2 
 |-  ( x = M -> ( 0 ..^ x ) = ( 0 ..^ M ) )
32 31 rexeqdv 
 |-  ( x = M -> ( E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
33 30 32 imbi12d 
 |-  ( x = M -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
34 27 33 raleqbidv 
 |-  ( x = M -> ( A. p e. ( RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0 ..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. ( RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
35 0nn0 
 |-  0 e. NN0
36 fveq2 
 |-  ( i = 0 -> ( p ` i ) = ( p ` 0 ) )
37 fv0p1e1 
 |-  ( i = 0 -> ( p ` ( i + 1 ) ) = ( p ` 1 ) )
38 36 37 oveq12d 
 |-  ( i = 0 -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
39 38 eleq2d 
 |-  ( i = 0 -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
40 39 rexsng 
 |-  ( 0 e. NN0 -> ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
41 35 40 ax-mp 
 |-  ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) )
42 41 biimpri 
 |-  ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
43 42 rgenw 
 |-  A. p e. ( RePart ` 1 ) ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
44 nfv 
 |-  F/ p y e. NN
45 nfra1 
 |-  F/ p A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
46 44 45 nfan 
 |-  F/ p ( y e. NN /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
47 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
48 fzonn0p1 
 |-  ( y e. NN0 -> y e. ( 0 ..^ ( y + 1 ) ) )
49 47 48 syl 
 |-  ( y e. NN -> y e. ( 0 ..^ ( y + 1 ) ) )
50 49 ad2antrr 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> y e. ( 0 ..^ ( y + 1 ) ) )
51 fveq2 
 |-  ( i = y -> ( p ` i ) = ( p ` y ) )
52 fvoveq1 
 |-  ( i = y -> ( p ` ( i + 1 ) ) = ( p ` ( y + 1 ) ) )
53 51 52 oveq12d 
 |-  ( i = y -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
54 53 eleq2d 
 |-  ( i = y -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
55 54 adantl 
 |-  ( ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) /\ i = y ) -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
56 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
57 56 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. NN )
58 simpr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> p e. ( RePart ` ( y + 1 ) ) )
59 56 nnnn0d 
 |-  ( y e. NN -> ( y + 1 ) e. NN0 )
60 0elfz 
 |-  ( ( y + 1 ) e. NN0 -> 0 e. ( 0 ... ( y + 1 ) ) )
61 59 60 syl 
 |-  ( y e. NN -> 0 e. ( 0 ... ( y + 1 ) ) )
62 61 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... ( y + 1 ) ) )
63 57 58 62 iccpartxr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) e. RR* )
64 nn0fz0 
 |-  ( ( y + 1 ) e. NN0 <-> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
65 59 64 sylib 
 |-  ( y e. NN -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
66 65 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
67 57 58 66 iccpartxr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p ` ( y + 1 ) ) e. RR* )
68 63 67 jca 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
69 68 adantlr 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
70 elico1 
 |-  ( ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
71 69 70 syl 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
72 simp1 
 |-  ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. RR* )
73 72 adantl 
 |-  ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
74 simpl 
 |-  ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` y ) <_ X )
75 simpr3 
 |-  ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` ( y + 1 ) ) )
76 73 74 75 3jca 
 |-  ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) )
77 76 ex 
 |-  ( ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
78 77 adantl 
 |-  ( ( y e. NN /\ ( p ` y ) <_ X ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
79 78 adantr 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
80 71 79 sylbid 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
81 80 impr 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) )
82 nn0fz0 
 |-  ( y e. NN0 <-> y e. ( 0 ... y ) )
83 47 82 sylib 
 |-  ( y e. NN -> y e. ( 0 ... y ) )
84 fzelp1 
 |-  ( y e. ( 0 ... y ) -> y e. ( 0 ... ( y + 1 ) ) )
85 83 84 syl 
 |-  ( y e. NN -> y e. ( 0 ... ( y + 1 ) ) )
86 85 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... ( y + 1 ) ) )
87 57 58 86 iccpartxr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p ` y ) e. RR* )
88 87 67 jca 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
89 88 ad2ant2r 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
90 elico1 
 |-  ( ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) -> ( X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
91 89 90 syl 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
92 81 91 mpbird 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
93 50 55 92 rspcedvd 
 |-  ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. ( RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
94 93 exp43 
 |-  ( y e. NN -> ( ( p ` y ) <_ X -> ( p e. ( RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
95 94 adantr 
 |-  ( ( y e. NN /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( ( p ` y ) <_ X -> ( p e. ( RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
96 iccpartres 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p |` ( 0 ... y ) ) e. ( RePart ` y ) )
97 rspsbca 
 |-  ( ( ( p |` ( 0 ... y ) ) e. ( RePart ` y ) /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
98 vex 
 |-  p e. _V
99 98 resex 
 |-  ( p |` ( 0 ... y ) ) e. _V
100 sbcimg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
101 sbcel2 
 |-  ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) )
102 csbov12g 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) ) )
103 csbfv12 
 |-  [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 )
104 csbvarg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ p = ( p |` ( 0 ... y ) ) )
105 csbconstg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ 0 = 0 )
106 104 105 fveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
107 103 106 eqtrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
108 csbfv12 
 |-  [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y )
109 csbconstg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ y = y )
110 104 109 fveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
111 108 110 eqtrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
112 107 111 oveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
113 102 112 eqtrd 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
114 113 eleq2d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
115 101 114 bitrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
116 sbcrex 
 |-  ( [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ y ) [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
117 sbcel2 
 |-  ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
118 csbov12g 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) ) )
119 csbfv12 
 |-  [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i )
120 csbconstg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ i = i )
121 104 120 fveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
122 119 121 eqtrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
123 csbfv12 
 |-  [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) )
124 csbconstg 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) = ( i + 1 ) )
125 104 124 fveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
126 123 125 eqtrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
127 122 126 oveq12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) ) = ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) )
128 118 127 eqtrd 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) )
129 128 eleq2d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
130 117 129 bitrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
131 130 rexbidv 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( E. i e. ( 0 ..^ y ) [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
132 116 131 bitrid 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
133 115 132 imbi12d 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) ) )
134 100 133 bitrd 
 |-  ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) ) )
135 99 134 ax-mp 
 |-  ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
136 68 70 syl 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
137 136 adantr 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
138 72 adantl 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
139 simpr2 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` 0 ) <_ X )
140 xrltnle 
 |-  ( ( X e. RR* /\ ( p ` y ) e. RR* ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
141 72 87 140 syl2anr 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
142 141 exbiri 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> X < ( p ` y ) ) ) )
143 142 com23 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X < ( p ` y ) ) ) )
144 143 imp31 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` y ) )
145 138 139 144 3jca 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) )
146 63 87 jca 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
147 146 ad2antrr 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
148 elico1 
 |-  ( ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) ) )
149 147 148 syl 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) ) )
150 145 149 mpbird 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) )
151 150 ex 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
152 137 151 sylbid 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
153 0elfz 
 |-  ( y e. NN0 -> 0 e. ( 0 ... y ) )
154 47 153 syl 
 |-  ( y e. NN -> 0 e. ( 0 ... y ) )
155 154 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... y ) )
156 fvres 
 |-  ( 0 e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
157 155 156 syl 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
158 157 eqcomd 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
159 83 adantr 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... y ) )
160 fvres 
 |-  ( y e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
161 159 160 syl 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
162 161 eqcomd 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
163 158 162 oveq12d 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
164 163 eleq2d 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
165 164 biimpa 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
166 elfzofz 
 |-  ( i e. ( 0 ..^ y ) -> i e. ( 0 ... y ) )
167 166 adantl 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0 ..^ y ) ) -> i e. ( 0 ... y ) )
168 fvres 
 |-  ( i e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
169 167 168 syl 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
170 fzofzp1 
 |-  ( i e. ( 0 ..^ y ) -> ( i + 1 ) e. ( 0 ... y ) )
171 170 adantl 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( i + 1 ) e. ( 0 ... y ) )
172 fvres 
 |-  ( ( i + 1 ) e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
173 171 172 syl 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
174 173 adantlr 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
175 169 174 oveq12d 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) = ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
176 175 eleq2d 
 |-  ( ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0 ..^ y ) ) -> ( X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) <-> X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
177 176 rexbidva 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
178 nnz 
 |-  ( y e. NN -> y e. ZZ )
179 uzid 
 |-  ( y e. ZZ -> y e. ( ZZ>= ` y ) )
180 peano2uz 
 |-  ( y e. ( ZZ>= ` y ) -> ( y + 1 ) e. ( ZZ>= ` y ) )
181 fzoss2 
 |-  ( ( y + 1 ) e. ( ZZ>= ` y ) -> ( 0 ..^ y ) C_ ( 0 ..^ ( y + 1 ) ) )
182 178 179 180 181 4syl 
 |-  ( y e. NN -> ( 0 ..^ y ) C_ ( 0 ..^ ( y + 1 ) ) )
183 182 ad2antrr 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( 0 ..^ y ) C_ ( 0 ..^ ( y + 1 ) ) )
184 ssrexv 
 |-  ( ( 0 ..^ y ) C_ ( 0 ..^ ( y + 1 ) ) -> ( E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
185 183 184 syl 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
186 177 185 sylbid 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
187 165 186 embantd 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
188 187 ex 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
189 188 adantr 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
190 152 189 syld 
 |-  ( ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
191 190 ex 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
192 191 com34 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
193 192 com13 
 |-  ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
194 135 193 sylbi 
 |-  ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
195 97 194 syl 
 |-  ( ( ( p |` ( 0 ... y ) ) e. ( RePart ` y ) /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
196 195 ex 
 |-  ( ( p |` ( 0 ... y ) ) e. ( RePart ` y ) -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
197 196 com24 
 |-  ( ( p |` ( 0 ... y ) ) e. ( RePart ` y ) -> ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
198 96 197 mpcom 
 |-  ( ( y e. NN /\ p e. ( RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
199 198 ex 
 |-  ( y e. NN -> ( p e. ( RePart ` ( y + 1 ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
200 199 com24 
 |-  ( y e. NN -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( p e. ( RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
201 200 imp 
 |-  ( ( y e. NN /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( p e. ( RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
202 95 201 pm2.61d 
 |-  ( ( y e. NN /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( p e. ( RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
203 46 202 ralrimi 
 |-  ( ( y e. NN /\ A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> A. p e. ( RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
204 203 ex 
 |-  ( y e. NN -> ( A. p e. ( RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0 ..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> A. p e. ( RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0 ..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
205 10 18 26 34 43 204 nnind 
 |-  ( M e. NN -> A. p e. ( RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )