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 23586

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 14043	. . . 4 ⊢ ℜ:ℂ⟶ℝ
2		mbff 23585	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
3		fco 6211	. . . 4 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
4	1, 2, 3	sylancr 698	. . 3 ⊢ (𝐹 ∈ MblFn → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
5		fimacnv 6502	. . 3 ⊢ ((ℜ ∘ 𝐹):dom 𝐹⟶ℝ → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
6	4, 5	syl 17	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
7		ioomax 12433	. . . 4 ⊢ (-∞(,)+∞) = ℝ
8		ioof 12456	. . . . . 6 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
9		ffn 6198	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
10	8, 9	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
11		mnfxr 10280	. . . . 5 ⊢ -∞ ∈ ℝ^*
12		pnfxr 10276	. . . . 5 ⊢ +∞ ∈ ℝ^*
13		fnovrn 6966	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ -∞ ∈ ℝ^ ∧ +∞ ∈ ℝ^*) → (-∞(,)+∞) ∈ ran (,))
14	10, 11, 12, 13	mp3an 1565	. . . 4 ⊢ (-∞(,)+∞) ∈ ran (,)
15	7, 14	eqeltrri 2828	. . 3 ⊢ ℝ ∈ ran (,)
16		ismbf1 23584	. . . . 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 3082	. . . 4 ⊢ (∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
20	17, 19	syl 17	. . 3 ⊢ (𝐹 ∈ MblFn → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
21		imaeq2 5612	. . . . 5 ⊢ (𝑥 = ℝ → (^◡(ℜ ∘ 𝐹) “ 𝑥) = (^◡(ℜ ∘ 𝐹) “ ℝ))
22	21	eleq1d 2816	. . . 4 ⊢ (𝑥 = ℝ → ((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
23	22	rspcv 3437	. . 3 ⊢ (ℝ ∈ ran (,) → (∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
24	15, 20, 23	mpsyl 68	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol)
25	6, 24	eqeltrrd 2832	1 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1624 ∈ wcel 2131 ∀wral 3042 𝒫 cpw 4294 × cxp 5256 ^◡ccnv 5257 dom cdm 5258 ran crn 5259 “ cima 5261 ∘ ccom 5262 Fn wfn 6036 ⟶wf 6037 (class class class)co 6805 ↑_pm cpm 8016 ℂcc 10118 ℝcr 10119 +∞cpnf 10255 -∞cmnf 10256 ℝ^*cxr 10257 (,)cioo 12360 ℜcre 14028 ℑcim 14029 volcvol 23424 MblFncmbf 23574

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-cnex 10176 ax-resscn 10177 ax-1cn 10178 ax-icn 10179 ax-addcl 10180 ax-addrcl 10181 ax-mulcl 10182 ax-mulrcl 10183 ax-mulcom 10184 ax-addass 10185 ax-mulass 10186 ax-distr 10187 ax-i2m1 10188 ax-1ne0 10189 ax-1rid 10190 ax-rnegex 10191 ax-rrecex 10192 ax-cnre 10193 ax-pre-lttri 10194 ax-pre-lttrn 10195 ax-pre-ltadd 10196 ax-pre-mulgt0 10197

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-nel 3028 df-ral 3047 df-rex 3048 df-reu 3049 df-rmo 3050 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-po 5179 df-so 5180 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-riota 6766 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-1st 7325 df-2nd 7326 df-er 7903 df-pm 8018 df-en 8114 df-dom 8115 df-sdom 8116 df-pnf 10260 df-mnf 10261 df-xr 10262 df-ltxr 10263 df-le 10264 df-sub 10452 df-neg 10453 df-div 10869 df-2 11263 df-ioo 12364 df-cj 14030 df-re 14031 df-mbf 23579

This theorem is referenced by: ismbf 23588 ismbfcn 23589 mbfimaicc 23591 mbfdm2 23596 mbfres 23602 mbfmulc2lem 23605 mbfimaopn2 23615 cncombf 23616 mbfaddlem 23618 mbfadd 23619 mbfsub 23620 mbfmullem2 23682 mbfmul 23684 bddmulibl 23796 bddibl 23797 itgulm 24353 bddiblnc 33785 ftc1anclem1 33790 ftc1anclem5 33794 ftc1anclem8 33797 smfmbfcex 41466

W3C validator