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 ) ) ) ) )

Metamath Proof Explorer

Theorem iccelpart

Proof