mbfdm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfdm		Structured version Visualization version GIF version

Theorem mbfdm 23565

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)

**Assertion**
Ref	Expression
mbfdm	⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)

Proof of Theorem mbfdm Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ref 14022	. . . 4 ⊢ ℜ:ℂ⟶ℝ
2		mbff 23564	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
3		fco 6207	. . . 4 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
4	1, 2, 3	sylancr 698	. . 3 ⊢ (𝐹 ∈ MblFn → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
5		fimacnv 6498	. . 3 ⊢ ((ℜ ∘ 𝐹):dom 𝐹⟶ℝ → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
6	4, 5	syl 17	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
7		ioomax 12412	. . . 4 ⊢ (-∞(,)+∞) = ℝ
8		ioof 12435	. . . . . 6 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
9		ffn 6194	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
10	8, 9	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
11		mnfxr 10259	. . . . 5 ⊢ -∞ ∈ ℝ^*
12		pnfxr 10255	. . . . 5 ⊢ +∞ ∈ ℝ^*
13		fnovrn 6962	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ -∞ ∈ ℝ^ ∧ +∞ ∈ ℝ^*) → (-∞(,)+∞) ∈ ran (,))
14	10, 11, 12, 13	mp3an 1561	. . . 4 ⊢ (-∞(,)+∞) ∈ ran (,)
15	7, 14	eqeltrri 2824	. . 3 ⊢ ℝ ∈ ran (,)
16		ismbf1 23563	. . . . 5 ⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑_pm ℝ) ∧ ∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
17	16	simprbi 483	. . . 4 ⊢ (𝐹 ∈ MblFn → ∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))
18		simpl 474	. . . . 5 ⊢ (((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) → (^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
19	18	ralimi 3078	. . . 4 ⊢ (∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
20	17, 19	syl 17	. . 3 ⊢ (𝐹 ∈ MblFn → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
21		imaeq2 5608	. . . . 5 ⊢ (𝑥 = ℝ → (^◡(ℜ ∘ 𝐹) “ 𝑥) = (^◡(ℜ ∘ 𝐹) “ ℝ))
22	21	eleq1d 2812	. . . 4 ⊢ (𝑥 = ℝ → ((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
23	22	rspcv 3433	. . 3 ⊢ (ℝ ∈ ran (,) → (∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
24	15, 20, 23	mpsyl 68	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol)
25	6, 24	eqeltrrd 2828	1 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1620 ∈ wcel 2127 ∀wral 3038 𝒫 cpw 4290 × cxp 5252 ^◡ccnv 5253 dom cdm 5254 ran crn 5255 “ cima 5257 ∘ ccom 5258 Fn wfn 6032 ⟶wf 6033 (class class class)co 6801 ↑_pm cpm 8012 ℂcc 10097 ℝcr 10098 +∞cpnf 10234 -∞cmnf 10235 ℝ^*cxr 10236 (,)cioo 12339 ℜcre 14007 ℑcim 14008 volcvol 23403 MblFncmbf 23553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-id 5162 df-po 5175 df-so 5176 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-1st 7321 df-2nd 7322 df-er 7899 df-pm 8014 df-en 8110 df-dom 8111 df-sdom 8112 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-div 10848 df-2 11242 df-ioo 12343 df-cj 14009 df-re 14010 df-mbf 23558

This theorem is referenced by: ismbf 23567 ismbfcn 23568 mbfimaicc 23570 mbfdm2 23575 mbfres 23581 mbfmulc2lem 23584 mbfimaopn2 23594 cncombf 23595 mbfaddlem 23597 mbfadd 23598 mbfsub 23599 mbfmullem2 23661 mbfmul 23663 bddmulibl 23775 bddibl 23776 itgulm 24332 bddiblnc 33762 ftc1anclem1 33767 ftc1anclem5 33771 ftc1anclem8 33774 smfmbfcex 41443

W3C validator