ovolval4 - Mathbox for Glauco Siliprandi

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

Theorem ovolval4 39345

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 39341, but here 𝑓 may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

**Hypotheses**
Ref	Expression
ovolval4.a	⊢ (𝜑 → 𝐴 ⊆ ℝ)
ovolval4.m	⊢ 𝑀 = {𝑦 ∈ ℝ^* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑_𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^{^}‘((vol ∘ (,)) ∘ 𝑓)))}

**Assertion**
Ref	Expression
ovolval4	⊢ (𝜑 → (vol‘𝐴) = inf(𝑀, ℝ^, < ))

Distinct variable groups: 𝐴,𝑓,𝑦 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑓) 𝑀(𝑦,𝑓)

Proof of Theorem ovolval4 Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovolval4.a	. 2 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
2		ovolval4.m	. 2 ⊢ 𝑀 = {𝑦 ∈ ℝ^* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑_𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^{^}‘((vol ∘ (,)) ∘ 𝑓)))}
3		fveq2 6088	. . . . 5 ⊢ (𝑘 = 𝑛 → (𝑓‘𝑘) = (𝑓‘𝑛))
4	3	fveq2d 6092	. . . 4 ⊢ (𝑘 = 𝑛 → (1^st ‘(𝑓‘𝑘)) = (1^st ‘(𝑓‘𝑛)))
5	3	fveq2d 6092	. . . . . 6 ⊢ (𝑘 = 𝑛 → (2^nd ‘(𝑓‘𝑘)) = (2^nd ‘(𝑓‘𝑛)))
6	4, 5	breq12d 4590	. . . . 5 ⊢ (𝑘 = 𝑛 → ((1^st ‘(𝑓‘𝑘)) ≤ (2^nd ‘(𝑓‘𝑘)) ↔ (1^st ‘(𝑓‘𝑛)) ≤ (2^nd ‘(𝑓‘𝑛))))
7	6, 5, 4	ifbieq12d 4062	. . . 4 ⊢ (𝑘 = 𝑛 → if((1^st ‘(𝑓‘𝑘)) ≤ (2^nd ‘(𝑓‘𝑘)), (2^nd ‘(𝑓‘𝑘)), (1^st ‘(𝑓‘𝑘))) = if((1^st ‘(𝑓‘𝑛)) ≤ (2^nd ‘(𝑓‘𝑛)), (2^nd ‘(𝑓‘𝑛)), (1^st ‘(𝑓‘𝑛))))
8	4, 7	opeq12d 4342	. . 3 ⊢ (𝑘 = 𝑛 → ⟨(1^st ‘(𝑓‘𝑘)), if((1^st ‘(𝑓‘𝑘)) ≤ (2^nd ‘(𝑓‘𝑘)), (2^nd ‘(𝑓‘𝑘)), (1^st ‘(𝑓‘𝑘)))⟩ = ⟨(1^st ‘(𝑓‘𝑛)), if((1^st ‘(𝑓‘𝑛)) ≤ (2^nd ‘(𝑓‘𝑛)), (2^nd ‘(𝑓‘𝑛)), (1^st ‘(𝑓‘𝑛)))⟩)
9	8	cbvmptv 4672	. 2 ⊢ (𝑘 ∈ ℕ ↦ ⟨(1^st ‘(𝑓‘𝑘)), if((1^st ‘(𝑓‘𝑘)) ≤ (2^nd ‘(𝑓‘𝑘)), (2^nd ‘(𝑓‘𝑘)), (1^st ‘(𝑓‘𝑘)))⟩) = (𝑛 ∈ ℕ ↦ ⟨(1^st ‘(𝑓‘𝑛)), if((1^st ‘(𝑓‘𝑛)) ≤ (2^nd ‘(𝑓‘𝑛)), (2^nd ‘(𝑓‘𝑛)), (1^st ‘(𝑓‘𝑛)))⟩)
10	1, 2, 9	ovolval4lem2 39344	1 ⊢ (𝜑 → (vol‘𝐴) = inf(𝑀, ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 = wceq 1474 ∃wrex 2896 {crab 2899 ⊆ wss 3539 ifcif 4035 ⟨cop 4130 ∪ cuni 4366 class class class wbr 4577 ↦ cmpt 4637 × cxp 5026 ran crn 5029 ∘ ccom 5032 ‘cfv 5790 (class class class)co 6527 1^st c1st 7034 2^nd c2nd 7035 ↑_𝑚 cmap 7721 infcinf 8207 ℝcr 9791 ℝ^*cxr 9929 < clt 9930 ≤ cle 9931 ℕcn 10867 (,)cioo 12002 vol*covol 22955 volcvol 22956 Σ^{^}csumge0 39059

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2032 ax-13 2232 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6824 ax-inf2 8398 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-pre-sup 9870

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4939 df-id 4943 df-po 4949 df-so 4950 df-fr 4987 df-se 4988 df-we 4989 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-res 5040 df-ima 5041 df-pred 5583 df-ord 5629 df-on 5630 df-lim 5631 df-suc 5632 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-f1 5795 df-fo 5796 df-f1o 5797 df-fv 5798 df-isom 5799 df-riota 6489 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-of 6772 df-om 6935 df-1st 7036 df-2nd 7037 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-2o 7425 df-oadd 7428 df-er 7606 df-map 7723 df-pm 7724 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-fi 8177 df-sup 8208 df-inf 8209 df-oi 8275 df-card 8625 df-cda 8850 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-div 10534 df-nn 10868 df-2 10926 df-3 10927 df-n0 11140 df-z 11211 df-uz 11520 df-q 11621 df-rp 11665 df-xneg 11778 df-xadd 11779 df-xmul 11780 df-ioo 12006 df-ico 12008 df-icc 12009 df-fz 12153 df-fzo 12290 df-fl 12410 df-seq 12619 df-exp 12678 df-hash 12935 df-cj 13633 df-re 13634 df-im 13635 df-sqrt 13769 df-abs 13770 df-clim 14013 df-rlim 14014 df-sum 14211 df-rest 15852 df-topgen 15873 df-psmet 19505 df-xmet 19506 df-met 19507 df-bl 19508 df-mopn 19509 df-top 20463 df-bases 20464 df-topon 20465 df-cmp 20942 df-ovol 22957 df-vol 22958 df-sumge0 39060

This theorem is referenced by: ovolval5 39349

W3C validator