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

Proof

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