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 ⊢ φ → M ∈ ℕ
iccpartiun.p ⊢ φ → P ∈ RePart ⁡ M
Assertion iccpartdisj ⊢ φ → Disj i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1

Proof

Step Hyp Ref Expression
1 iccpartiun.m ⊢ φ → M ∈ ℕ
2 iccpartiun.p ⊢ φ → P ∈ RePart ⁡ M
3 nfv ⊢ Ⅎ i φ
4 nfreu1 ⊢ Ⅎ i ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
5 simpl ⊢ φ ∧ i ∈ 0 ..^ M → φ
6 1 adantr ⊢ φ ∧ i ∈ 0 ..^ M → M ∈ ℕ
7 2 adantr ⊢ φ ∧ i ∈ 0 ..^ M → P ∈ RePart ⁡ M
8 nnnn0 ⊢ M ∈ ℕ → M ∈ ℕ 0
9 0elfz ⊢ M ∈ ℕ 0 → 0 ∈ 0 … M
10 1 8 9 3syl ⊢ φ → 0 ∈ 0 … M
11 10 adantr ⊢ φ ∧ i ∈ 0 ..^ M → 0 ∈ 0 … M
12 6 7 11 iccpartxr ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ 0 ∈ ℝ *
13 nn0fz0 ⊢ M ∈ ℕ 0 ↔ M ∈ 0 … M
14 13 biimpi ⊢ M ∈ ℕ 0 → M ∈ 0 … M
15 1 8 14 3syl ⊢ φ → M ∈ 0 … M
16 15 adantr ⊢ φ ∧ i ∈ 0 ..^ M → M ∈ 0 … M
17 6 7 16 iccpartxr ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ M ∈ ℝ *
18 1 2 iccpartgel ⊢ φ → ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j
19 elfzofz ⊢ i ∈ 0 ..^ M → i ∈ 0 … M
20 19 adantl ⊢ φ ∧ i ∈ 0 ..^ M → i ∈ 0 … M
21 fveq2 ⊢ j = i → P ⁡ j = P ⁡ i
22 21 breq2d ⊢ j = i → P ⁡ 0 ≤ P ⁡ j ↔ P ⁡ 0 ≤ P ⁡ i
23 22 rspcv ⊢ i ∈ 0 … M → ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j → P ⁡ 0 ≤ P ⁡ i
24 20 23 syl ⊢ φ ∧ i ∈ 0 ..^ M → ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j → P ⁡ 0 ≤ P ⁡ i
25 24 ex ⊢ φ → i ∈ 0 ..^ M → ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j → P ⁡ 0 ≤ P ⁡ i
26 18 25 mpid ⊢ φ → i ∈ 0 ..^ M → P ⁡ 0 ≤ P ⁡ i
27 26 imp ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ 0 ≤ P ⁡ i
28 1 2 iccpartleu ⊢ φ → ∀ j ∈ 0 … M P ⁡ j ≤ P ⁡ M
29 fzofzp1 ⊢ i ∈ 0 ..^ M → i + 1 ∈ 0 … M
30 29 adantl ⊢ φ ∧ i ∈ 0 ..^ M → i + 1 ∈ 0 … M
31 fveq2 ⊢ j = i + 1 → P ⁡ j = P ⁡ i + 1
32 31 breq1d ⊢ j = i + 1 → P ⁡ j ≤ P ⁡ M ↔ P ⁡ i + 1 ≤ P ⁡ M
33 32 rspcv ⊢ i + 1 ∈ 0 … M → ∀ j ∈ 0 … M P ⁡ j ≤ P ⁡ M → P ⁡ i + 1 ≤ P ⁡ M
34 30 33 syl ⊢ φ ∧ i ∈ 0 ..^ M → ∀ j ∈ 0 … M P ⁡ j ≤ P ⁡ M → P ⁡ i + 1 ≤ P ⁡ M
35 34 ex ⊢ φ → i ∈ 0 ..^ M → ∀ j ∈ 0 … M P ⁡ j ≤ P ⁡ M → P ⁡ i + 1 ≤ P ⁡ M
36 28 35 mpid ⊢ φ → i ∈ 0 ..^ M → P ⁡ i + 1 ≤ P ⁡ M
37 36 imp ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ i + 1 ≤ P ⁡ M
38 icossico ⊢ P ⁡ 0 ∈ ℝ * ∧ P ⁡ M ∈ ℝ * ∧ P ⁡ 0 ≤ P ⁡ i ∧ P ⁡ i + 1 ≤ P ⁡ M → P ⁡ i P ⁡ i + 1 ⊆ P ⁡ 0 P ⁡ M
39 12 17 27 37 38 syl22anc ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ i P ⁡ i + 1 ⊆ P ⁡ 0 P ⁡ M
40 39 sseld ⊢ φ ∧ i ∈ 0 ..^ M → p ∈ P ⁡ i P ⁡ i + 1 → p ∈ P ⁡ 0 P ⁡ M
41 1 2 icceuelpart ⊢ φ ∧ p ∈ P ⁡ 0 P ⁡ M → ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
42 5 40 41 syl6an ⊢ φ ∧ i ∈ 0 ..^ M → p ∈ P ⁡ i P ⁡ i + 1 → ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
43 42 ex ⊢ φ → i ∈ 0 ..^ M → p ∈ P ⁡ i P ⁡ i + 1 → ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
44 3 4 43 rexlimd ⊢ φ → ∃ i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1 → ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
45 rmo5 ⊢ ∃* i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1 ↔ ∃ i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1 → ∃! i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
46 44 45 sylibr ⊢ φ → ∃* i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
47 46 alrimiv ⊢ φ → ∀ p ∃* i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
48 df-disj ⊢ Disj i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1 ↔ ∀ p ∃* i ∈ 0 ..^ M p ∈ P ⁡ i P ⁡ i + 1
49 47 48 sylibr ⊢ φ → Disj i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1