Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  oms0 Structured version   Visualization version   GIF version

Theorem oms0 32400
Description: A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
Hypotheses
Ref Expression
oms.m 𝑀 = (toOMeas‘𝑅)
oms.o (𝜑𝑄𝑉)
oms.r (𝜑𝑅:𝑄⟶(0[,]+∞))
oms.d (𝜑 → ∅ ∈ dom 𝑅)
oms.0 (𝜑 → (𝑅‘∅) = 0)
Assertion
Ref Expression
oms0 (𝜑 → (𝑀‘∅) = 0)

Proof of Theorem oms0
Dummy variables 𝑥 𝑦 𝑧 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oms.m . . 3 𝑀 = (toOMeas‘𝑅)
21fveq1i 6812 . 2 (𝑀‘∅) = ((toOMeas‘𝑅)‘∅)
3 oms.o . . . 4 (𝜑𝑄𝑉)
4 oms.r . . . 4 (𝜑𝑅:𝑄⟶(0[,]+∞))
5 0ss 4340 . . . . 5 ∅ ⊆ dom 𝑅
64fdmd 6648 . . . . . 6 (𝜑 → dom 𝑅 = 𝑄)
76unieqd 4863 . . . . 5 (𝜑 dom 𝑅 = 𝑄)
85, 7sseqtrid 3982 . . . 4 (𝜑 → ∅ ⊆ 𝑄)
9 omsfval 32397 . . . 4 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ ∅ ⊆ 𝑄) → ((toOMeas‘𝑅)‘∅) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)), (0[,]+∞), < ))
103, 4, 8, 9syl3anc 1370 . . 3 (𝜑 → ((toOMeas‘𝑅)‘∅) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)), (0[,]+∞), < ))
11 iccssxr 13241 . . . . . 6 (0[,]+∞) ⊆ ℝ*
12 xrltso 12954 . . . . . 6 < Or ℝ*
13 soss 5540 . . . . . 6 ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
1411, 12, 13mp2 9 . . . . 5 < Or (0[,]+∞)
1514a1i 11 . . . 4 (𝜑 → < Or (0[,]+∞))
16 0e0iccpnf 13270 . . . . 5 0 ∈ (0[,]+∞)
1716a1i 11 . . . 4 (𝜑 → 0 ∈ (0[,]+∞))
18 oms.d . . . . . . . . . 10 (𝜑 → ∅ ∈ dom 𝑅)
1918snssd 4753 . . . . . . . . 9 (𝜑 → {∅} ⊆ dom 𝑅)
20 p0ex 5321 . . . . . . . . . 10 {∅} ∈ V
2120elpw 4548 . . . . . . . . 9 ({∅} ∈ 𝒫 dom 𝑅 ↔ {∅} ⊆ dom 𝑅)
2219, 21sylibr 233 . . . . . . . 8 (𝜑 → {∅} ∈ 𝒫 dom 𝑅)
23 0ss 4340 . . . . . . . . 9 ∅ ⊆ {∅}
24 0ex 5245 . . . . . . . . . 10 ∅ ∈ V
25 snct 31179 . . . . . . . . . 10 (∅ ∈ V → {∅} ≼ ω)
2624, 25ax-mp 5 . . . . . . . . 9 {∅} ≼ ω
2723, 26pm3.2i 471 . . . . . . . 8 (∅ ⊆ {∅} ∧ {∅} ≼ ω)
2822, 27jctir 521 . . . . . . 7 (𝜑 → ({∅} ∈ 𝒫 dom 𝑅 ∧ (∅ ⊆ {∅} ∧ {∅} ≼ ω)))
29 unieq 4860 . . . . . . . . . 10 (𝑧 = {∅} → 𝑧 = {∅})
3029sseq2d 3962 . . . . . . . . 9 (𝑧 = {∅} → (∅ ⊆ 𝑧 ↔ ∅ ⊆ {∅}))
31 breq1 5089 . . . . . . . . 9 (𝑧 = {∅} → (𝑧 ≼ ω ↔ {∅} ≼ ω))
3230, 31anbi12d 631 . . . . . . . 8 (𝑧 = {∅} → ((∅ ⊆ 𝑧𝑧 ≼ ω) ↔ (∅ ⊆ {∅} ∧ {∅} ≼ ω)))
3332elrab 3633 . . . . . . 7 ({∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↔ ({∅} ∈ 𝒫 dom 𝑅 ∧ (∅ ⊆ {∅} ∧ {∅} ≼ ω)))
3428, 33sylibr 233 . . . . . 6 (𝜑 → {∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)})
35 simpr 485 . . . . . . . . . 10 ((𝜑𝑦 = ∅) → 𝑦 = ∅)
3635fveq2d 6815 . . . . . . . . 9 ((𝜑𝑦 = ∅) → (𝑅𝑦) = (𝑅‘∅))
37 oms.0 . . . . . . . . . 10 (𝜑 → (𝑅‘∅) = 0)
3837adantr 481 . . . . . . . . 9 ((𝜑𝑦 = ∅) → (𝑅‘∅) = 0)
3936, 38eqtrd 2776 . . . . . . . 8 ((𝜑𝑦 = ∅) → (𝑅𝑦) = 0)
4039, 18, 17esumsn 32169 . . . . . . 7 (𝜑 → Σ*𝑦 ∈ {∅} (𝑅𝑦) = 0)
4140eqcomd 2742 . . . . . 6 (𝜑 → 0 = Σ*𝑦 ∈ {∅} (𝑅𝑦))
42 esumeq1 32138 . . . . . . 7 (𝑥 = {∅} → Σ*𝑦𝑥(𝑅𝑦) = Σ*𝑦 ∈ {∅} (𝑅𝑦))
4342rspceeqv 3583 . . . . . 6 (({∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ∧ 0 = Σ*𝑦 ∈ {∅} (𝑅𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}0 = Σ*𝑦𝑥(𝑅𝑦))
4434, 41, 43syl2anc 584 . . . . 5 (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}0 = Σ*𝑦𝑥(𝑅𝑦))
45 0xr 11101 . . . . . 6 0 ∈ ℝ*
46 eqid 2736 . . . . . . 7 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
4746elrnmpt 5884 . . . . . 6 (0 ∈ ℝ* → (0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}0 = Σ*𝑦𝑥(𝑅𝑦)))
4845, 47ax-mp 5 . . . . 5 (0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}0 = Σ*𝑦𝑥(𝑅𝑦))
4944, 48sylibr 233 . . . 4 (𝜑 → 0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)))
50 nfv 1916 . . . . . . . 8 𝑥𝜑
51 nfmpt1 5194 . . . . . . . . . 10 𝑥(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
5251nfrn 5880 . . . . . . . . 9 𝑥ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
5352nfcri 2891 . . . . . . . 8 𝑥 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
5450, 53nfan 1901 . . . . . . 7 𝑥(𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)))
55 simpr 485 . . . . . . . 8 ((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) → 𝑎 = Σ*𝑦𝑥(𝑅𝑦))
56 vex 3444 . . . . . . . . 9 𝑥 ∈ V
57 nfv 1916 . . . . . . . . . . . . 13 𝑦𝜑
58 nfcv 2904 . . . . . . . . . . . . . . . 16 𝑦{𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}
59 nfcv 2904 . . . . . . . . . . . . . . . . 17 𝑦𝑥
6059nfesum1 32144 . . . . . . . . . . . . . . . 16 𝑦Σ*𝑦𝑥(𝑅𝑦)
6158, 60nfmpt 5193 . . . . . . . . . . . . . . 15 𝑦(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
6261nfrn 5880 . . . . . . . . . . . . . 14 𝑦ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
6362nfcri 2891 . . . . . . . . . . . . 13 𝑦 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))
6457, 63nfan 1901 . . . . . . . . . . . 12 𝑦(𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)))
65 nfv 1916 . . . . . . . . . . . 12 𝑦 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}
6664, 65nfan 1901 . . . . . . . . . . 11 𝑦((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)})
6760nfeq2 2921 . . . . . . . . . . 11 𝑦 𝑎 = Σ*𝑦𝑥(𝑅𝑦)
6866, 67nfan 1901 . . . . . . . . . 10 𝑦(((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦))
694ad4antr 729 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑅:𝑄⟶(0[,]+∞))
70 ssrab2 4023 . . . . . . . . . . . . . . . 16 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ⊆ 𝒫 dom 𝑅
71 simpllr 773 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)})
7270, 71sselid 3928 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑥 ∈ 𝒫 dom 𝑅)
736pweqd 4561 . . . . . . . . . . . . . . . 16 (𝜑 → 𝒫 dom 𝑅 = 𝒫 𝑄)
7473ad4antr 729 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝒫 dom 𝑅 = 𝒫 𝑄)
7572, 74eleqtrd 2839 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑥 ∈ 𝒫 𝑄)
7675elpwid 4553 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑥𝑄)
77 simpr 485 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑦𝑥)
7876, 77sseldd 3931 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → 𝑦𝑄)
7969, 78ffvelcdmd 7001 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) ∧ 𝑦𝑥) → (𝑅𝑦) ∈ (0[,]+∞))
8079ex 413 . . . . . . . . . 10 ((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) → (𝑦𝑥 → (𝑅𝑦) ∈ (0[,]+∞)))
8168, 80ralrimi 3236 . . . . . . . . 9 ((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) → ∀𝑦𝑥 (𝑅𝑦) ∈ (0[,]+∞))
8259esumcl 32134 . . . . . . . . 9 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (𝑅𝑦) ∈ (0[,]+∞)) → Σ*𝑦𝑥(𝑅𝑦) ∈ (0[,]+∞))
8356, 81, 82sylancr 587 . . . . . . . 8 ((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) → Σ*𝑦𝑥(𝑅𝑦) ∈ (0[,]+∞))
8455, 83eqeltrd 2837 . . . . . . 7 ((((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}) ∧ 𝑎 = Σ*𝑦𝑥(𝑅𝑦)) → 𝑎 ∈ (0[,]+∞))
85 vex 3444 . . . . . . . . . 10 𝑎 ∈ V
8646elrnmpt 5884 . . . . . . . . . 10 (𝑎 ∈ V → (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}𝑎 = Σ*𝑦𝑥(𝑅𝑦)))
8785, 86ax-mp 5 . . . . . . . . 9 (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}𝑎 = Σ*𝑦𝑥(𝑅𝑦))
8887biimpi 215 . . . . . . . 8 (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}𝑎 = Σ*𝑦𝑥(𝑅𝑦))
8988adantl 482 . . . . . . 7 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)}𝑎 = Σ*𝑦𝑥(𝑅𝑦))
9054, 84, 89r19.29af 3247 . . . . . 6 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → 𝑎 ∈ (0[,]+∞))
91 pnfxr 11108 . . . . . . 7 +∞ ∈ ℝ*
92 iccgelb 13214 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑎 ∈ (0[,]+∞)) → 0 ≤ 𝑎)
9345, 91, 92mp3an12 1450 . . . . . 6 (𝑎 ∈ (0[,]+∞) → 0 ≤ 𝑎)
9490, 93syl 17 . . . . 5 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → 0 ≤ 𝑎)
9511, 90sselid 3928 . . . . . 6 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → 𝑎 ∈ ℝ*)
96 xrlenlt 11119 . . . . . . 7 ((0 ∈ ℝ*𝑎 ∈ ℝ*) → (0 ≤ 𝑎 ↔ ¬ 𝑎 < 0))
9796bicomd 222 . . . . . 6 ((0 ∈ ℝ*𝑎 ∈ ℝ*) → (¬ 𝑎 < 0 ↔ 0 ≤ 𝑎))
9845, 95, 97sylancr 587 . . . . 5 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → (¬ 𝑎 < 0 ↔ 0 ≤ 𝑎))
9994, 98mpbird 256 . . . 4 ((𝜑𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦))) → ¬ 𝑎 < 0)
10015, 17, 49, 99infmin 9329 . . 3 (𝜑 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑅𝑦)), (0[,]+∞), < ) = 0)
10110, 100eqtrd 2776 . 2 (𝜑 → ((toOMeas‘𝑅)‘∅) = 0)
1022, 101eqtrid 2788 1 (𝜑 → (𝑀‘∅) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  wrex 3070  {crab 3403  Vcvv 3440  wss 3896  c0 4266  𝒫 cpw 4544  {csn 4570   cuni 4849   class class class wbr 5086  cmpt 5169   Or wor 5519  dom cdm 5607  ran crn 5608  wf 6461  cfv 6465  (class class class)co 7316  ωcom 7758  cdom 8780  infcinf 9276  0cc0 10950  +∞cpnf 11085  *cxr 11087   < clt 11088  cle 11089  [,]cicc 13161  Σ*cesum 32131  toOMeascoms 32394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-inf2 9476  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-of 7574  df-om 7759  df-1st 7877  df-2nd 7878  df-supp 8026  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-er 8547  df-map 8666  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-fsupp 9205  df-fi 9246  df-sup 9277  df-inf 9278  df-oi 9345  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-4 12117  df-5 12118  df-6 12119  df-7 12120  df-8 12121  df-9 12122  df-n0 12313  df-z 12399  df-dec 12517  df-uz 12662  df-q 12768  df-xadd 12928  df-ioo 13162  df-ioc 13163  df-ico 13164  df-icc 13165  df-fz 13319  df-fzo 13462  df-seq 13801  df-hash 14124  df-struct 16922  df-sets 16939  df-slot 16957  df-ndx 16969  df-base 16987  df-ress 17016  df-plusg 17049  df-mulr 17050  df-tset 17055  df-ple 17056  df-ds 17058  df-rest 17207  df-topn 17208  df-0g 17226  df-gsum 17227  df-topgen 17228  df-ordt 17286  df-xrs 17287  df-mre 17369  df-mrc 17370  df-acs 17372  df-ps 18358  df-tsr 18359  df-mgm 18400  df-sgrp 18449  df-mnd 18460  df-submnd 18505  df-mulg 18774  df-cntz 18996  df-cmn 19460  df-fbas 20674  df-fg 20675  df-top 22123  df-topon 22140  df-topsp 22162  df-bases 22176  df-ntr 22251  df-nei 22329  df-cn 22458  df-haus 22546  df-fil 23077  df-fm 23169  df-flim 23170  df-flf 23171  df-tsms 23358  df-esum 32132  df-oms 32395
This theorem is referenced by:  omsmeas  32426
  Copyright terms: Public domain W3C validator