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 ) ) ) )