Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iccelpart Structured version   Visualization version   Unicode version
Theorem iccelpart 41369
Description: An element of any partitioned half opened interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.)
Assertion
Ref Expression
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 ) ) ) ) )
Distinct variable groups:   i, M, p   i, X, p
Proof of Theorem iccelpart
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6191 . . 3 |- ( x = 1 -> (RePart ` x ) = (RePart ` 1 ) )
2 fveq2 6191 . . . . . 6 |- ( x = 1 -> ( p ` x ) = ( p ` 1 ) )
32oveq2d 6666 . . . . 5 |- ( x = 1 -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
43eleq2d 2687 . . . 4 |- ( x = 1 -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
5 oveq2 6658 . . . . . 6 |- ( x = 1 -> ( 0..^ x ) = ( 0..^ 1 ) )
6 fzo01 12550 . . . . . 6 |- ( 0..^ 1 ) = { 0 }
75, 6syl6eq 2672 . . . . 5 |- ( x = 1 -> ( 0..^ x ) = { 0 } )
87rexeqdv 3145 . . . 4 |- ( 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 ) ) ) ) )
94, 8imbi12d 334 . . 3 |- ( 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 ) ) ) ) ) )
101, 9raleqbidv 3152 . 2 |- ( 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 6191 . . 3 |- ( x = y -> (RePart ` x ) = (RePart ` y ) )
12 fveq2 6191 . . . . . 6 |- ( x = y -> ( p ` x ) = ( p ` y ) )
1312oveq2d 6666 . . . . 5 |- ( x = y -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` y ) ) )
1413eleq2d 2687 . . . 4 |- ( x = y -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
15 oveq2 6658 . . . . 5 |- ( x = y -> ( 0..^ x ) = ( 0..^ y ) )
1615rexeqdv 3145 . . . 4 |- ( 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 ) ) ) ) )
1714, 16imbi12d 334 . . 3 |- ( 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 ) ) ) ) ) )
1811, 17raleqbidv 3152 . 2 |- ( 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 6191 . . 3 |- ( x = ( y + 1 ) -> (RePart ` x ) = (RePart ` ( y + 1 ) ) )
20 fveq2 6191 . . . . . 6 |- ( x = ( y + 1 ) -> ( p ` x ) = ( p ` ( y + 1 ) ) )
2120oveq2d 6666 . . . . 5 |- ( x = ( y + 1 ) -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) )
2221eleq2d 2687 . . . 4 |- ( x = ( y + 1 ) -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) )
23 oveq2 6658 . . . . 5 |- ( x = ( y + 1 ) -> ( 0..^ x ) = ( 0..^ ( y + 1 ) ) )
2423rexeqdv 3145 . . . 4 |- ( 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 ) ) ) ) )
2522, 24imbi12d 334 . . 3 |- ( 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 ) ) ) ) ) )
2619, 25raleqbidv 3152 . 2 |- ( 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 6191 . . 3 |- ( x = M -> (RePart ` x ) = (RePart ` M ) )
28 fveq2 6191 . . . . . 6 |- ( x = M -> ( p ` x ) = ( p ` M ) )
2928oveq2d 6666 . . . . 5 |- ( x = M -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` M ) ) )
3029eleq2d 2687 . . . 4 |- ( x = M -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` M ) ) ) )
31 oveq2 6658 . . . . 5 |- ( x = M -> ( 0..^ x ) = ( 0..^ M ) )
3231rexeqdv 3145 . . . 4 |- ( 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 ) ) ) ) )
3330, 32imbi12d 334 . . 3 |- ( 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 ) ) ) ) ) )
3427, 33raleqbidv 3152 . 2 |- ( 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 11307 . . . . 5 |- 0 e. NN0
36 fveq2 6191 . . . . . . . 8 |- ( i = 0 -> ( p ` i ) = ( p ` 0 ) )
37 oveq1 6657 . . . . . . . . . 10 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
38 0p1e1 11132 . . . . . . . . . 10 |- ( 0 + 1 ) = 1
3937, 38syl6eq 2672 . . . . . . . . 9 |- ( i = 0 -> ( i + 1 ) = 1 )
4039fveq2d 6195 . . . . . . . 8 |- ( i = 0 -> ( p ` ( i + 1 ) ) = ( p ` 1 ) )
4136, 40oveq12d 6668 . . . . . . 7 |- ( i = 0 -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
4241eleq2d 2687 . . . . . 6 |- ( i = 0 -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
4342rexsng 4219 . . . . 5 |- ( 0 e. NN0 -> ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
4435, 43ax-mp 5 . . . 4 |- ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) )
4544biimpri 218 . . 3 |- ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
4645rgenw 2924 . 2 |- A. p e. (RePart ` 1 ) ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
47 nfv 1843 . . . . 5 |- F/ p y e. NN
48 nfra1 2941 . . . . 5 |- 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 ) ) ) )
4947, 48nfan 1828 . . . 4 |- 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 ) ) ) ) )
50 nnnn0 11299 . . . . . . . . . 10 |- ( y e. NN -> y e. NN0 )
51 fzonn0p1 12544 . . . . . . . . . 10 |- ( y e. NN0 -> y e. ( 0..^ ( y + 1 ) ) )
5250, 51syl 17 . . . . . . . . 9 |- ( y e. NN -> y e. ( 0..^ ( y + 1 ) ) )
5352ad2antrr 762 . . . . . . . 8 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> y e. ( 0..^ ( y + 1 ) ) )
54 fveq2 6191 . . . . . . . . . . 11 |- ( i = y -> ( p ` i ) = ( p ` y ) )
55 oveq1 6657 . . . . . . . . . . . 12 |- ( i = y -> ( i + 1 ) = ( y + 1 ) )
5655fveq2d 6195 . . . . . . . . . . 11 |- ( i = y -> ( p ` ( i + 1 ) ) = ( p ` ( y + 1 ) ) )
5754, 56oveq12d 6668 . . . . . . . . . 10 |- ( i = y -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
5857eleq2d 2687 . . . . . . . . 9 |- ( i = y -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
5958adantl 482 . . . . . . . 8 |- ( ( ( ( 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 ) ) ) ) )
60 peano2nn 11032 . . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. NN )
6160adantr 481 . . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. NN )
62 simpr 477 . . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> p e. (RePart ` ( y + 1 ) ) )
6360nnnn0d 11351 . . . . . . . . . . . . . . . . 17 |- ( y e. NN -> ( y + 1 ) e. NN0 )
64 0elfz 12436 . . . . . . . . . . . . . . . . 17 |- ( ( y + 1 ) e. NN0 -> 0 e. ( 0 ... ( y + 1 ) ) )
6563, 64syl 17 . . . . . . . . . . . . . . . 16 |- ( y e. NN -> 0 e. ( 0 ... ( y + 1 ) ) )
6665adantr 481 . . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... ( y + 1 ) ) )
6761, 62, 66iccpartxr 41355 . . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) e. RR* )
68 nn0fz0 12437 . . . . . . . . . . . . . . . . 17 |- ( ( y + 1 ) e. NN0 <-> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
6963, 68sylib 208 . . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
7069adantr 481 . . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
7161, 62, 70iccpartxr 41355 . . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` ( y + 1 ) ) e. RR* )
7267, 71jca 554 . . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
7372adantlr 751 . . . . . . . . . . . 12 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
74 elico1 12218 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) ) )
7573, 74syl 17 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) )
76 simp1 1061 . . . . . . . . . . . . . . . 16 |- ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. RR* )
7776adantl 482 . . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
78 simpl 473 . . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` y ) <_ X )
79 simpr3 1069 . . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` ( y + 1 ) ) )
8077, 78, 793jca 1242 . . . . . . . . . . . . . 14 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) )
8180ex 450 . . . . . . . . . . . . 13 |- ( ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
8281adantl 482 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) ) )
8382adantr 481 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) )
8475, 83sylbid 230 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
8584impr 649 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
86 nn0fz0 12437 . . . . . . . . . . . . . . . 16 |- ( y e. NN0 <-> y e. ( 0 ... y ) )
8750, 86sylib 208 . . . . . . . . . . . . . . 15 |- ( y e. NN -> y e. ( 0 ... y ) )
88 fzelp1 12393 . . . . . . . . . . . . . . 15 |- ( y e. ( 0 ... y ) -> y e. ( 0 ... ( y + 1 ) ) )
8987, 88syl 17 . . . . . . . . . . . . . 14 |- ( y e. NN -> y e. ( 0 ... ( y + 1 ) ) )
9089adantr 481 . . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... ( y + 1 ) ) )
9161, 62, 90iccpartxr 41355 . . . . . . . . . . . 12 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) e. RR* )
9291, 71jca 554 . . . . . . . . . . 11 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
9392ad2ant2r 783 . . . . . . . . . 10 |- ( ( ( 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* ) )
94 elico1 12218 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
9593, 94syl 17 . . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
9685, 95mpbird 247 . . . . . . . 8 |- ( ( ( 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 ) ) ) )
9753, 59, 96rspcedvd 3317 . . . . . . 7 |- ( ( ( 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 ) ) ) )
9897exp43 640 . . . . . 6 |- ( 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 ) ) ) ) ) ) )
9998adantr 481 . . . . 5 |- ( ( 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 ) ) ) ) ) ) )
100 iccpartres 41354 . . . . . . . . 9 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p |` ( 0 ... y ) ) e. (RePart ` y ) )
101 rspsbca 3519 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) ) )
102 vex 3203 . . . . . . . . . . . . . . 15 |- p e. _V
103102resex 5443 . . . . . . . . . . . . . 14 |- ( p |` ( 0 ... y ) ) e. _V
104 sbcimg 3477 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) ) )
105 sbcel2 3989 . . . . . . . . . . . . . . . . 17 |- ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) )
106 csbov12g 6689 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) )
107 csbfv12 6231 . . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 )
108 csbvarg 4003 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ p = ( p |` ( 0 ... y ) ) )
109 csbconstg 3546 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ 0 = 0 )
110108, 109fveq12d 6197 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
111107, 110syl5eq 2668 . . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
112 csbfv12 6231 . . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y )
113 csbconstg 3546 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ y = y )
114108, 113fveq12d 6197 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
115112, 114syl5eq 2668 . . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
116111, 115oveq12d 6668 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) )
117106, 116eqtrd 2656 . . . . . . . . . . . . . . . . . 18 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
118117eleq2d 2687 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
119105, 118syl5bb 272 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
120 sbcrex 3514 . . . . . . . . . . . . . . . . 17 |- ( [. ( 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 ) ) ) )
121 sbcel2 3989 . . . . . . . . . . . . . . . . . . 19 |- ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
122 csbov12g 6689 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) )
123 csbfv12 6231 . . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i )
124 csbconstg 3546 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ i = i )
125108, 124fveq12d 6197 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
126123, 125syl5eq 2668 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
127 csbfv12 6231 . . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) )
128 csbconstg 3546 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) = ( i + 1 ) )
129108, 128fveq12d 6197 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
130127, 129syl5eq 2668 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
131126, 130oveq12d 6668 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) )
132122, 131eqtrd 2656 . . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) )
133132eleq2d 2687 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
134121, 133syl5bb 272 . . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) )
135134rexbidv 3052 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) ) )
136120, 135syl5bb 272 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) ) )
137119, 136imbi12d 334 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) ) )
138104, 137bitrd 268 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
139103, 138ax-mp 5 . . . . . . . . . . . . 13 |- ( [. ( 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 ) ) ) ) )
14072, 74syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
141140adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
14276adantl 482 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
143 simpr2 1068 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` 0 ) <_ X )
144 xrltnle 10105 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( X e. RR* /\ ( p ` y ) e. RR* ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
14576, 91, 144syl2anr 495 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
146145exbiri 652 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> X < ( p ` y ) ) ) )
147146com23 86 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X < ( p ` y ) ) ) )
148147imp31 448 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` y ) )
149142, 143, 1483jca 1242 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) )
15067, 91jca 554 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
151150ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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* ) )
152 elico1 12218 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) ) )
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) )
154149, 153mpbird 247 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) ) )
155154ex 450 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
156141, 155sylbid 230 . . . . . . . . . . . . . . . . 17 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
157 0elfz 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. NN0 -> 0 e. ( 0 ... y ) )
15850, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. NN -> 0 e. ( 0 ... y ) )
159158adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... y ) )
160 fvres 6207 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
161159, 160syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
162161eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
16387adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... y ) )
164 fvres 6207 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
166165eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
167162, 166oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
168167eleq2d 2687 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
169168biimpa 501 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
170 elfzofz 12485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i e. ( 0..^ y ) -> i e. ( 0 ... y ) )
171170adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> i e. ( 0 ... y ) )
172 fvres 6207 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
174 fzofzp1 12565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i e. ( 0..^ y ) -> ( i + 1 ) e. ( 0 ... y ) )
175174adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ i e. ( 0..^ y ) ) -> ( i + 1 ) e. ( 0 ... y ) )
176 fvres 6207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( i + 1 ) e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
177175, 176syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
178177adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) )
179173, 178oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) ) )
180179eleq2d 2687 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) ) ) )
181180rexbidva 3049 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) ) )
182 nnz 11399 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. NN -> y e. ZZ )
183 uzid 11702 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ZZ -> y e. ( ZZ>= ` y ) )
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. NN -> y e. ( ZZ>= ` y ) )
185 peano2uz 11741 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ZZ>= ` y ) -> ( y + 1 ) e. ( ZZ>= ` y ) )
186 fzoss2 12496 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y + 1 ) e. ( ZZ>= ` y ) -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
187184, 185, 1863syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. NN -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
188187ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
189 ssrexv 3667 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) ) ) )
190188, 189syl 17 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) ) )
191181, 190sylbid 230 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) ) )
192169, 191embantd 59 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) ) )
193192ex 450 . . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) ) )
194193adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) ) ) )
195156, 194syld 47 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) ) ) )
196195ex 450 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) ) ) )
197196com34 91 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) ) )
198197com13 88 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) ) ) )
199139, 198sylbi 207 . . . . . . . . . . . 12 |- ( [. ( 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 ) ) ) ) ) ) )
200101, 199syl 17 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) ) ) )
201200ex 450 . . . . . . . . . 10 |- ( ( 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 ) ) ) ) ) ) ) )
202201com24 95 . . . . . . . . 9 |- ( ( 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 ) ) ) ) ) ) ) )
203100, 202mpcom 38 . . . . . . . 8 |- ( ( 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 ) ) ) ) ) ) )
204203ex 450 . . . . . . 7 |- ( 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 ) ) ) ) ) ) ) )
205204com24 95 . . . . . 6 |- ( 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 ) ) ) ) ) ) ) )
206205imp 445 . . . . 5 |- ( ( 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 ) ) ) ) ) ) )
20799, 206pm2.61d 170 . . . 4 |- ( ( 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 ) ) ) ) ) )
20849, 207ralrimi 2957 . . 3 |- ( ( 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 ) ) ) ) )
209208ex 450 . 2 |- ( 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 ) ) ) ) ) )
21010, 18, 26, 34, 46, 209nnind 11038 1 |- ( 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 ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   [_csb 3533   C_ wss 3574   {csn 4177   class class class wbr 4653   |` cres 5116   ` cfv 5888  (class class class)co 6650   0cc0 9936   1c1 9937   + caddc 9939   RR*cxr 10073   < clt 10074   <_ cle 10075   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   [,)cico 12177   ...cfz 12326  ..^cfzo 12465  RePartciccp 41349
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-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-fal 1489  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-map 7859  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-ico 12181  df-fz 12327  df-fzo 12466  df-iccp 41350
This theorem is referenced by:  iccpartiun  41370  icceuelpart  41372  bgoldbtbnd  41697
  Copyright terms: Public domain W3C validator