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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartiun.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartdisj ( 𝜑 → Disj 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )

Proof

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