Step | Hyp | Ref
| Expression |
1 | | omssubaddlem.m |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) |
2 | | omssubaddlem.e |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
3 | 2 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) |
4 | 1, 3 | readdcld 9948 |
. . . . 5
⊢ (𝜑 → ((𝑀‘𝐴) + 𝐸) ∈ ℝ) |
5 | 4 | rexrd 9968 |
. . . 4
⊢ (𝜑 → ((𝑀‘𝐴) + 𝐸) ∈
ℝ*) |
6 | | oms.o |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
7 | | oms.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
8 | | omsf 29685 |
. . . . . . . . 9
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) →
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
9 | 6, 7, 8 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞)) |
10 | | oms.m |
. . . . . . . . 9
⊢ 𝑀 = (toOMeas‘𝑅) |
11 | 10 | feq1i 5949 |
. . . . . . . 8
⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
12 | 9, 11 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
13 | | omssubaddlem.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑄) |
14 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄) |
15 | 7, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑅 = 𝑄) |
16 | 15 | unieqd 4382 |
. . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
17 | 13, 16 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ∪ dom
𝑅) |
18 | | uniexg 6853 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ 𝑉 → ∪ 𝑄 ∈ V) |
19 | 6, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑄
∈ V) |
20 | 13, 19 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ⊆ ∪ 𝑄 ∧ ∪ 𝑄
∈ V)) |
21 | | ssexg 4732 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
22 | | elpwg 4116 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
24 | 17, 23 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
25 | 12, 24 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞)) |
26 | | elxrge0 12152 |
. . . . . . 7
⊢ ((𝑀‘𝐴) ∈ (0[,]+∞) ↔ ((𝑀‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝑀‘𝐴))) |
27 | 26 | simprbi 479 |
. . . . . 6
⊢ ((𝑀‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝑀‘𝐴)) |
28 | 25, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝑀‘𝐴)) |
29 | 2 | rpge0d 11752 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝐸) |
30 | 1, 3, 28, 29 | addge0d 10482 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝑀‘𝐴) + 𝐸)) |
31 | | elxrge0 12152 |
. . . 4
⊢ (((𝑀‘𝐴) + 𝐸) ∈ (0[,]+∞) ↔ (((𝑀‘𝐴) + 𝐸) ∈ ℝ* ∧ 0 ≤
((𝑀‘𝐴) + 𝐸))) |
32 | 5, 30, 31 | sylanbrc 695 |
. . 3
⊢ (𝜑 → ((𝑀‘𝐴) + 𝐸) ∈ (0[,]+∞)) |
33 | 10 | fveq1i 6104 |
. . . . 5
⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴) |
34 | | omsfval 29683 |
. . . . . 6
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
35 | 6, 7, 13, 34 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
36 | 33, 35 | syl5req 2657 |
. . . 4
⊢ (𝜑 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) = (𝑀‘𝐴)) |
37 | 1, 2 | ltaddrpd 11781 |
. . . 4
⊢ (𝜑 → (𝑀‘𝐴) < ((𝑀‘𝐴) + 𝐸)) |
38 | 36, 37 | eqbrtrd 4605 |
. . 3
⊢ (𝜑 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + 𝐸)) |
39 | | iccssxr 12127 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
40 | | xrltso 11850 |
. . . . . 6
⊢ < Or
ℝ* |
41 | | soss 4977 |
. . . . . 6
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
42 | 39, 40, 41 | mp2 9 |
. . . . 5
⊢ < Or
(0[,]+∞) |
43 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → < Or
(0[,]+∞)) |
44 | | omscl 29684 |
. . . . . 6
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
45 | 6, 7, 24, 44 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
46 | | xrge0infss 28915 |
. . . . 5
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈
(0[,]+∞)(∀𝑡
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
48 | 43, 47 | infglb 8279 |
. . 3
⊢ (𝜑 → ((((𝑀‘𝐴) + 𝐸) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + 𝐸)) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + 𝐸))) |
49 | 32, 38, 48 | mp2and 711 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + 𝐸)) |
50 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
51 | | esumex 29418 |
. . . . . . . 8
⊢
Σ*𝑤
∈ 𝑥(𝑅‘𝑤) ∈ V |
52 | 50, 51 | elrnmpti 5297 |
. . . . . . 7
⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
53 | 52 | anbi1i 727 |
. . . . . 6
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
54 | | r19.41v 3070 |
. . . . . 6
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
(𝑢 =
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
55 | 53, 54 | bitr4i 266 |
. . . . 5
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
56 | 55 | exbii 1764 |
. . . 4
⊢
(∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
57 | | df-rex 2902 |
. . . 4
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + 𝐸) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
58 | | rexcom4 3198 |
. . . 4
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
59 | 56, 57, 58 | 3bitr4i 291 |
. . 3
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + 𝐸) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸))) |
60 | | breq1 4586 |
. . . . . 6
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + 𝐸) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸))) |
61 | 60 | biimpa 500 |
. . . . 5
⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) |
62 | 61 | exlimiv 1845 |
. . . 4
⊢
(∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) |
63 | 62 | reximi 2994 |
. . 3
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + 𝐸)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) |
64 | 59, 63 | sylbi 206 |
. 2
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + 𝐸) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) |
65 | 49, 64 | syl 17 |
1
⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) |