ismbf3d

Description: Simplified form of ismbfd . (Contributed by Mario Carneiro, 18-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ismbf3d.1	$⊢ φ \to F : A ⟶ ℝ$
2		ismbf3d.2	$⊢ (φ \land x \in ℝ) \to F^{-1} [(x, +∞)] \in dom vol$
3		fimacnv	$⊢ F : A ⟶ ℝ \to F^{-1} [ℝ] = A$
4	1 3	syl	$⊢ φ \to F^{-1} [ℝ] = A$
5		imaiun	$⊢ F^{-1} [⋃_{y \in ℕ} (- y, +∞)] = ⋃_{y \in ℕ} F^{-1} [(- y, +∞)]$
6		ioossre	$⊢ (- y, +∞) \subseteq ℝ$
7	6	rgenw	$⊢ \forall y \in ℕ (- y, +∞) \subseteq ℝ$
8		iunss	$⊢ ⋃_{y \in ℕ} (- y, +∞) \subseteq ℝ \leftrightarrow \forall y \in ℕ (- y, +∞) \subseteq ℝ$
9	7 8	mpbir	$⊢ ⋃_{y \in ℕ} (- y, +∞) \subseteq ℝ$
10		renegcl	$⊢ z \in ℝ \to - z \in ℝ$
11		arch	$⊢ - z \in ℝ \to \exists y \in ℕ - z < y$
12	10 11	syl	$⊢ z \in ℝ \to \exists y \in ℕ - z < y$
13		simpl	$⊢ (z \in ℝ \land y \in ℕ) \to z \in ℝ$
14	13	biantrurd	$⊢ (z \in ℝ \land y \in ℕ) \to (- y < z \leftrightarrow (z \in ℝ \land - y < z))$
15		nnre	$⊢ y \in ℕ \to y \in ℝ$
16		ltnegcon1	$⊢ (z \in ℝ \land y \in ℝ) \to (- z < y \leftrightarrow - y < z)$
17	15 16	sylan2	$⊢ (z \in ℝ \land y \in ℕ) \to (- z < y \leftrightarrow - y < z)$
18	15	adantl	$⊢ (z \in ℝ \land y \in ℕ) \to y \in ℝ$
19	18	renegcld	$⊢ (z \in ℝ \land y \in ℕ) \to - y \in ℝ$
20	19	rexrd	$⊢ (z \in ℝ \land y \in ℕ) \to - y \in ℝ^{*}$
21		elioopnf	$⊢ - y \in ℝ^{*} \to (z \in (- y, +∞) \leftrightarrow (z \in ℝ \land - y < z))$
22	20 21	syl	$⊢ (z \in ℝ \land y \in ℕ) \to (z \in (- y, +∞) \leftrightarrow (z \in ℝ \land - y < z))$
23	14 17 22	3bitr4d	$⊢ (z \in ℝ \land y \in ℕ) \to (- z < y \leftrightarrow z \in (- y, +∞))$
24	23	rexbidva	$⊢ z \in ℝ \to (\exists y \in ℕ - z < y \leftrightarrow \exists y \in ℕ z \in (- y, +∞))$
25	12 24	mpbid	$⊢ z \in ℝ \to \exists y \in ℕ z \in (- y, +∞)$
26		eliun	$⊢ z \in ⋃_{y \in ℕ} (- y, +∞) \leftrightarrow \exists y \in ℕ z \in (- y, +∞)$
27	25 26	sylibr	$⊢ z \in ℝ \to z \in ⋃_{y \in ℕ} (- y, +∞)$
28	27	ssriv	$⊢ ℝ \subseteq ⋃_{y \in ℕ} (- y, +∞)$
29	9 28	eqssi	$⊢ ⋃_{y \in ℕ} (- y, +∞) = ℝ$
30	29	imaeq2i	$⊢ F^{-1} [⋃_{y \in ℕ} (- y, +∞)] = F^{-1} [ℝ]$
31	5 30	eqtr3i	$⊢ ⋃_{y \in ℕ} F^{-1} [(- y, +∞)] = F^{-1} [ℝ]$
32	2	ralrimiva	$⊢ φ \to \forall x \in ℝ F^{-1} [(x, +∞)] \in dom vol$
33	15	renegcld	$⊢ y \in ℕ \to - y \in ℝ$
34		oveq1	$⊢ x = - y \to (x, +∞) = (- y, +∞)$
35	34	imaeq2d	$⊢ x = - y \to F^{-1} [(x, +∞)] = F^{-1} [(- y, +∞)]$
36	35	eleq1d	$⊢ x = - y \to (F^{-1} [(x, +∞)] \in dom vol \leftrightarrow F^{-1} [(- y, +∞)] \in dom vol)$
37	36	rspccva	$⊢ (\forall x \in ℝ F^{-1} [(x, +∞)] \in dom vol \land - y \in ℝ) \to F^{-1} [(- y, +∞)] \in dom vol$
38	32 33 37	syl2an	$⊢ (φ \land y \in ℕ) \to F^{-1} [(- y, +∞)] \in dom vol$
39	38	ralrimiva	$⊢ φ \to \forall y \in ℕ F^{-1} [(- y, +∞)] \in dom vol$
40		iunmbl	$⊢ \forall y \in ℕ F^{-1} [(- y, +∞)] \in dom vol \to ⋃_{y \in ℕ} F^{-1} [(- y, +∞)] \in dom vol$
41	39 40	syl	$⊢ φ \to ⋃_{y \in ℕ} F^{-1} [(- y, +∞)] \in dom vol$
42	31 41	eqeltrrid	$⊢ φ \to F^{-1} [ℝ] \in dom vol$
43	4 42	eqeltrrd	$⊢ φ \to A \in dom vol$
44		imaiun	$⊢ F^{-1} [⋃_{y \in ℕ} (−∞, z - (\frac{1}{y})]] = ⋃_{y \in ℕ} F^{-1} [(−∞, z - (\frac{1}{y})]]$
45		eliun	$⊢ x \in ⋃_{y \in ℕ} (−∞, z - (\frac{1}{y})] \leftrightarrow \exists y \in ℕ x \in (−∞, z - (\frac{1}{y})]$
46		3simpb	$⊢ (x \in ℝ \land −∞ < x \land x \leq z - (\frac{1}{y})) \to (x \in ℝ \land x \leq z - (\frac{1}{y}))$
47		simplr	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to z \in ℝ$
48		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
49	48	ad2antrl	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to y \in ℝ^{+}$
50	49	rpreccld	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to \frac{1}{y} \in ℝ^{+}$
51	47 50	ltsubrpd	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to z - (\frac{1}{y}) < z$
52		simprr	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to x \in ℝ$
53		simpr	$⊢ (φ \land z \in ℝ) \to z \in ℝ$
54		nnrecre	$⊢ y \in ℕ \to \frac{1}{y} \in ℝ$
55		resubcl	$⊢ (z \in ℝ \land \frac{1}{y} \in ℝ) \to z - (\frac{1}{y}) \in ℝ$
56	53 54 55	syl2an	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to z - (\frac{1}{y}) \in ℝ$
57	56	adantrr	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to z - (\frac{1}{y}) \in ℝ$
58		lelttr	$⊢ (x \in ℝ \land z - (\frac{1}{y}) \in ℝ \land z \in ℝ) \to ((x \leq z - (\frac{1}{y}) \land z - (\frac{1}{y}) < z) \to x < z)$
59	52 57 47 58	syl3anc	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to ((x \leq z - (\frac{1}{y}) \land z - (\frac{1}{y}) < z) \to x < z)$
60	51 59	mpan2d	$⊢ ((φ \land z \in ℝ) \land (y \in ℕ \land x \in ℝ)) \to (x \leq z - (\frac{1}{y}) \to x < z)$
61	60	anassrs	$⊢ (((φ \land z \in ℝ) \land y \in ℕ) \land x \in ℝ) \to (x \leq z - (\frac{1}{y}) \to x < z)$
62	61	imdistanda	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to ((x \in ℝ \land x \leq z - (\frac{1}{y})) \to (x \in ℝ \land x < z))$
63	46 62	syl5	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to ((x \in ℝ \land −∞ < x \land x \leq z - (\frac{1}{y})) \to (x \in ℝ \land x < z))$
64		mnfxr	$⊢ −∞ \in ℝ^{*}$
65		elioc2	$⊢ (−∞ \in ℝ^{*} \land z - (\frac{1}{y}) \in ℝ) \to (x \in (−∞, z - (\frac{1}{y})] \leftrightarrow (x \in ℝ \land −∞ < x \land x \leq z - (\frac{1}{y})))$
66	64 56 65	sylancr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (x \in (−∞, z - (\frac{1}{y})] \leftrightarrow (x \in ℝ \land −∞ < x \land x \leq z - (\frac{1}{y})))$
67		rexr	$⊢ z \in ℝ \to z \in ℝ^{*}$
68	67	adantl	$⊢ (φ \land z \in ℝ) \to z \in ℝ^{*}$
69		elioomnf	$⊢ z \in ℝ^{*} \to (x \in (−∞, z) \leftrightarrow (x \in ℝ \land x < z))$
70	68 69	syl	$⊢ (φ \land z \in ℝ) \to (x \in (−∞, z) \leftrightarrow (x \in ℝ \land x < z))$
71	70	adantr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (x \in (−∞, z) \leftrightarrow (x \in ℝ \land x < z))$
72	63 66 71	3imtr4d	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (x \in (−∞, z - (\frac{1}{y})] \to x \in (−∞, z))$
73	72	rexlimdva	$⊢ (φ \land z \in ℝ) \to (\exists y \in ℕ x \in (−∞, z - (\frac{1}{y})] \to x \in (−∞, z))$
74	73 70	sylibd	$⊢ (φ \land z \in ℝ) \to (\exists y \in ℕ x \in (−∞, z - (\frac{1}{y})] \to (x \in ℝ \land x < z))$
75		simprl	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to x \in ℝ$
76	75	adantr	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to x \in ℝ$
77	76	mnfltd	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to −∞ < x$
78	56	ad2ant2r	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to z - (\frac{1}{y}) \in ℝ$
79	54	ad2antrl	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to \frac{1}{y} \in ℝ$
80		simplr	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to z \in ℝ$
81	80	adantr	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to z \in ℝ$
82		simprr	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to \frac{1}{y} < z - x$
83	79 81 76 82	ltsub13d	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to x < z - (\frac{1}{y})$
84	76 78 83	ltled	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to x \leq z - (\frac{1}{y})$
85	66	ad2ant2r	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to (x \in (−∞, z - (\frac{1}{y})] \leftrightarrow (x \in ℝ \land −∞ < x \land x \leq z - (\frac{1}{y})))$
86	76 77 84 85	mpbir3and	$⊢ (((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \land (y \in ℕ \land \frac{1}{y} < z - x)) \to x \in (−∞, z - (\frac{1}{y})]$
87	80 75	resubcld	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to z - x \in ℝ$
88		simprr	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to x < z$
89	75 80	posdifd	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to (x < z \leftrightarrow 0 < z - x)$
90	88 89	mpbid	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to 0 < z - x$
91		nnrecl	$⊢ (z - x \in ℝ \land 0 < z - x) \to \exists y \in ℕ \frac{1}{y} < z - x$
92	87 90 91	syl2anc	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to \exists y \in ℕ \frac{1}{y} < z - x$
93	86 92	reximddv	$⊢ ((φ \land z \in ℝ) \land (x \in ℝ \land x < z)) \to \exists y \in ℕ x \in (−∞, z - (\frac{1}{y})]$
94	93	ex	$⊢ (φ \land z \in ℝ) \to ((x \in ℝ \land x < z) \to \exists y \in ℕ x \in (−∞, z - (\frac{1}{y})])$
95	74 94	impbid	$⊢ (φ \land z \in ℝ) \to (\exists y \in ℕ x \in (−∞, z - (\frac{1}{y})] \leftrightarrow (x \in ℝ \land x < z))$
96	95 70	bitr4d	$⊢ (φ \land z \in ℝ) \to (\exists y \in ℕ x \in (−∞, z - (\frac{1}{y})] \leftrightarrow x \in (−∞, z))$
97	45 96	syl5bb	$⊢ (φ \land z \in ℝ) \to (x \in ⋃_{y \in ℕ} (−∞, z - (\frac{1}{y})] \leftrightarrow x \in (−∞, z))$
98	97	eqrdv	$⊢ (φ \land z \in ℝ) \to ⋃_{y \in ℕ} (−∞, z - (\frac{1}{y})] = (−∞, z)$
99	98	imaeq2d	$⊢ (φ \land z \in ℝ) \to F^{-1} [⋃_{y \in ℕ} (−∞, z - (\frac{1}{y})]] = F^{-1} [(−∞, z)]$
100	44 99	syl5eqr	$⊢ (φ \land z \in ℝ) \to ⋃_{y \in ℕ} F^{-1} [(−∞, z - (\frac{1}{y})]] = F^{-1} [(−∞, z)]$
101	1	ad2antrr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F : A ⟶ ℝ$
102		ffun	$⊢ F : A ⟶ ℝ \to Fun F$
103		funcnvcnv	$⊢ Fun F \to Fun {F^{-1}}^{-1}$
104		imadif	$⊢ Fun {F^{-1}}^{-1} \to F^{-1} [ℝ ∖ (z - (\frac{1}{y}), +∞)] = F^{-1} [ℝ] ∖ F^{-1} [(z - (\frac{1}{y}), +∞)]$
105	101 102 103 104	4syl	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [ℝ ∖ (z - (\frac{1}{y}), +∞)] = F^{-1} [ℝ] ∖ F^{-1} [(z - (\frac{1}{y}), +∞)]$
106	64	a1i	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to −∞ \in ℝ^{*}$
107	56	rexrd	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to z - (\frac{1}{y}) \in ℝ^{*}$
108		pnfxr	$⊢ +∞ \in ℝ^{*}$
109	108	a1i	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to +∞ \in ℝ^{*}$
110	56	mnfltd	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to −∞ < z - (\frac{1}{y})$
111	56	ltpnfd	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to z - (\frac{1}{y}) < +∞$
112		df-ioc	$⊢ (.] = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u < w \land w \leq v)\})$
113		df-ioo	$⊢ (.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u < w \land w < v)\})$
114		xrltnle	$⊢ (z - (\frac{1}{y}) \in ℝ^{} \land x \in ℝ^{}) \to (z - (\frac{1}{y}) < x \leftrightarrow \neg x \leq z - (\frac{1}{y}))$
115		xrlelttr	$⊢ (x \in ℝ^{} \land z - (\frac{1}{y}) \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((x \leq z - (\frac{1}{y}) \land z - (\frac{1}{y}) < +∞) \to x < +∞)$
116		xrlttr	$⊢ (−∞ \in ℝ^{} \land z - (\frac{1}{y}) \in ℝ^{} \land x \in ℝ^{*}) \to ((−∞ < z - (\frac{1}{y}) \land z - (\frac{1}{y}) < x) \to −∞ < x)$
117	112 113 114 113 115 116	ixxun	$⊢ ((−∞ \in ℝ^{} \land z - (\frac{1}{y}) \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ < z - (\frac{1}{y}) \land z - (\frac{1}{y}) < +∞)) \to (−∞, z - (\frac{1}{y})] \cup (z - (\frac{1}{y}), +∞) = (−∞, +∞)$
118	106 107 109 110 111 117	syl32anc	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (−∞, z - (\frac{1}{y})] \cup (z - (\frac{1}{y}), +∞) = (−∞, +∞)$
119		uncom	$⊢ (−∞, z - (\frac{1}{y})] \cup (z - (\frac{1}{y}), +∞) = (z - (\frac{1}{y}), +∞) \cup (−∞, z - (\frac{1}{y})]$
120		ioomax	$⊢ (−∞, +∞) = ℝ$
121	118 119 120	3eqtr3g	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (z - (\frac{1}{y}), +∞) \cup (−∞, z - (\frac{1}{y})] = ℝ$
122		ioossre	$⊢ (z - (\frac{1}{y}), +∞) \subseteq ℝ$
123		incom	$⊢ (z - (\frac{1}{y}), +∞) \cap (−∞, z - (\frac{1}{y})] = (−∞, z - (\frac{1}{y})] \cap (z - (\frac{1}{y}), +∞)$
124	112 113 114	ixxdisj	$⊢ (−∞ \in ℝ^{} \land z - (\frac{1}{y}) \in ℝ^{} \land +∞ \in ℝ^{*}) \to (−∞, z - (\frac{1}{y})] \cap (z - (\frac{1}{y}), +∞) = \emptyset$
125	64 108 124	mp3an13	$⊢ z - (\frac{1}{y}) \in ℝ^{*} \to (−∞, z - (\frac{1}{y})] \cap (z - (\frac{1}{y}), +∞) = \emptyset$
126	107 125	syl	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (−∞, z - (\frac{1}{y})] \cap (z - (\frac{1}{y}), +∞) = \emptyset$
127	123 126	syl5eq	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to (z - (\frac{1}{y}), +∞) \cap (−∞, z - (\frac{1}{y})] = \emptyset$
128		uneqdifeq	$⊢ ((z - (\frac{1}{y}), +∞) \subseteq ℝ \land (z - (\frac{1}{y}), +∞) \cap (−∞, z - (\frac{1}{y})] = \emptyset) \to ((z - (\frac{1}{y}), +∞) \cup (−∞, z - (\frac{1}{y})] = ℝ \leftrightarrow ℝ ∖ (z - (\frac{1}{y}), +∞) = (−∞, z - (\frac{1}{y})])$
129	122 127 128	sylancr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to ((z - (\frac{1}{y}), +∞) \cup (−∞, z - (\frac{1}{y})] = ℝ \leftrightarrow ℝ ∖ (z - (\frac{1}{y}), +∞) = (−∞, z - (\frac{1}{y})])$
130	121 129	mpbid	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to ℝ ∖ (z - (\frac{1}{y}), +∞) = (−∞, z - (\frac{1}{y})]$
131	130	imaeq2d	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [ℝ ∖ (z - (\frac{1}{y}), +∞)] = F^{-1} [(−∞, z - (\frac{1}{y})]]$
132	105 131	eqtr3d	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [ℝ] ∖ F^{-1} [(z - (\frac{1}{y}), +∞)] = F^{-1} [(−∞, z - (\frac{1}{y})]]$
133	42	ad2antrr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [ℝ] \in dom vol$
134		oveq1	$⊢ x = z - (\frac{1}{y}) \to (x, +∞) = (z - (\frac{1}{y}), +∞)$
135	134	imaeq2d	$⊢ x = z - (\frac{1}{y}) \to F^{-1} [(x, +∞)] = F^{-1} [(z - (\frac{1}{y}), +∞)]$
136	135	eleq1d	$⊢ x = z - (\frac{1}{y}) \to (F^{-1} [(x, +∞)] \in dom vol \leftrightarrow F^{-1} [(z - (\frac{1}{y}), +∞)] \in dom vol)$
137	32	ad2antrr	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to \forall x \in ℝ F^{-1} [(x, +∞)] \in dom vol$
138	136 137 56	rspcdva	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [(z - (\frac{1}{y}), +∞)] \in dom vol$
139		difmbl	$⊢ (F^{-1} [ℝ] \in dom vol \land F^{-1} [(z - (\frac{1}{y}), +∞)] \in dom vol) \to F^{-1} [ℝ] ∖ F^{-1} [(z - (\frac{1}{y}), +∞)] \in dom vol$
140	133 138 139	syl2anc	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [ℝ] ∖ F^{-1} [(z - (\frac{1}{y}), +∞)] \in dom vol$
141	132 140	eqeltrrd	$⊢ ((φ \land z \in ℝ) \land y \in ℕ) \to F^{-1} [(−∞, z - (\frac{1}{y})]] \in dom vol$
142	141	ralrimiva	$⊢ (φ \land z \in ℝ) \to \forall y \in ℕ F^{-1} [(−∞, z - (\frac{1}{y})]] \in dom vol$
143		iunmbl	$⊢ \forall y \in ℕ F^{-1} [(−∞, z - (\frac{1}{y})]] \in dom vol \to ⋃_{y \in ℕ} F^{-1} [(−∞, z - (\frac{1}{y})]] \in dom vol$
144	142 143	syl	$⊢ (φ \land z \in ℝ) \to ⋃_{y \in ℕ} F^{-1} [(−∞, z - (\frac{1}{y})]] \in dom vol$
145	100 144	eqeltrrd	$⊢ (φ \land z \in ℝ) \to F^{-1} [(−∞, z)] \in dom vol$
146	145	ralrimiva	$⊢ φ \to \forall z \in ℝ F^{-1} [(−∞, z)] \in dom vol$
147		oveq2	$⊢ z = x \to (−∞, z) = (−∞, x)$
148	147	imaeq2d	$⊢ z = x \to F^{-1} [(−∞, z)] = F^{-1} [(−∞, x)]$
149	148	eleq1d	$⊢ z = x \to (F^{-1} [(−∞, z)] \in dom vol \leftrightarrow F^{-1} [(−∞, x)] \in dom vol)$
150	149	cbvralvw	$⊢ \forall z \in ℝ F^{-1} [(−∞, z)] \in dom vol \leftrightarrow \forall x \in ℝ F^{-1} [(−∞, x)] \in dom vol$
151	146 150	sylib	$⊢ φ \to \forall x \in ℝ F^{-1} [(−∞, x)] \in dom vol$
152	151	r19.21bi	$⊢ (φ \land x \in ℝ) \to F^{-1} [(−∞, x)] \in dom vol$
153	1 43 2 152	ismbf2d	$⊢ φ \to F \in MblFn$

Metamath Proof Explorer

Theorem ismbf3d

Proof