iccpartiun

Description: A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020)

	Ref	Expression
Hypotheses	iccpartiun.m	$⊢ φ \to M \in ℕ$
	iccpartiun.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartiun	$⊢ φ \to [P (0), P (M)) = ⋃_{i \in (0 ..^M)} [P (i), P (i + 1))$

Proof

Step	Hyp	Ref	Expression
1		iccpartiun.m	$⊢ φ \to M \in ℕ$
2		iccpartiun.p	$⊢ φ \to P \in RePart (M)$
3		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)))$
4		fveq1	$⊢ p = P \to p (0) = P (0)$
5		fveq1	$⊢ p = P \to p (M) = P (M)$
6	4 5	oveq12d	$⊢ p = P \to [p (0), p (M)) = [P (0), P (M))$
7	6	eleq2d	$⊢ p = P \to (x \in [p (0), p (M)) \leftrightarrow x \in [P (0), P (M)))$
8		fveq1	$⊢ p = P \to p (i) = P (i)$
9		fveq1	$⊢ p = P \to p (i + 1) = P (i + 1)$
10	8 9	oveq12d	$⊢ p = P \to [p (i), p (i + 1)) = [P (i), P (i + 1))$
11	10	eleq2d	$⊢ p = P \to (x \in [p (i), p (i + 1)) \leftrightarrow x \in [P (i), P (i + 1)))$
12	11	rexbidv	$⊢ p = P \to (\exists i \in (0 ..^M) x \in [p (i), p (i + 1)) \leftrightarrow \exists i \in (0 ..^M) x \in [P (i), P (i + 1)))$
13	7 12	imbi12d	$⊢ p = P \to ((x \in [p (0), p (M)) \to \exists i \in (0 ..^M) 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))))$
14	13	rspcva	$⊢ (P \in RePart (M) \land \forall p \in RePart (M) (x \in [p (0), p (M)) \to \exists i \in (0 ..^M) x \in [p (i), p (i + 1)))) \to (x \in [P (0), P (M)) \to \exists i \in (0 ..^M) x \in [P (i), P (i + 1)))$
15	14	expcom	$⊢ \forall p \in RePart (M) (x \in [p (0), p (M)) \to \exists i \in (0 ..^M) x \in [p (i), p (i + 1))) \to (P \in RePart (M) \to (x \in [P (0), P (M)) \to \exists i \in (0 ..^M) x \in [P (i), P (i + 1))))$
16	1 3 15	3syl	$⊢ φ \to (P \in RePart (M) \to (x \in [P (0), P (M)) \to \exists i \in (0 ..^M) x \in [P (i), P (i + 1))))$
17	2 16	mpd	$⊢ φ \to (x \in [P (0), P (M)) \to \exists i \in (0 ..^M) x \in [P (i), P (i + 1)))$
18		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
19		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
20	1 18 19	3syl	$⊢ φ \to 0 \in (0 \dots M)$
21	1 2 20	iccpartxr	$⊢ φ \to P (0) \in ℝ^{*}$
22		nn0fz0	$⊢ M \in ℕ_{0} \leftrightarrow M \in (0 \dots M)$
23	22	biimpi	$⊢ M \in ℕ_{0} \to M \in (0 \dots M)$
24	1 18 23	3syl	$⊢ φ \to M \in (0 \dots M)$
25	1 2 24	iccpartxr	$⊢ φ \to P (M) \in ℝ^{*}$
26	21 25	jca	$⊢ φ \to (P (0) \in ℝ^{} \land P (M) \in ℝ^{})$
27	26	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (P (0) \in ℝ^{} \land P (M) \in ℝ^{})$
28		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
29	1 2	iccpartgel	$⊢ φ \to \forall j \in (0 \dots M) P (0) \leq P (j)$
30		fveq2	$⊢ j = i \to P (j) = P (i)$
31	30	breq2d	$⊢ j = i \to (P (0) \leq P (j) \leftrightarrow P (0) \leq P (i))$
32	31	rspcva	$⊢ (i \in (0 \dots M) \land \forall j \in (0 \dots M) P (0) \leq P (j)) \to P (0) \leq P (i)$
33	28 29 32	syl2anr	$⊢ (φ \land i \in (0 ..^M)) \to P (0) \leq P (i)$
34		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
35	1 2	iccpartleu	$⊢ φ \to \forall k \in (0 \dots M) P (k) \leq P (M)$
36		fveq2	$⊢ k = i + 1 \to P (k) = P (i + 1)$
37	36	breq1d	$⊢ k = i + 1 \to (P (k) \leq P (M) \leftrightarrow P (i + 1) \leq P (M))$
38	37	rspcva	$⊢ (i + 1 \in (0 \dots M) \land \forall k \in (0 \dots M) P (k) \leq P (M)) \to P (i + 1) \leq P (M)$
39	34 35 38	syl2anr	$⊢ (φ \land i \in (0 ..^M)) \to P (i + 1) \leq P (M)$
40		icossico	$⊢ ((P (0) \in ℝ^{} \land P (M) \in ℝ^{}) \land (P (0) \leq P (i) \land P (i + 1) \leq P (M))) \to [P (i), P (i + 1)) \subseteq [P (0), P (M))$
41	27 33 39 40	syl12anc	$⊢ (φ \land i \in (0 ..^M)) \to [P (i), P (i + 1)) \subseteq [P (0), P (M))$
42	41	sseld	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [P (i), P (i + 1)) \to x \in [P (0), P (M)))$
43	42	rexlimdva	$⊢ φ \to (\exists i \in (0 ..^M) x \in [P (i), P (i + 1)) \to x \in [P (0), P (M)))$
44	17 43	impbid	$⊢ φ \to (x \in [P (0), P (M)) \leftrightarrow \exists i \in (0 ..^M) x \in [P (i), P (i + 1)))$
45		eliun	$⊢ x \in ⋃_{i \in (0 ..^M)} [P (i), P (i + 1)) \leftrightarrow \exists i \in (0 ..^M) x \in [P (i), P (i + 1))$
46	44 45	bitr4di	$⊢ φ \to (x \in [P (0), P (M)) \leftrightarrow x \in ⋃_{i \in (0 ..^M)} [P (i), P (i + 1)))$
47	46	eqrdv	$⊢ φ \to [P (0), P (M)) = ⋃_{i \in (0 ..^M)} [P (i), P (i + 1))$

Metamath Proof Explorer

Theorem iccpartiun

Proof