# Metamath Proof Explorer

## Theorem icceuelpart

Description: An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (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 icceuelpart ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \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 2 adantr ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
4 iccelpart ${⊢}{M}\in ℕ\to \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
5 1 4 syl ${⊢}{\phi }\to \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
6 5 adantr ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
7 fveq1 ${⊢}{p}={P}\to {p}\left(0\right)={P}\left(0\right)$
8 fveq1 ${⊢}{p}={P}\to {p}\left({M}\right)={P}\left({M}\right)$
9 7 8 oveq12d ${⊢}{p}={P}\to \left[{p}\left(0\right),{p}\left({M}\right)\right)=\left[{P}\left(0\right),{P}\left({M}\right)\right)$
10 9 eleq2d ${⊢}{p}={P}\to \left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)↔{X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)$
11 fveq1 ${⊢}{p}={P}\to {p}\left({i}\right)={P}\left({i}\right)$
12 fveq1 ${⊢}{p}={P}\to {p}\left({i}+1\right)={P}\left({i}+1\right)$
13 11 12 oveq12d ${⊢}{p}={P}\to \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)=\left[{P}\left({i}\right),{P}\left({i}+1\right)\right)$
14 13 eleq2d ${⊢}{p}={P}\to \left({X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)$
15 14 rexbidv ${⊢}{p}={P}\to \left(\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)$
16 10 15 imbi12d ${⊢}{p}={P}\to \left(\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\left({X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)\right)$
17 16 rspcva ${⊢}\left({P}\in \mathrm{RePart}\left({M}\right)\wedge \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left({X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)$
18 17 adantld ${⊢}\left({P}\in \mathrm{RePart}\left({M}\right)\wedge \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left(\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)$
19 18 com12 ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \left(\left({P}\in \mathrm{RePart}\left({M}\right)\wedge \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\right)$
20 3 6 19 mp2and ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)$
21 1 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {M}\in ℕ$
22 2 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
23 elfzofz ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in \left(0\dots {M}\right)$
24 23 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}\in \left(0\dots {M}\right)$
25 21 22 24 iccpartxr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
26 fzofzp1 ${⊢}{i}\in \left(0..^{M}\right)\to {i}+1\in \left(0\dots {M}\right)$
27 26 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}+1\in \left(0\dots {M}\right)$
28 21 22 27 iccpartxr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {P}\left({i}+1\right)\in {ℝ}^{*}$
29 25 28 jca ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\right)$
30 29 adantrr ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\right)$
31 elico1 ${⊢}\left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\right)\to \left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\right)$
32 30 31 syl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\right)$
33 1 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {M}\in ℕ$
34 2 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
35 elfzofz ${⊢}{j}\in \left(0..^{M}\right)\to {j}\in \left(0\dots {M}\right)$
36 35 adantl ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
37 33 34 36 iccpartxr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {P}\left({j}\right)\in {ℝ}^{*}$
38 fzofzp1 ${⊢}{j}\in \left(0..^{M}\right)\to {j}+1\in \left(0\dots {M}\right)$
39 38 adantl ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {j}+1\in \left(0\dots {M}\right)$
40 33 34 39 iccpartxr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {P}\left({j}+1\right)\in {ℝ}^{*}$
41 37 40 jca ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to \left({P}\left({j}\right)\in {ℝ}^{*}\wedge {P}\left({j}+1\right)\in {ℝ}^{*}\right)$
42 41 adantrl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({j}\right)\in {ℝ}^{*}\wedge {P}\left({j}+1\right)\in {ℝ}^{*}\right)$
43 elico1 ${⊢}\left({P}\left({j}\right)\in {ℝ}^{*}\wedge {P}\left({j}+1\right)\in {ℝ}^{*}\right)\to \left({X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)$
44 42 43 syl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)$
45 32 44 anbi12d ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge {X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)↔\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\right)$
46 elfzoelz ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in ℤ$
47 46 zred ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in ℝ$
48 elfzoelz ${⊢}{j}\in \left(0..^{M}\right)\to {j}\in ℤ$
49 48 zred ${⊢}{j}\in \left(0..^{M}\right)\to {j}\in ℝ$
50 47 49 anim12i ${⊢}\left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\to \left({i}\in ℝ\wedge {j}\in ℝ\right)$
51 50 adantl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({i}\in ℝ\wedge {j}\in ℝ\right)$
52 lttri4 ${⊢}\left({i}\in ℝ\wedge {j}\in ℝ\right)\to \left({i}<{j}\vee {i}={j}\vee {j}<{i}\right)$
53 51 52 syl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({i}<{j}\vee {i}={j}\vee {j}<{i}\right)$
54 1 2 icceuelpartlem ${⊢}{\phi }\to \left(\left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\to \left({i}<{j}\to {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\right)$
55 54 imp31 ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {i}<{j}\right)\to {P}\left({i}+1\right)\le {P}\left({j}\right)$
56 simpl ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to {X}\in {ℝ}^{*}$
57 28 adantrr ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to {P}\left({i}+1\right)\in {ℝ}^{*}$
58 57 adantl ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to {P}\left({i}+1\right)\in {ℝ}^{*}$
59 37 adantrl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to {P}\left({j}\right)\in {ℝ}^{*}$
60 59 adantl ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to {P}\left({j}\right)\in {ℝ}^{*}$
61 nltle2tri ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\wedge {P}\left({j}\right)\in {ℝ}^{*}\right)\to ¬\left({X}<{P}\left({i}+1\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\wedge {P}\left({j}\right)\le {X}\right)$
62 56 58 60 61 syl3anc ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to ¬\left({X}<{P}\left({i}+1\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\wedge {P}\left({j}\right)\le {X}\right)$
63 62 pm2.21d ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to \left(\left({X}<{P}\left({i}+1\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\wedge {P}\left({j}\right)\le {X}\right)\to {i}={j}\right)$
64 63 3expd ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to \left({X}<{P}\left({i}+1\right)\to \left({P}\left({i}+1\right)\le {P}\left({j}\right)\to \left({P}\left({j}\right)\le {X}\to {i}={j}\right)\right)\right)$
65 64 ex ${⊢}{X}\in {ℝ}^{*}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({X}<{P}\left({i}+1\right)\to \left({P}\left({i}+1\right)\le {P}\left({j}\right)\to \left({P}\left({j}\right)\le {X}\to {i}={j}\right)\right)\right)\right)$
66 65 com23 ${⊢}{X}\in {ℝ}^{*}\to \left({X}<{P}\left({i}+1\right)\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({i}+1\right)\le {P}\left({j}\right)\to \left({P}\left({j}\right)\le {X}\to {i}={j}\right)\right)\right)\right)$
67 66 com25 ${⊢}{X}\in {ℝ}^{*}\to \left({P}\left({j}\right)\le {X}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({i}+1\right)\le {P}\left({j}\right)\to \left({X}<{P}\left({i}+1\right)\to {i}={j}\right)\right)\right)\right)$
68 67 imp4b ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to \left({X}<{P}\left({i}+1\right)\to {i}={j}\right)\right)$
69 68 com23 ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\right)\to \left({X}<{P}\left({i}+1\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to {i}={j}\right)\right)$
70 69 3adant3 ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left({X}<{P}\left({i}+1\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to {i}={j}\right)\right)$
71 70 com12 ${⊢}{X}<{P}\left({i}+1\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to {i}={j}\right)\right)$
72 71 3ad2ant3 ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to {i}={j}\right)\right)$
73 72 imp ${⊢}\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to {i}={j}\right)$
74 73 com12 ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({i}+1\right)\le {P}\left({j}\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
75 55 74 syldan ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {i}<{j}\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
76 75 expcom ${⊢}{i}<{j}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)\right)$
77 2a1 ${⊢}{i}={j}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)\right)$
78 1 2 icceuelpartlem ${⊢}{\phi }\to \left(\left({j}\in \left(0..^{M}\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({j}<{i}\to {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\right)$
79 78 ancomsd ${⊢}{\phi }\to \left(\left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\to \left({j}<{i}\to {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\right)$
80 79 imp31 ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {j}<{i}\right)\to {P}\left({j}+1\right)\le {P}\left({i}\right)$
81 40 adantrl ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to {P}\left({j}+1\right)\in {ℝ}^{*}$
82 81 adantl ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to {P}\left({j}+1\right)\in {ℝ}^{*}$
83 25 adantrr ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
84 83 adantl ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
85 nltle2tri ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({j}+1\right)\in {ℝ}^{*}\wedge {P}\left({i}\right)\in {ℝ}^{*}\right)\to ¬\left({X}<{P}\left({j}+1\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\wedge {P}\left({i}\right)\le {X}\right)$
86 56 82 84 85 syl3anc ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to ¬\left({X}<{P}\left({j}+1\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\wedge {P}\left({i}\right)\le {X}\right)$
87 86 pm2.21d ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to \left(\left({X}<{P}\left({j}+1\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\wedge {P}\left({i}\right)\le {X}\right)\to {i}={j}\right)$
88 87 3expd ${⊢}\left({X}\in {ℝ}^{*}\wedge \left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\right)\to \left({X}<{P}\left({j}+1\right)\to \left({P}\left({j}+1\right)\le {P}\left({i}\right)\to \left({P}\left({i}\right)\le {X}\to {i}={j}\right)\right)\right)$
89 88 ex ${⊢}{X}\in {ℝ}^{*}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({X}<{P}\left({j}+1\right)\to \left({P}\left({j}+1\right)\le {P}\left({i}\right)\to \left({P}\left({i}\right)\le {X}\to {i}={j}\right)\right)\right)\right)$
90 89 com23 ${⊢}{X}\in {ℝ}^{*}\to \left({X}<{P}\left({j}+1\right)\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({j}+1\right)\le {P}\left({i}\right)\to \left({P}\left({i}\right)\le {X}\to {i}={j}\right)\right)\right)\right)$
91 90 imp4b ${⊢}\left({X}\in {ℝ}^{*}\wedge {X}<{P}\left({j}+1\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to \left({P}\left({i}\right)\le {X}\to {i}={j}\right)\right)$
92 91 com23 ${⊢}\left({X}\in {ℝ}^{*}\wedge {X}<{P}\left({j}+1\right)\right)\to \left({P}\left({i}\right)\le {X}\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to {i}={j}\right)\right)$
93 92 3adant2 ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left({P}\left({i}\right)\le {X}\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to {i}={j}\right)\right)$
94 93 com12 ${⊢}{P}\left({i}\right)\le {X}\to \left(\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to {i}={j}\right)\right)$
95 94 3ad2ant2 ${⊢}\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to {i}={j}\right)\right)$
96 95 imp ${⊢}\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to \left(\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to {i}={j}\right)$
97 96 com12 ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {P}\left({j}+1\right)\le {P}\left({i}\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
98 80 97 syldan ${⊢}\left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\wedge {j}<{i}\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
99 98 expcom ${⊢}{j}<{i}\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)\right)$
100 76 77 99 3jaoi ${⊢}\left({i}<{j}\vee {i}={j}\vee {j}<{i}\right)\to \left(\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)\right)$
101 53 100 mpcom ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left(\left({X}\in {ℝ}^{*}\wedge {P}\left({i}\right)\le {X}\wedge {X}<{P}\left({i}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {P}\left({j}\right)\le {X}\wedge {X}<{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
102 45 101 sylbid ${⊢}\left({\phi }\wedge \left({i}\in \left(0..^{M}\right)\wedge {j}\in \left(0..^{M}\right)\right)\right)\to \left(\left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge {X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
103 102 ralrimivva ${⊢}{\phi }\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge {X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
104 103 adantr ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge {X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)$
105 fveq2 ${⊢}{i}={j}\to {P}\left({i}\right)={P}\left({j}\right)$
106 fvoveq1 ${⊢}{i}={j}\to {P}\left({i}+1\right)={P}\left({j}+1\right)$
107 105 106 oveq12d ${⊢}{i}={j}\to \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)=\left[{P}\left({j}\right),{P}\left({j}+1\right)\right)$
108 107 eleq2d ${⊢}{i}={j}\to \left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)↔{X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)$
109 108 reu4 ${⊢}\exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)↔\left(\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)\wedge {X}\in \left[{P}\left({j}\right),{P}\left({j}+1\right)\right)\right)\to {i}={j}\right)\right)$
110 20 104 109 sylanbrc ${⊢}\left({\phi }\wedge {X}\in \left[{P}\left(0\right),{P}\left({M}\right)\right)\right)\to \exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right)$