| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovolval5lem3.q | . . . . 5
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} | 
| 2 | 1 | ssrab3 4081 | . . . 4
⊢ 𝑄 ⊆
ℝ* | 
| 3 |  | infxrcl 13376 | . . . 4
⊢ (𝑄 ⊆ ℝ*
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) | 
| 4 | 2, 3 | mp1i 13 | . . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) | 
| 5 |  | ovolval5lem3.m | . . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} | 
| 6 | 5 | ssrab3 4081 | . . . 4
⊢ 𝑀 ⊆
ℝ* | 
| 7 |  | infxrcl 13376 | . . . 4
⊢ (𝑀 ⊆ ℝ*
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) | 
| 8 | 6, 7 | mp1i 13 | . . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) | 
| 9 | 2 | a1i 11 | . . . 4
⊢ (⊤
→ 𝑄 ⊆
ℝ*) | 
| 10 | 6 | a1i 11 | . . . 4
⊢ (⊤
→ 𝑀 ⊆
ℝ*) | 
| 11 | 5 | reqabi 3459 | . . . . . . 7
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) | 
| 12 | 11 | simprbi 496 | . . . . . 6
⊢ (𝑦 ∈ 𝑀 → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | 
| 13 |  | coeq2 5868 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → ((,) ∘ 𝑔) = ((,) ∘ 𝑓)) | 
| 14 | 13 | rneqd 5948 | . . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓)) | 
| 15 | 14 | unieqd 4919 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → ∪ ran ((,)
∘ 𝑔) = ∪ ran ((,) ∘ 𝑓)) | 
| 16 | 15 | sseq2d 4015 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓))) | 
| 17 |  | coeq2 5868 | . . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝑓)) | 
| 18 | 17 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) | 
| 19 | 18 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 20 | 16, 19 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) | 
| 21 | 20 | cbvrexvw 3237 | . . . . . . . . . 10
⊢
(∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 22 | 21 | rabbii 3441 | . . . . . . . . 9
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} | 
| 23 | 1, 22 | eqtr4i 2767 | . . . . . . . 8
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑔 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} | 
| 24 |  | simp3r 1202 | . . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) | 
| 25 |  | eqid 2736 | . . . . . . . 8
⊢
(Σ^‘((vol ∘ (,)) ∘
(𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) =
(Σ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) | 
| 26 |  | elmapi 8890 | . . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) | 
| 27 | 26 | 3ad2ant2 1134 | . . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓:ℕ⟶(ℝ ×
ℝ)) | 
| 28 |  | simp3l 1201 | . . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) | 
| 29 |  | simp1 1136 | . . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑤 ∈ ℝ+) | 
| 30 |  | 2fveq3 6910 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) | 
| 31 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) | 
| 32 | 31 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑤 / (2↑𝑚)) = (𝑤 / (2↑𝑛))) | 
| 33 | 30, 32 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))) = ((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛)))) | 
| 34 |  | 2fveq3 6910 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) | 
| 35 | 33, 34 | opeq12d 4880 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈((1st
‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) | 
| 36 | 35 | cbvmptv 5254 | . . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) | 
| 37 | 23, 24, 25, 27, 28, 29, 36 | ovolval5lem2 46673 | . . . . . . 7
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) | 
| 38 | 37 | rexlimdv3a 3158 | . . . . . 6
⊢ (𝑤 ∈ ℝ+
→ (∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))) | 
| 39 | 12, 38 | mpan9 506 | . . . . 5
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) | 
| 40 | 39 | 3adant1 1130 | . . . 4
⊢
((⊤ ∧ 𝑦
∈ 𝑀 ∧ 𝑤 ∈ ℝ+)
→ ∃𝑧 ∈
𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) | 
| 41 | 9, 10, 40 | infleinf 45388 | . . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ≤ inf(𝑀, ℝ*, <
)) | 
| 42 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 43 | 42 | anbi2d 630 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) | 
| 44 | 43 | rexbidv 3178 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) | 
| 45 | 44 | cbvrabv 3446 | . . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} | 
| 46 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) | 
| 47 |  | ioossico 13479 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))) | 
| 48 | 47 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛))) ⊆ ((1st
‘(𝑓‘𝑛))[,)(2nd
‘(𝑓‘𝑛)))) | 
| 49 | 26 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) | 
| 50 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) | 
| 51 | 49, 50 | fvovco 45203 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) | 
| 52 | 49, 50 | fvovco 45203 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (([,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛)))) | 
| 53 | 48, 51, 52 | 3sstr4d 4038 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) | 
| 54 | 53 | ralrimiva 3145 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) | 
| 55 |  | ss2iun 5009 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) | 
| 57 |  | ioof 13488 | . . . . . . . . . . . . . . . . . . 19
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ | 
| 58 | 57 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (,):(ℝ* ×
ℝ*)⟶𝒫 ℝ) | 
| 59 |  | rexpssxrxp 11307 | . . . . . . . . . . . . . . . . . . 19
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆
(ℝ* × ℝ*)) | 
| 61 | 58, 60, 26 | fcoss 45220 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) | 
| 62 | 61 | ffnd 6736 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓) Fn ℕ) | 
| 63 |  | fniunfv 7268 | . . . . . . . . . . . . . . . 16
⊢ (((,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ∪ ran ((,)
∘ 𝑓)) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) = ∪
ran ((,) ∘ 𝑓)) | 
| 65 |  | icof 45229 | . . . . . . . . . . . . . . . . . . 19
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* | 
| 66 | 65 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → [,):(ℝ* ×
ℝ*)⟶𝒫 ℝ*) | 
| 67 | 66, 60, 26 | fcoss 45220 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) | 
| 68 | 67 | ffnd 6736 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓) Fn ℕ) | 
| 69 |  | fniunfv 7268 | . . . . . . . . . . . . . . . 16
⊢ (([,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ∪ ran ([,)
∘ 𝑓)) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛) = ∪
ran ([,) ∘ 𝑓)) | 
| 71 | 56, 64, 70 | 3sstr3d 4037 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪ ran
((,) ∘ 𝑓) ⊆
∪ ran ([,) ∘ 𝑓)) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓)) | 
| 73 | 46, 72 | sstrd 3993 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ([,) ∘ 𝑓)) | 
| 74 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) | 
| 75 | 26 | voliooicof 46016 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ [,)) ∘
𝑓)) | 
| 76 | 75 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) | 
| 77 | 76 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) | 
| 78 | 74, 77 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) | 
| 79 | 73, 78 | anim12dan 619 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | 
| 80 | 79 | ex 412 | . . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) | 
| 81 | 80 | reximia 3080 | . . . . . . . . 9
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | 
| 82 | 81 | a1i 11 | . . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) | 
| 83 | 82 | ss2rabi 4076 | . . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} | 
| 84 | 45, 83 | eqsstri 4029 | . . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} | 
| 85 | 84, 1, 5 | 3sstr4i 4034 | . . . . 5
⊢ 𝑄 ⊆ 𝑀 | 
| 86 |  | infxrss 13382 | . . . . 5
⊢ ((𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ*) →
inf(𝑀, ℝ*,
< ) ≤ inf(𝑄,
ℝ*, < )) | 
| 87 | 85, 6, 86 | mp2an 692 | . . . 4
⊢ inf(𝑀, ℝ*, < )
≤ inf(𝑄,
ℝ*, < ) | 
| 88 | 87 | a1i 11 | . . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ≤ inf(𝑄, ℝ*, <
)) | 
| 89 | 4, 8, 41, 88 | xrletrid 13198 | . 2
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) = inf(𝑀, ℝ*, <
)) | 
| 90 | 89 | mptru 1546 | 1
⊢ inf(𝑄, ℝ*, < ) =
inf(𝑀, ℝ*,
< ) |