iccpartdisj

Description: The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020)

	Ref	Expression
Hypotheses	iccpartiun.m	$⊢ φ \to M \in ℕ$
	iccpartiun.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartdisj	$⊢ φ \to \underset{i \in (0 ..^M)}{Disj} [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		nfv	$⊢ Ⅎ i φ$
4		nfreu1	$⊢ Ⅎ i \exists! i \in (0 ..^M) p \in [P (i), P (i + 1))$
5		simpl	$⊢ (φ \land i \in (0 ..^M)) \to φ$
6	1	adantr	$⊢ (φ \land i \in (0 ..^M)) \to M \in ℕ$
7	2	adantr	$⊢ (φ \land i \in (0 ..^M)) \to P \in RePart (M)$
8		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
9		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
10	1 8 9	3syl	$⊢ φ \to 0 \in (0 \dots M)$
11	10	adantr	$⊢ (φ \land i \in (0 ..^M)) \to 0 \in (0 \dots M)$
12	6 7 11	iccpartxr	$⊢ (φ \land i \in (0 ..^M)) \to P (0) \in ℝ^{*}$
13		nn0fz0	$⊢ M \in ℕ_{0} \leftrightarrow M \in (0 \dots M)$
14	13	biimpi	$⊢ M \in ℕ_{0} \to M \in (0 \dots M)$
15	1 8 14	3syl	$⊢ φ \to M \in (0 \dots M)$
16	15	adantr	$⊢ (φ \land i \in (0 ..^M)) \to M \in (0 \dots M)$
17	6 7 16	iccpartxr	$⊢ (φ \land i \in (0 ..^M)) \to P (M) \in ℝ^{*}$
18	1 2	iccpartgel	$⊢ φ \to \forall j \in (0 \dots M) P (0) \leq P (j)$
19		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
20	19	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
21		fveq2	$⊢ j = i \to P (j) = P (i)$
22	21	breq2d	$⊢ j = i \to (P (0) \leq P (j) \leftrightarrow P (0) \leq P (i))$
23	22	rspcv	$⊢ i \in (0 \dots M) \to (\forall j \in (0 \dots M) P (0) \leq P (j) \to P (0) \leq P (i))$
24	20 23	syl	$⊢ (φ \land i \in (0 ..^M)) \to (\forall j \in (0 \dots M) P (0) \leq P (j) \to P (0) \leq P (i))$
25	24	ex	$⊢ φ \to (i \in (0 ..^M) \to (\forall j \in (0 \dots M) P (0) \leq P (j) \to P (0) \leq P (i)))$
26	18 25	mpid	$⊢ φ \to (i \in (0 ..^M) \to P (0) \leq P (i))$
27	26	imp	$⊢ (φ \land i \in (0 ..^M)) \to P (0) \leq P (i)$
28	1 2	iccpartleu	$⊢ φ \to \forall j \in (0 \dots M) P (j) \leq P (M)$
29		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
30	29	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
31		fveq2	$⊢ j = i + 1 \to P (j) = P (i + 1)$
32	31	breq1d	$⊢ j = i + 1 \to (P (j) \leq P (M) \leftrightarrow P (i + 1) \leq P (M))$
33	32	rspcv	$⊢ i + 1 \in (0 \dots M) \to (\forall j \in (0 \dots M) P (j) \leq P (M) \to P (i + 1) \leq P (M))$
34	30 33	syl	$⊢ (φ \land i \in (0 ..^M)) \to (\forall j \in (0 \dots M) P (j) \leq P (M) \to P (i + 1) \leq P (M))$
35	34	ex	$⊢ φ \to (i \in (0 ..^M) \to (\forall j \in (0 \dots M) P (j) \leq P (M) \to P (i + 1) \leq P (M)))$
36	28 35	mpid	$⊢ φ \to (i \in (0 ..^M) \to P (i + 1) \leq P (M))$
37	36	imp	$⊢ (φ \land i \in (0 ..^M)) \to P (i + 1) \leq P (M)$
38		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))$
39	12 17 27 37 38	syl22anc	$⊢ (φ \land i \in (0 ..^M)) \to [P (i), P (i + 1)) \subseteq [P (0), P (M))$
40	39	sseld	$⊢ (φ \land i \in (0 ..^M)) \to (p \in [P (i), P (i + 1)) \to p \in [P (0), P (M)))$
41	1 2	icceuelpart	$⊢ (φ \land p \in [P (0), P (M))) \to \exists! i \in (0 ..^M) p \in [P (i), P (i + 1))$
42	5 40 41	syl6an	$⊢ (φ \land i \in (0 ..^M)) \to (p \in [P (i), P (i + 1)) \to \exists! i \in (0 ..^M) p \in [P (i), P (i + 1)))$
43	42	ex	$⊢ φ \to (i \in (0 ..^M) \to (p \in [P (i), P (i + 1)) \to \exists! i \in (0 ..^M) p \in [P (i), P (i + 1))))$
44	3 4 43	rexlimd	$⊢ φ \to (\exists i \in (0 ..^M) p \in [P (i), P (i + 1)) \to \exists! i \in (0 ..^M) p \in [P (i), P (i + 1)))$
45		rmo5	$⊢ \exists^{*} i \in (0 ..^M) p \in [P (i), P (i + 1)) \leftrightarrow (\exists i \in (0 ..^M) p \in [P (i), P (i + 1)) \to \exists! i \in (0 ..^M) p \in [P (i), P (i + 1)))$
46	44 45	sylibr	$⊢ φ \to \exists^{*} i \in (0 ..^M) p \in [P (i), P (i + 1))$
47	46	alrimiv	$⊢ φ \to \forall p \exists^{*} i \in (0 ..^M) p \in [P (i), P (i + 1))$
48		df-disj	$⊢ \underset{i \in (0 ..^M)}{Disj} [P (i), P (i + 1)) \leftrightarrow \forall p \exists^{*} i \in (0 ..^M) p \in [P (i), P (i + 1))$
49	47 48	sylibr	$⊢ φ \to \underset{i \in (0 ..^M)}{Disj} [P (i), P (i + 1))$

Metamath Proof Explorer

Theorem iccpartdisj

Proof