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 23301

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 13786	. . . 4 ⊢ ℜ:ℂ⟶ℝ
2		mbff 23300	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
3		fco 6015	. . . 4 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
4	1, 2, 3	sylancr 694	. . 3 ⊢ (𝐹 ∈ MblFn → (ℜ ∘ 𝐹):dom 𝐹⟶ℝ)
5		fimacnv 6303	. . 3 ⊢ ((ℜ ∘ 𝐹):dom 𝐹⟶ℝ → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
6	4, 5	syl 17	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) = dom 𝐹)
7		ioomax 12190	. . . 4 ⊢ (-∞(,)+∞) = ℝ
8		ioof 12213	. . . . . 6 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
9		ffn 6002	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
10	8, 9	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
11		mnfxr 10040	. . . . 5 ⊢ -∞ ∈ ℝ^*
12		pnfxr 10036	. . . . 5 ⊢ +∞ ∈ ℝ^*
13		fnovrn 6762	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ -∞ ∈ ℝ^ ∧ +∞ ∈ ℝ^*) → (-∞(,)+∞) ∈ ran (,))
14	10, 11, 12, 13	mp3an 1421	. . . 4 ⊢ (-∞(,)+∞) ∈ ran (,)
15	7, 14	eqeltrri 2695	. . 3 ⊢ ℝ ∈ ran (,)
16		ismbf1 23299	. . . . 5 ⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑_pm ℝ) ∧ ∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
17	16	simprbi 480	. . . 4 ⊢ (𝐹 ∈ MblFn → ∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))
18		simpl 473	. . . . 5 ⊢ (((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) → (^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
19	18	ralimi 2947	. . . 4 ⊢ (∀𝑥 ∈ ran (,)((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (^◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
20	17, 19	syl 17	. . 3 ⊢ (𝐹 ∈ MblFn → ∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)
21		imaeq2 5421	. . . . 5 ⊢ (𝑥 = ℝ → (^◡(ℜ ∘ 𝐹) “ 𝑥) = (^◡(ℜ ∘ 𝐹) “ ℝ))
22	21	eleq1d 2683	. . . 4 ⊢ (𝑥 = ℝ → ((^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
23	22	rspcv 3291	. . 3 ⊢ (ℝ ∈ ran (,) → (∀𝑥 ∈ ran (,)(^◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol))
24	15, 20, 23	mpsyl 68	. 2 ⊢ (𝐹 ∈ MblFn → (^◡(ℜ ∘ 𝐹) “ ℝ) ∈ dom vol)
25	6, 24	eqeltrrd 2699	1 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ∀wral 2907 𝒫 cpw 4130 × cxp 5072 ^◡ccnv 5073 dom cdm 5074 ran crn 5075 “ cima 5077 ∘ ccom 5078 Fn wfn 5842 ⟶wf 5843 (class class class)co 6604 ↑_pm cpm 7803 ℂcc 9878 ℝcr 9879 +∞cpnf 10015 -∞cmnf 10016 ℝ^*cxr 10017 (,)cioo 12117 ℜcre 13771 ℑcim 13772 volcvol 23139 MblFncmbf 23289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-op 4155 df-uni 4403 df-iun 4487 df-br 4614 df-opab 4674 df-mpt 4675 df-id 4989 df-po 4995 df-so 4996 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-1st 7113 df-2nd 7114 df-er 7687 df-pm 7805 df-en 7900 df-dom 7901 df-sdom 7902 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-div 10629 df-2 11023 df-ioo 12121 df-cj 13773 df-re 13774 df-mbf 23294

This theorem is referenced by: ismbf 23303 ismbfcn 23304 mbfimaicc 23306 mbfdm2 23311 mbfres 23317 mbfmulc2lem 23320 mbfimaopn2 23330 cncombf 23331 mbfaddlem 23333 mbfadd 23334 mbfsub 23335 mbfmullem2 23397 mbfmul 23399 bddmulibl 23511 bddibl 23512 itgulm 24066 bddiblnc 33109 ftc1anclem1 33114 ftc1anclem5 33118 ftc1anclem8 33121 smfmbfcex 40272

W3C validator