Step | Hyp | Ref
| Expression |
1 | | ovolval5lem3.q |
. . . . 5
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
2 | | ssrab2 3650 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆
ℝ* |
3 | 1, 2 | eqsstri 3598 |
. . . 4
⊢ 𝑄 ⊆
ℝ* |
4 | | infxrcl 12035 |
. . . 4
⊢ (𝑄 ⊆ ℝ*
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
5 | 3, 4 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
6 | | ovolval5lem3.m |
. . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
7 | | ssrab2 3650 |
. . . . 5
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⊆
ℝ* |
8 | 6, 7 | eqsstri 3598 |
. . . 4
⊢ 𝑀 ⊆
ℝ* |
9 | | infxrcl 12035 |
. . . 4
⊢ (𝑀 ⊆ ℝ*
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
10 | 8, 9 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
11 | 3 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑄 ⊆
ℝ*) |
12 | 8 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑀 ⊆
ℝ*) |
13 | | simpr 476 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
14 | 6 | rabid3 38285 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
15 | 14 | biimpi 205 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑀 → (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
16 | 15 | simprd 478 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑀 → ∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
18 | | coeq2 5202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑓 → ((,) ∘ 𝑔) = ((,) ∘ 𝑓)) |
19 | 18 | rneqd 5274 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑓 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓)) |
20 | 19 | unieqd 4382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → ∪ ran ((,)
∘ 𝑔) = ∪ ran ((,) ∘ 𝑓)) |
21 | 20 | sseq2d 3596 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓))) |
22 | | coeq2 5202 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑓 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝑓)) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
24 | 23 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
25 | 21, 24 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
26 | 25 | cbvrexv 3148 |
. . . . . . . . . . . . 13
⊢
(∃𝑔 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
27 | 26 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ*
→ (∃𝑔 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
28 | 27 | rabbiia 3161 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑔 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
29 | 1, 28 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑔 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
30 | | simp3r 1083 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
31 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Σ^‘((vol ∘ (,)) ∘
(𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) =
(Σ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) |
32 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
33 | 32 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
34 | | simp3l 1082 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) |
35 | | simp1 1054 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑤 ∈ ℝ+) |
36 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑓‘𝑚) = (𝑓‘𝑛)) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
38 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) |
39 | 38 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑤 / (2↑𝑚)) = (𝑤 / (2↑𝑛))) |
40 | 37, 39 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))) = ((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛)))) |
41 | 36 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
42 | 40, 41 | opeq12d 4348 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈((1st
‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
43 | 42 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
44 | 29, 30, 31, 33, 34, 35, 43 | ovolval5lem2 39543 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
45 | 44 | 3exp 1256 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ+
→ (𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ) → ((𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)))) |
46 | 45 | rexlimdv 3012 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ+
→ (∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))) |
47 | 46 | imp 444 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ+
∧ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
48 | 13, 17, 47 | syl2anc 691 |
. . . . 5
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
49 | 48 | 3adant1 1072 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ 𝑀 ∧ 𝑤 ∈ ℝ+)
→ ∃𝑧 ∈
𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
50 | 11, 12, 49 | infleinf 38529 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ≤ inf(𝑀, ℝ*, <
)) |
51 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
52 | 51 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
53 | 52 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
54 | 53 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
55 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) |
56 | | ioossico 12133 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛))) ⊆ ((1st
‘(𝑓‘𝑛))[,)(2nd
‘(𝑓‘𝑛)))) |
58 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
59 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
60 | 58, 59 | fvovco 38376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) |
61 | 58, 59 | fvovco 38376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (([,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛)))) |
62 | 60, 61 | sseq12d 3597 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → ((((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) ↔ ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))))) |
63 | 57, 62 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
64 | 63 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
65 | | ss2iun 4472 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛)) |
67 | | ioof 12142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (,):(ℝ*
× ℝ*)⟶𝒫 ℝ) |
69 | | rexpssxrxp 9963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (ℝ × ℝ)
⊆ (ℝ* × ℝ*)) |
71 | 32, 70 | fssd 5970 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) |
72 | | fco 5971 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝑓:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) |
73 | 68, 71, 72 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) |
74 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((,)
∘ 𝑓):ℕ⟶𝒫 ℝ →
((,) ∘ 𝑓) Fn
ℕ) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((,) ∘ 𝑓) Fn ℕ) |
76 | | fniunfv 6409 |
. . . . . . . . . . . . . . . . . 18
⊢ (((,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ∪ ran ((,)
∘ 𝑓)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ∪ ran ((,)
∘ 𝑓)) |
78 | | icof 38406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → [,):(ℝ*
× ℝ*)⟶𝒫
ℝ*) |
80 | | fco 5971 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(([,):(ℝ* × ℝ*)⟶𝒫
ℝ* ∧ 𝑓:ℕ⟶(ℝ* ×
ℝ*)) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) |
81 | 79, 71, 80 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) |
82 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (([,)
∘ 𝑓):ℕ⟶𝒫
ℝ* → ([,) ∘ 𝑓) Fn ℕ) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ([,) ∘ 𝑓) Fn ℕ) |
84 | | fniunfv 6409 |
. . . . . . . . . . . . . . . . . 18
⊢ (([,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ∪ ran ([,)
∘ 𝑓)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ∪ ran ([,)
∘ 𝑓)) |
86 | 77, 85 | sseq12d 3597 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛) ↔ ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓))) |
87 | 66, 86 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓)) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓)) |
89 | 55, 88 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ([,) ∘ 𝑓)) |
90 | 89 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) |
91 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
92 | 32 | voliooicof 38889 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((vol ∘ (,)) ∘
𝑓) = ((vol ∘ [,))
∘ 𝑓)) |
93 | 92 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
95 | 91, 94 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
96 | 95 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
97 | 90, 96 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
98 | 97 | ex 449 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
99 | 98 | reximia 2992 |
. . . . . . . . 9
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
100 | 99 | rgenw 2908 |
. . . . . . . 8
⊢
∀𝑦 ∈
ℝ* (∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
101 | | ss2rab 3641 |
. . . . . . . 8
⊢ ({𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ↔ ∀𝑦 ∈ ℝ*
(∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
102 | 100, 101 | mpbir 220 |
. . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
103 | 54, 102 | eqsstri 3598 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
104 | 1, 6 | sseq12i 3594 |
. . . . . 6
⊢ (𝑄 ⊆ 𝑀 ↔ {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))}) |
105 | 103, 104 | mpbir 220 |
. . . . 5
⊢ 𝑄 ⊆ 𝑀 |
106 | | infxrss 12040 |
. . . . 5
⊢ ((𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ*) →
inf(𝑀, ℝ*,
< ) ≤ inf(𝑄,
ℝ*, < )) |
107 | 105, 8, 106 | mp2an 704 |
. . . 4
⊢ inf(𝑀, ℝ*, < )
≤ inf(𝑄,
ℝ*, < ) |
108 | 107 | a1i 11 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ≤ inf(𝑄, ℝ*, <
)) |
109 | 5, 10, 50, 108 | xrletrid 11862 |
. 2
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) = inf(𝑀, ℝ*, <
)) |
110 | 109 | trud 1484 |
1
⊢ inf(𝑄, ℝ*, < ) =
inf(𝑀, ℝ*,
< ) |