ovnf - Mathbox for Glauco Siliprandi

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

Theorem ovnf 44346

Description: The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypothesis**
Ref	Expression
ovnf.1	⊢ (𝜑 → 𝑋 ∈ Fin)

**Assertion**
Ref	Expression
ovnf	⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑_m 𝑋)⟶(0[,]+∞))

Proof of Theorem ovnf Dummy variables 𝑖 𝑗 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0e0iccpnf 13261	. . . . 5 ⊢ 0 ∈ (0[,]+∞)
2	1	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → 0 ∈ (0[,]+∞))
3		0xr 11092	. . . . . 6 ⊢ 0 ∈ ℝ^*
4	3	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → 0 ∈ ℝ^*)
5		pnfxr 11099	. . . . . 6 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → +∞ ∈ ℝ^*)
7		ovnf.1	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Fin)
8	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → 𝑋 ∈ Fin)
9		elpwi 4550	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) → 𝑦 ⊆ (ℝ ↑_m 𝑋))
10	9	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → 𝑦 ⊆ (ℝ ↑_m 𝑋))
11		eqid 2737	. . . . . 6 ⊢ {𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}
12	8, 10, 11	ovnsupge0 44340	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → {𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆ (0[,]+∞))
13	8, 10, 11	ovnpnfelsup 44342	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → +∞ ∈ {𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))})
14	13	ne0d 4279	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → {𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ≠ ∅)
15	4, 6, 12, 14	inficc 43316	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → inf({𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < ) ∈ (0[,]+∞))
16	2, 15	ifcld 4515	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋)) → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < )) ∈ (0[,]+∞))
17		eqid 2737	. . 3 ⊢ (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^, < ))) = (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^ ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < )))
18	16, 17	fmptd 7025	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < ))):𝒫 (ℝ ↑_m 𝑋)⟶(0[,]+∞))
19	7	ovnval 44324	. . 3 ⊢ (𝜑 → (voln‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^ ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < ))))
20	19	feq1d 6620	. 2 ⊢ (𝜑 → ((voln‘𝑋):𝒫 (ℝ ↑_m 𝑋)⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 (ℝ ↑_m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ^ ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑_m 𝑋) ↑_m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ^*, < ))):𝒫 (ℝ ↑_m 𝑋)⟶(0[,]+∞)))
21	18, 20	mpbird 256	1 ⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑_m 𝑋)⟶(0[,]+∞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ∃wrex 3071 {crab 3404 ⊆ wss 3896 ∅c0 4266 ifcif 4469 𝒫 cpw 4543 ∪ ciun 4935 ↦ cmpt 5168 × cxp 5603 ∘ ccom 5609 ⟶wf 6459 ‘cfv 6463 (class class class)co 7313 ↑_m cmap 8661 Xcixp 8731 Fincfn 8779 infcinf 9268 ℝcr 10940 0cc0 10941 +∞cpnf 11076 ℝ^*cxr 11078 < clt 11079 ℕcn 12043 [,)cico 13151 [,]cicc 13152 ∏cprod 15684 volcvol 24698 Σ^{^}csumge0 44145 voln*covoln 44319

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 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-inf2 9467 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 ax-pre-sup 11019

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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 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 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4849 df-int 4891 df-iun 4937 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-se 5561 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-isom 6472 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-of 7571 df-om 7756 df-1st 7874 df-2nd 7875 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-2o 8343 df-er 8544 df-map 8663 df-pm 8664 df-ixp 8732 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-fi 9238 df-sup 9269 df-inf 9270 df-oi 9337 df-dju 9727 df-card 9765 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-div 11703 df-nn 12044 df-2 12106 df-3 12107 df-n0 12304 df-z 12390 df-uz 12653 df-q 12759 df-rp 12801 df-xneg 12918 df-xadd 12919 df-xmul 12920 df-ioo 13153 df-ico 13155 df-icc 13156 df-fz 13310 df-fzo 13453 df-fl 13582 df-seq 13792 df-exp 13853 df-hash 14115 df-cj 14879 df-re 14880 df-im 14881 df-sqrt 15015 df-abs 15016 df-clim 15266 df-rlim 15267 df-sum 15467 df-prod 15685 df-rest 17200 df-topgen 17221 df-psmet 20660 df-xmet 20661 df-met 20662 df-bl 20663 df-mopn 20664 df-top 22114 df-topon 22131 df-bases 22167 df-cmp 22609 df-ovol 24699 df-vol 24700 df-sumge0 44146 df-ovoln 44320

This theorem is referenced by: ovn0 44349 ovncl 44350 ovn02 44351 ovnome 44356 dmovn 44387 hspmbl 44412

W3C validator