Metamath Proof Explorer

Theorem iccpartiun

Description: A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m ⊢ φ → M ∈ ℕ
iccpartiun.p ⊢ φ → P ∈ RePart ⁡ M
Assertion iccpartiun ⊢ φ → P ⁡ 0 P ⁡ M = ⋃ i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1

Proof

Step Hyp Ref Expression
1 iccpartiun.m ⊢ φ → M ∈ ℕ
2 iccpartiun.p ⊢ φ → P ∈ RePart ⁡ M
3 iccelpart ⊢ M ∈ ℕ → ∀ p ∈ RePart ⁡ M x ∈ p ⁡ 0 p ⁡ M → ∃ i ∈ 0 ..^ M x ∈ p ⁡ i p ⁡ i + 1
4 fveq1 ⊢ p = P → p ⁡ 0 = P ⁡ 0
5 fveq1 ⊢ p = P → p ⁡ M = P ⁡ M
6 4 5 oveq12d ⊢ p = P → p ⁡ 0 p ⁡ M = P ⁡ 0 P ⁡ M
7 6 eleq2d ⊢ p = P → x ∈ p ⁡ 0 p ⁡ M ↔ x ∈ P ⁡ 0 P ⁡ M
8 fveq1 ⊢ p = P → p ⁡ i = P ⁡ i
9 fveq1 ⊢ p = P → p ⁡ i + 1 = P ⁡ i + 1
10 8 9 oveq12d ⊢ p = P → p ⁡ i p ⁡ i + 1 = P ⁡ i P ⁡ i + 1
11 10 eleq2d ⊢ p = P → x ∈ p ⁡ i p ⁡ i + 1 ↔ x ∈ P ⁡ i P ⁡ i + 1
12 11 rexbidv ⊢ p = P → ∃ i ∈ 0 ..^ M x ∈ p ⁡ i p ⁡ i + 1 ↔ ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
13 7 12 imbi12d ⊢ p = P → x ∈ p ⁡ 0 p ⁡ M → ∃ i ∈ 0 ..^ M x ∈ p ⁡ i p ⁡ i + 1 ↔ x ∈ P ⁡ 0 P ⁡ M → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
14 13 rspcva ⊢ P ∈ RePart ⁡ M ∧ ∀ p ∈ RePart ⁡ M x ∈ p ⁡ 0 p ⁡ M → ∃ i ∈ 0 ..^ M x ∈ p ⁡ i p ⁡ i + 1 → x ∈ P ⁡ 0 P ⁡ M → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
15 14 expcom ⊢ ∀ p ∈ RePart ⁡ M x ∈ p ⁡ 0 p ⁡ M → ∃ i ∈ 0 ..^ M x ∈ p ⁡ i p ⁡ i + 1 → P ∈ RePart ⁡ M → x ∈ P ⁡ 0 P ⁡ M → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
16 1 3 15 3syl ⊢ φ → P ∈ RePart ⁡ M → x ∈ P ⁡ 0 P ⁡ M → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
17 2 16 mpd ⊢ φ → x ∈ P ⁡ 0 P ⁡ M → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
18 nnnn0 ⊢ M ∈ ℕ → M ∈ ℕ 0
19 0elfz ⊢ M ∈ ℕ 0 → 0 ∈ 0 … M
20 1 18 19 3syl ⊢ φ → 0 ∈ 0 … M
21 1 2 20 iccpartxr ⊢ φ → P ⁡ 0 ∈ ℝ *
22 nn0fz0 ⊢ M ∈ ℕ 0 ↔ M ∈ 0 … M
23 22 biimpi ⊢ M ∈ ℕ 0 → M ∈ 0 … M
24 1 18 23 3syl ⊢ φ → M ∈ 0 … M
25 1 2 24 iccpartxr ⊢ φ → P ⁡ M ∈ ℝ *
26 21 25 jca ⊢ φ → P ⁡ 0 ∈ ℝ * ∧ P ⁡ M ∈ ℝ *
27 26 adantr ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ 0 ∈ ℝ * ∧ P ⁡ M ∈ ℝ *
28 elfzofz ⊢ i ∈ 0 ..^ M → i ∈ 0 … M
29 1 2 iccpartgel ⊢ φ → ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j
30 fveq2 ⊢ j = i → P ⁡ j = P ⁡ i
31 30 breq2d ⊢ j = i → P ⁡ 0 ≤ P ⁡ j ↔ P ⁡ 0 ≤ P ⁡ i
32 31 rspcva ⊢ i ∈ 0 … M ∧ ∀ j ∈ 0 … M P ⁡ 0 ≤ P ⁡ j → P ⁡ 0 ≤ P ⁡ i
33 28 29 32 syl2anr ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ 0 ≤ P ⁡ i
34 fzofzp1 ⊢ i ∈ 0 ..^ M → i + 1 ∈ 0 … M
35 1 2 iccpartleu ⊢ φ → ∀ k ∈ 0 … M P ⁡ k ≤ P ⁡ M
36 fveq2 ⊢ k = i + 1 → P ⁡ k = P ⁡ i + 1
37 36 breq1d ⊢ k = i + 1 → P ⁡ k ≤ P ⁡ M ↔ P ⁡ i + 1 ≤ P ⁡ M
38 37 rspcva ⊢ i + 1 ∈ 0 … M ∧ ∀ k ∈ 0 … M P ⁡ k ≤ P ⁡ M → P ⁡ i + 1 ≤ P ⁡ M
39 34 35 38 syl2anr ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ i + 1 ≤ P ⁡ M
40 icossico ⊢ P ⁡ 0 ∈ ℝ * ∧ P ⁡ M ∈ ℝ * ∧ P ⁡ 0 ≤ P ⁡ i ∧ P ⁡ i + 1 ≤ P ⁡ M → P ⁡ i P ⁡ i + 1 ⊆ P ⁡ 0 P ⁡ M
41 27 33 39 40 syl12anc ⊢ φ ∧ i ∈ 0 ..^ M → P ⁡ i P ⁡ i + 1 ⊆ P ⁡ 0 P ⁡ M
42 41 sseld ⊢ φ ∧ i ∈ 0 ..^ M → x ∈ P ⁡ i P ⁡ i + 1 → x ∈ P ⁡ 0 P ⁡ M
43 42 rexlimdva ⊢ φ → ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1 → x ∈ P ⁡ 0 P ⁡ M
44 17 43 impbid ⊢ φ → x ∈ P ⁡ 0 P ⁡ M ↔ ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
45 eliun ⊢ x ∈ ⋃ i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1 ↔ ∃ i ∈ 0 ..^ M x ∈ P ⁡ i P ⁡ i + 1
46 44 45 bitr4di ⊢ φ → x ∈ P ⁡ 0 P ⁡ M ↔ x ∈ ⋃ i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1
47 46 eqrdv ⊢ φ → P ⁡ 0 P ⁡ M = ⋃ i ∈ 0 ..^ M P ⁡ i P ⁡ i + 1