Metamath Proof Explorer

Theorem 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 ${⊢}{\phi }\to {M}\in ℕ$
iccpartiun.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
Assertion iccpartdisj ${⊢}{\phi }\to \underset{{i}\in \left(0..^{M}\right)}{Disj}\left[{P}\left({i}\right),{P}\left({i}+1\right)\right)$

Proof

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