ismbfd

Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	ismbfd.1	$⊢ φ \to F : A ⟶ ℝ$
	ismbfd.2	$⊢ (φ \land x \in ℝ^{*}) \to F^{-1} [(x, +∞)] \in dom vol$
	ismbfd.3	$⊢ (φ \land x \in ℝ^{*}) \to F^{-1} [(−∞, x)] \in dom vol$
Assertion	ismbfd	$⊢ φ \to F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		ismbfd.1	$⊢ φ \to F : A ⟶ ℝ$
2		ismbfd.2	$⊢ (φ \land x \in ℝ^{*}) \to F^{-1} [(x, +∞)] \in dom vol$
3		ismbfd.3	$⊢ (φ \land x \in ℝ^{*}) \to F^{-1} [(−∞, x)] \in dom vol$
4		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
5		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
6		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (z \in ran (.) \leftrightarrow \exists x \in ℝ^{} \exists y \in ℝ^{} z = (x, y))$
7	4 5 6	mp2b	$⊢ z \in ran (.) \leftrightarrow \exists x \in ℝ^{} \exists y \in ℝ^{} z = (x, y)$
8		simprl	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to x \in ℝ^{*}$
9		pnfxr	$⊢ +∞ \in ℝ^{*}$
10	9	a1i	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to +∞ \in ℝ^{*}$
11		mnfxr	$⊢ −∞ \in ℝ^{*}$
12	11	a1i	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to −∞ \in ℝ^{*}$
13		simprr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to y \in ℝ^{*}$
14		iooin	$⊢ ((x \in ℝ^{} \land +∞ \in ℝ^{}) \land (−∞ \in ℝ^{} \land y \in ℝ^{})) \to (x, +∞) \cap (−∞, y) = (if (x \leq −∞, −∞, x), if (+∞ \leq y, +∞, y))$
15	8 10 12 13 14	syl22anc	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to (x, +∞) \cap (−∞, y) = (if (x \leq −∞, −∞, x), if (+∞ \leq y, +∞, y))$
16		ifcl	$⊢ (−∞ \in ℝ^{} \land x \in ℝ^{}) \to if (x \leq −∞, −∞, x) \in ℝ^{*}$
17	11 8 16	sylancr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (x \leq −∞, −∞, x) \in ℝ^{*}$
18		mnfle	$⊢ x \in ℝ^{*} \to −∞ \leq x$
19		xrleid	$⊢ x \in ℝ^{*} \to x \leq x$
20		breq1	$⊢ −∞ = if (x \leq −∞, −∞, x) \to (−∞ \leq x \leftrightarrow if (x \leq −∞, −∞, x) \leq x)$
21		breq1	$⊢ x = if (x \leq −∞, −∞, x) \to (x \leq x \leftrightarrow if (x \leq −∞, −∞, x) \leq x)$
22	20 21	ifboth	$⊢ (−∞ \leq x \land x \leq x) \to if (x \leq −∞, −∞, x) \leq x$
23	18 19 22	syl2anc	$⊢ x \in ℝ^{*} \to if (x \leq −∞, −∞, x) \leq x$
24	23	ad2antrl	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (x \leq −∞, −∞, x) \leq x$
25		xrmax1	$⊢ (x \in ℝ^{} \land −∞ \in ℝ^{}) \to x \leq if (x \leq −∞, −∞, x)$
26	8 11 25	sylancl	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to x \leq if (x \leq −∞, −∞, x)$
27	17 8 24 26	xrletrid	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (x \leq −∞, −∞, x) = x$
28		ifcl	$⊢ (+∞ \in ℝ^{} \land y \in ℝ^{}) \to if (+∞ \leq y, +∞, y) \in ℝ^{*}$
29	9 13 28	sylancr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (+∞ \leq y, +∞, y) \in ℝ^{*}$
30		xrmin2	$⊢ (+∞ \in ℝ^{} \land y \in ℝ^{}) \to if (+∞ \leq y, +∞, y) \leq y$
31	9 13 30	sylancr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (+∞ \leq y, +∞, y) \leq y$
32		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
33		xrleid	$⊢ y \in ℝ^{*} \to y \leq y$
34		breq2	$⊢ +∞ = if (+∞ \leq y, +∞, y) \to (y \leq +∞ \leftrightarrow y \leq if (+∞ \leq y, +∞, y))$
35		breq2	$⊢ y = if (+∞ \leq y, +∞, y) \to (y \leq y \leftrightarrow y \leq if (+∞ \leq y, +∞, y))$
36	34 35	ifboth	$⊢ (y \leq +∞ \land y \leq y) \to y \leq if (+∞ \leq y, +∞, y)$
37	32 33 36	syl2anc	$⊢ y \in ℝ^{*} \to y \leq if (+∞ \leq y, +∞, y)$
38	37	ad2antll	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to y \leq if (+∞ \leq y, +∞, y)$
39	29 13 31 38	xrletrid	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to if (+∞ \leq y, +∞, y) = y$
40	27 39	oveq12d	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to (if (x \leq −∞, −∞, x), if (+∞ \leq y, +∞, y)) = (x, y)$
41	15 40	eqtrd	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to (x, +∞) \cap (−∞, y) = (x, y)$
42	41	imaeq2d	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, +∞) \cap (−∞, y)] = F^{-1} [(x, y)]$
43	1	adantr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F : A ⟶ ℝ$
44	43	ffund	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to Fun F$
45		inpreima	$⊢ Fun F \to F^{-1} [(x, +∞) \cap (−∞, y)] = F^{-1} [(x, +∞)] \cap F^{-1} [(−∞, y)]$
46	44 45	syl	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, +∞) \cap (−∞, y)] = F^{-1} [(x, +∞)] \cap F^{-1} [(−∞, y)]$
47	42 46	eqtr3d	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, y)] = F^{-1} [(x, +∞)] \cap F^{-1} [(−∞, y)]$
48	2	adantrr	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, +∞)] \in dom vol$
49	3	ralrimiva	$⊢ φ \to \forall x \in ℝ^{*} F^{-1} [(−∞, x)] \in dom vol$
50		oveq2	$⊢ x = y \to (−∞, x) = (−∞, y)$
51	50	imaeq2d	$⊢ x = y \to F^{-1} [(−∞, x)] = F^{-1} [(−∞, y)]$
52	51	eleq1d	$⊢ x = y \to (F^{-1} [(−∞, x)] \in dom vol \leftrightarrow F^{-1} [(−∞, y)] \in dom vol)$
53	52	rspccva	$⊢ (\forall x \in ℝ^{} F^{-1} [(−∞, x)] \in dom vol \land y \in ℝ^{}) \to F^{-1} [(−∞, y)] \in dom vol$
54	49 53	sylan	$⊢ (φ \land y \in ℝ^{*}) \to F^{-1} [(−∞, y)] \in dom vol$
55	54	adantrl	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(−∞, y)] \in dom vol$
56		inmbl	$⊢ (F^{-1} [(x, +∞)] \in dom vol \land F^{-1} [(−∞, y)] \in dom vol) \to F^{-1} [(x, +∞)] \cap F^{-1} [(−∞, y)] \in dom vol$
57	48 55 56	syl2anc	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, +∞)] \cap F^{-1} [(−∞, y)] \in dom vol$
58	47 57	eqeltrd	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to F^{-1} [(x, y)] \in dom vol$
59		imaeq2	$⊢ z = (x, y) \to F^{-1} [z] = F^{-1} [(x, y)]$
60	59	eleq1d	$⊢ z = (x, y) \to (F^{-1} [z] \in dom vol \leftrightarrow F^{-1} [(x, y)] \in dom vol)$
61	58 60	syl5ibrcom	$⊢ (φ \land (x \in ℝ^{} \land y \in ℝ^{})) \to (z = (x, y) \to F^{-1} [z] \in dom vol)$
62	61	rexlimdvva	$⊢ φ \to (\exists x \in ℝ^{} \exists y \in ℝ^{} z = (x, y) \to F^{-1} [z] \in dom vol)$
63	7 62	syl5bi	$⊢ φ \to (z \in ran (.) \to F^{-1} [z] \in dom vol)$
64	63	ralrimiv	$⊢ φ \to \forall z \in ran (.) F^{-1} [z] \in dom vol$
65		ismbf	$⊢ F : A ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall z \in ran (.) F^{-1} [z] \in dom vol)$
66	1 65	syl	$⊢ φ \to (F \in MblFn \leftrightarrow \forall z \in ran (.) F^{-1} [z] \in dom vol)$
67	64 66	mpbird	$⊢ φ \to F \in MblFn$

Metamath Proof Explorer

Theorem ismbfd

Proof