Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovolval5lem3 Structured version   Visualization version   GIF version

Theorem ovolval5lem3 45243
Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovolval5lem3.m 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))}
ovolval5lem3.q 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
Assertion
Ref Expression
ovolval5lem3 inf(𝑄, ℝ*, < ) = inf(𝑀, ℝ*, < )
Distinct variable groups:   𝐴,𝑓,𝑧,𝑦   𝑦,𝑀,𝑧   𝑄,𝑓,𝑦,𝑧
Allowed substitution hint:   𝑀(𝑓)

Proof of Theorem ovolval5lem3
Dummy variables 𝑔 𝑛 𝑤 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolval5lem3.q . . . . 5 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
21ssrab3 4078 . . . 4 𝑄 ⊆ ℝ*
3 infxrcl 13299 . . . 4 (𝑄 ⊆ ℝ* → inf(𝑄, ℝ*, < ) ∈ ℝ*)
42, 3mp1i 13 . . 3 (⊤ → inf(𝑄, ℝ*, < ) ∈ ℝ*)
5 ovolval5lem3.m . . . . 5 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))}
65ssrab3 4078 . . . 4 𝑀 ⊆ ℝ*
7 infxrcl 13299 . . . 4 (𝑀 ⊆ ℝ* → inf(𝑀, ℝ*, < ) ∈ ℝ*)
86, 7mp1i 13 . . 3 (⊤ → inf(𝑀, ℝ*, < ) ∈ ℝ*)
92a1i 11 . . . 4 (⊤ → 𝑄 ⊆ ℝ*)
106a1i 11 . . . 4 (⊤ → 𝑀 ⊆ ℝ*)
115reqabi 3455 . . . . . . 7 (𝑦𝑀 ↔ (𝑦 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))))
1211simprbi 498 . . . . . 6 (𝑦𝑀 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))
13 coeq2 5853 . . . . . . . . . . . . . . 15 (𝑔 = 𝑓 → ((,) ∘ 𝑔) = ((,) ∘ 𝑓))
1413rneqd 5932 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓))
1514unieqd 4918 . . . . . . . . . . . . 13 (𝑔 = 𝑓 ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓))
1615sseq2d 4012 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (𝐴 ran ((,) ∘ 𝑔) ↔ 𝐴 ran ((,) ∘ 𝑓)))
17 coeq2 5853 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘ 𝑓))
1817fveq2d 6885 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → (Σ^‘((vol ∘ (,)) ∘ 𝑔)) = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))
1918eqeq2d 2744 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
2016, 19anbi12d 632 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((𝐴 ran ((,) ∘ 𝑔) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
2120cbvrexvw 3236 . . . . . . . . . 10 (∃𝑔 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑔) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
2221rabbii 3439 . . . . . . . . 9 {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑔) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑔)))} = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
231, 22eqtr4i 2764 . . . . . . . 8 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑔) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑔)))}
24 simp3r 1203 . . . . . . . 8 ((𝑤 ∈ ℝ+𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))
25 eqid 2733 . . . . . . . 8 ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝑓𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓𝑚))⟩))) = (Σ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝑓𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓𝑚))⟩)))
26 elmapi 8831 . . . . . . . . 9 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ × ℝ))
27263ad2ant2 1135 . . . . . . . 8 ((𝑤 ∈ ℝ+𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓:ℕ⟶(ℝ × ℝ))
28 simp3l 1202 . . . . . . . 8 ((𝑤 ∈ ℝ+𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ran ([,) ∘ 𝑓))
29 simp1 1137 . . . . . . . 8 ((𝑤 ∈ ℝ+𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑤 ∈ ℝ+)
30 2fveq3 6886 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1st ‘(𝑓𝑚)) = (1st ‘(𝑓𝑛)))
31 oveq2 7404 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛))
3231oveq2d 7412 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑤 / (2↑𝑚)) = (𝑤 / (2↑𝑛)))
3330, 32oveq12d 7414 . . . . . . . . . 10 (𝑚 = 𝑛 → ((1st ‘(𝑓𝑚)) − (𝑤 / (2↑𝑚))) = ((1st ‘(𝑓𝑛)) − (𝑤 / (2↑𝑛))))
34 2fveq3 6886 . . . . . . . . . 10 (𝑚 = 𝑛 → (2nd ‘(𝑓𝑚)) = (2nd ‘(𝑓𝑛)))
3533, 34opeq12d 4877 . . . . . . . . 9 (𝑚 = 𝑛 → ⟨((1st ‘(𝑓𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓𝑚))⟩ = ⟨((1st ‘(𝑓𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓𝑛))⟩)
3635cbvmptv 5257 . . . . . . . 8 (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝑓𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓𝑚))⟩) = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝑓𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓𝑛))⟩)
3723, 24, 25, 27, 28, 29, 36ovolval5lem2 45242 . . . . . . 7 ((𝑤 ∈ ℝ+𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))
3837rexlimdv3a 3160 . . . . . 6 (𝑤 ∈ ℝ+ → (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)))
3912, 38mpan9 508 . . . . 5 ((𝑦𝑀𝑤 ∈ ℝ+) → ∃𝑧𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))
40393adant1 1131 . . . 4 ((⊤ ∧ 𝑦𝑀𝑤 ∈ ℝ+) → ∃𝑧𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))
419, 10, 40infleinf 43955 . . 3 (⊤ → inf(𝑄, ℝ*, < ) ≤ inf(𝑀, ℝ*, < ))
42 eqeq1 2737 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
4342anbi2d 630 . . . . . . . . 9 (𝑧 = 𝑦 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
4443rexbidv 3179 . . . . . . . 8 (𝑧 = 𝑦 → (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
4544cbvrabv 3443 . . . . . . 7 {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
46 simpr 486 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝐴 ran ((,) ∘ 𝑓)) → 𝐴 ran ((,) ∘ 𝑓))
47 ioossico 13402 . . . . . . . . . . . . . . . . . . 19 ((1st ‘(𝑓𝑛))(,)(2nd ‘(𝑓𝑛))) ⊆ ((1st ‘(𝑓𝑛))[,)(2nd ‘(𝑓𝑛)))
4847a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝑓𝑛))(,)(2nd ‘(𝑓𝑛))) ⊆ ((1st ‘(𝑓𝑛))[,)(2nd ‘(𝑓𝑛))))
4926adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶(ℝ × ℝ))
50 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
5149, 50fvovco 43763 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓𝑛))(,)(2nd ‘(𝑓𝑛))))
5249, 50fvovco 43763 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (([,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓𝑛))[,)(2nd ‘(𝑓𝑛))))
5348, 51, 523sstr4d 4027 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛))
5453ralrimiva 3147 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛))
55 ss2iun 5011 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) → 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛))
5654, 55syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛))
57 ioof 13411 . . . . . . . . . . . . . . . . . . 19 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
5857a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
59 rexpssxrxp 11246 . . . . . . . . . . . . . . . . . . 19 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
6059a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
6158, 60, 26fcoss 43780 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ((,) ∘ 𝑓):ℕ⟶𝒫 ℝ)
6261ffnd 6708 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ((,) ∘ 𝑓) Fn ℕ)
63 fniunfv 7233 . . . . . . . . . . . . . . . 16 (((,) ∘ 𝑓) Fn ℕ → 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ran ((,) ∘ 𝑓))
6462, 63syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ran ((,) ∘ 𝑓))
65 icof 43789 . . . . . . . . . . . . . . . . . . 19 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
6665a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
6766, 60, 26fcoss 43780 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ([,) ∘ 𝑓):ℕ⟶𝒫 ℝ*)
6867ffnd 6708 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ([,) ∘ 𝑓) Fn ℕ)
69 fniunfv 7233 . . . . . . . . . . . . . . . 16 (([,) ∘ 𝑓) Fn ℕ → 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ran ([,) ∘ 𝑓))
7068, 69syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ran ([,) ∘ 𝑓))
7156, 64, 703sstr3d 4026 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ran ((,) ∘ 𝑓) ⊆ ran ([,) ∘ 𝑓))
7271adantr 482 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝐴 ran ((,) ∘ 𝑓)) → ran ((,) ∘ 𝑓) ⊆ ran ([,) ∘ 𝑓))
7346, 72sstrd 3990 . . . . . . . . . . . 12 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝐴 ran ((,) ∘ 𝑓)) → 𝐴 ran ([,) ∘ 𝑓))
74 simpr 486 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))
7526voliooicof 44585 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ [,)) ∘ 𝑓))
7675fveq2d 6885 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))
7776adantr 482 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))
7874, 77eqtrd 2773 . . . . . . . . . . . 12 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))
7973, 78anim12dan 620 . . . . . . . . . . 11 ((𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))
8079ex 414 . . . . . . . . . 10 (𝑓 ∈ ((ℝ × ℝ) ↑m ℕ) → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))))
8180reximia 3082 . . . . . . . . 9 (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))
8281a1i 11 . . . . . . . 8 (𝑦 ∈ ℝ* → (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))))
8382ss2rabi 4072 . . . . . . 7 {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))}
8445, 83eqsstri 4014 . . . . . 6 {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))}
8584, 1, 53sstr4i 4023 . . . . 5 𝑄𝑀
86 infxrss 13305 . . . . 5 ((𝑄𝑀𝑀 ⊆ ℝ*) → inf(𝑀, ℝ*, < ) ≤ inf(𝑄, ℝ*, < ))
8785, 6, 86mp2an 691 . . . 4 inf(𝑀, ℝ*, < ) ≤ inf(𝑄, ℝ*, < )
8887a1i 11 . . 3 (⊤ → inf(𝑀, ℝ*, < ) ≤ inf(𝑄, ℝ*, < ))
894, 8, 41, 88xrletrid 13121 . 2 (⊤ → inf(𝑄, ℝ*, < ) = inf(𝑀, ℝ*, < ))
9089mptru 1549 1 inf(𝑄, ℝ*, < ) = inf(𝑀, ℝ*, < )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wtru 1543  wcel 2107  wral 3062  wrex 3071  {crab 3433  wss 3946  𝒫 cpw 4598  cop 4630   cuni 4904   ciun 4993   class class class wbr 5144  cmpt 5227   × cxp 5670  ran crn 5673  ccom 5676   Fn wfn 6530  wf 6531  cfv 6535  (class class class)co 7396  1st c1st 7960  2nd c2nd 7961  m cmap 8808  infcinf 9423  cr 11096  *cxr 11234   < clt 11235  cle 11236  cmin 11431   / cdiv 11858  cn 12199  2c2 12254  +crp 12961   +𝑒 cxad 13077  (,)cioo 13311  [,)cico 13313  cexp 14014  volcvol 24949  Σ^csumge0 44951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-inf2 9623  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174  ax-pre-sup 11175
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7657  df-om 7843  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8691  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fi 9393  df-sup 9424  df-inf 9425  df-oi 9492  df-dju 9883  df-card 9921  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-3 12263  df-n0 12460  df-z 12546  df-uz 12810  df-q 12920  df-rp 12962  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-ioo 13315  df-ico 13317  df-icc 13318  df-fz 13472  df-fzo 13615  df-fl 13744  df-seq 13954  df-exp 14015  df-hash 14278  df-cj 15033  df-re 15034  df-im 15035  df-sqrt 15169  df-abs 15170  df-clim 15419  df-rlim 15420  df-sum 15620  df-rest 17355  df-topgen 17376  df-psmet 20910  df-xmet 20911  df-met 20912  df-bl 20913  df-mopn 20914  df-top 22365  df-topon 22382  df-bases 22418  df-cmp 22860  df-ovol 24950  df-vol 24951  df-sumge0 44952
This theorem is referenced by:  ovolval5  45244
  Copyright terms: Public domain W3C validator