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 \in ℕ \to \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))$

Proof

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

Metamath Proof Explorer

Theorem iccelpart

Proof