mbfmax

Description: The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	mbfmax.1	$⊢ φ \to F : A ⟶ ℝ$
	mbfmax.2	$⊢ φ \to F \in MblFn$
	mbfmax.3	$⊢ φ \to G : A ⟶ ℝ$
	mbfmax.4	$⊢ φ \to G \in MblFn$
	mbfmax.5	$⊢ H = (x \in A ⟼ if (F (x) \leq G (x), G (x), F (x)))$
Assertion	mbfmax	$⊢ φ \to H \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmax.1	$⊢ φ \to F : A ⟶ ℝ$
2		mbfmax.2	$⊢ φ \to F \in MblFn$
3		mbfmax.3	$⊢ φ \to G : A ⟶ ℝ$
4		mbfmax.4	$⊢ φ \to G \in MblFn$
5		mbfmax.5	$⊢ H = (x \in A ⟼ if (F (x) \leq G (x), G (x), F (x)))$
6	3	ffvelrnda	$⊢ (φ \land x \in A) \to G (x) \in ℝ$
7	1	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in ℝ$
8	6 7	ifcld	$⊢ (φ \land x \in A) \to if (F (x) \leq G (x), G (x), F (x)) \in ℝ$
9	8 5	fmptd	$⊢ φ \to H : A ⟶ ℝ$
10	1	adantr	$⊢ (φ \land y \in ℝ^{*}) \to F : A ⟶ ℝ$
11	10	ffvelrnda	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to F (z) \in ℝ$
12	11	rexrd	$⊢ ((φ \land y \in ℝ^{}) \land z \in A) \to F (z) \in ℝ^{}$
13	3	adantr	$⊢ (φ \land y \in ℝ^{*}) \to G : A ⟶ ℝ$
14	13	ffvelrnda	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to G (z) \in ℝ$
15	14	rexrd	$⊢ ((φ \land y \in ℝ^{}) \land z \in A) \to G (z) \in ℝ^{}$
16		simplr	$⊢ ((φ \land y \in ℝ^{}) \land z \in A) \to y \in ℝ^{}$
17		xrmaxle	$⊢ (F (z) \in ℝ^{} \land G (z) \in ℝ^{} \land y \in ℝ^{*}) \to (if (F (z) \leq G (z), G (z), F (z)) \leq y \leftrightarrow (F (z) \leq y \land G (z) \leq y))$
18	12 15 16 17	syl3anc	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \leq y \leftrightarrow (F (z) \leq y \land G (z) \leq y))$
19	18	notbid	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (\neg if (F (z) \leq G (z), G (z), F (z)) \leq y \leftrightarrow \neg (F (z) \leq y \land G (z) \leq y))$
20		ianor	$⊢ \neg (F (z) \leq y \land G (z) \leq y) \leftrightarrow (\neg F (z) \leq y \lor \neg G (z) \leq y)$
21	19 20	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (\neg if (F (z) \leq G (z), G (z), F (z)) \leq y \leftrightarrow (\neg F (z) \leq y \lor \neg G (z) \leq y))$
22		pnfxr	$⊢ +∞ \in ℝ^{*}$
23		elioo2	$⊢ (y \in ℝ^{} \land +∞ \in ℝ^{}) \to (if (F (z) \leq G (z), G (z), F (z)) \in (y, +∞) \leftrightarrow (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land y < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < +∞))$
24	16 22 23	sylancl	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in (y, +∞) \leftrightarrow (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land y < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < +∞))$
25		3anan12	$⊢ (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land y < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < +∞) \leftrightarrow (y < if (F (z) \leq G (z), G (z), F (z)) \land (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land if (F (z) \leq G (z), G (z), F (z)) < +∞))$
26	24 25	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in (y, +∞) \leftrightarrow (y < if (F (z) \leq G (z), G (z), F (z)) \land (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land if (F (z) \leq G (z), G (z), F (z)) < +∞)))$
27		fveq2	$⊢ x = z \to F (x) = F (z)$
28		fveq2	$⊢ x = z \to G (x) = G (z)$
29	27 28	breq12d	$⊢ x = z \to (F (x) \leq G (x) \leftrightarrow F (z) \leq G (z))$
30	29 28 27	ifbieq12d	$⊢ x = z \to if (F (x) \leq G (x), G (x), F (x)) = if (F (z) \leq G (z), G (z), F (z))$
31		fvex	$⊢ G (z) \in V$
32		fvex	$⊢ F (z) \in V$
33	31 32	ifex	$⊢ if (F (z) \leq G (z), G (z), F (z)) \in V$
34	30 5 33	fvmpt	$⊢ z \in A \to H (z) = if (F (z) \leq G (z), G (z), F (z))$
35	34	adantl	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to H (z) = if (F (z) \leq G (z), G (z), F (z))$
36	35	eleq1d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (y, +∞) \leftrightarrow if (F (z) \leq G (z), G (z), F (z)) \in (y, +∞))$
37	14 11	ifcld	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to if (F (z) \leq G (z), G (z), F (z)) \in ℝ$
38		ltpnf	$⊢ if (F (z) \leq G (z), G (z), F (z)) \in ℝ \to if (F (z) \leq G (z), G (z), F (z)) < +∞$
39	37 38	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land if (F (z) \leq G (z), G (z), F (z)) < +∞)$
40	39	biantrud	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < if (F (z) \leq G (z), G (z), F (z)) \leftrightarrow (y < if (F (z) \leq G (z), G (z), F (z)) \land (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land if (F (z) \leq G (z), G (z), F (z)) < +∞)))$
41	26 36 40	3bitr4d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (y, +∞) \leftrightarrow y < if (F (z) \leq G (z), G (z), F (z)))$
42	37	rexrd	$⊢ ((φ \land y \in ℝ^{}) \land z \in A) \to if (F (z) \leq G (z), G (z), F (z)) \in ℝ^{}$
43		xrltnle	$⊢ (y \in ℝ^{} \land if (F (z) \leq G (z), G (z), F (z)) \in ℝ^{}) \to (y < if (F (z) \leq G (z), G (z), F (z)) \leftrightarrow \neg if (F (z) \leq G (z), G (z), F (z)) \leq y)$
44	16 42 43	syl2anc	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < if (F (z) \leq G (z), G (z), F (z)) \leftrightarrow \neg if (F (z) \leq G (z), G (z), F (z)) \leq y)$
45	41 44	bitrd	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (y, +∞) \leftrightarrow \neg if (F (z) \leq G (z), G (z), F (z)) \leq y)$
46		elioo2	$⊢ (y \in ℝ^{} \land +∞ \in ℝ^{}) \to (F (z) \in (y, +∞) \leftrightarrow (F (z) \in ℝ \land y < F (z) \land F (z) < +∞))$
47	16 22 46	sylancl	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (y, +∞) \leftrightarrow (F (z) \in ℝ \land y < F (z) \land F (z) < +∞))$
48		3anan12	$⊢ (F (z) \in ℝ \land y < F (z) \land F (z) < +∞) \leftrightarrow (y < F (z) \land (F (z) \in ℝ \land F (z) < +∞))$
49	47 48	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (y, +∞) \leftrightarrow (y < F (z) \land (F (z) \in ℝ \land F (z) < +∞)))$
50		ltpnf	$⊢ F (z) \in ℝ \to F (z) < +∞$
51	11 50	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in ℝ \land F (z) < +∞)$
52	51	biantrud	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < F (z) \leftrightarrow (y < F (z) \land (F (z) \in ℝ \land F (z) < +∞)))$
53		xrltnle	$⊢ (y \in ℝ^{} \land F (z) \in ℝ^{}) \to (y < F (z) \leftrightarrow \neg F (z) \leq y)$
54	16 12 53	syl2anc	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < F (z) \leftrightarrow \neg F (z) \leq y)$
55	49 52 54	3bitr2d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (y, +∞) \leftrightarrow \neg F (z) \leq y)$
56		elioo2	$⊢ (y \in ℝ^{} \land +∞ \in ℝ^{}) \to (G (z) \in (y, +∞) \leftrightarrow (G (z) \in ℝ \land y < G (z) \land G (z) < +∞))$
57	16 22 56	sylancl	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (y, +∞) \leftrightarrow (G (z) \in ℝ \land y < G (z) \land G (z) < +∞))$
58		3anan12	$⊢ (G (z) \in ℝ \land y < G (z) \land G (z) < +∞) \leftrightarrow (y < G (z) \land (G (z) \in ℝ \land G (z) < +∞))$
59	57 58	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (y, +∞) \leftrightarrow (y < G (z) \land (G (z) \in ℝ \land G (z) < +∞)))$
60		ltpnf	$⊢ G (z) \in ℝ \to G (z) < +∞$
61	14 60	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in ℝ \land G (z) < +∞)$
62	61	biantrud	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < G (z) \leftrightarrow (y < G (z) \land (G (z) \in ℝ \land G (z) < +∞)))$
63		xrltnle	$⊢ (y \in ℝ^{} \land G (z) \in ℝ^{}) \to (y < G (z) \leftrightarrow \neg G (z) \leq y)$
64	16 15 63	syl2anc	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (y < G (z) \leftrightarrow \neg G (z) \leq y)$
65	59 62 64	3bitr2d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (y, +∞) \leftrightarrow \neg G (z) \leq y)$
66	55 65	orbi12d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to ((F (z) \in (y, +∞) \lor G (z) \in (y, +∞)) \leftrightarrow (\neg F (z) \leq y \lor \neg G (z) \leq y))$
67	21 45 66	3bitr4d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (y, +∞) \leftrightarrow (F (z) \in (y, +∞) \lor G (z) \in (y, +∞)))$
68	67	pm5.32da	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in A \land H (z) \in (y, +∞)) \leftrightarrow (z \in A \land (F (z) \in (y, +∞) \lor G (z) \in (y, +∞))))$
69		andi	$⊢ (z \in A \land (F (z) \in (y, +∞) \lor G (z) \in (y, +∞))) \leftrightarrow ((z \in A \land F (z) \in (y, +∞)) \lor (z \in A \land G (z) \in (y, +∞)))$
70	68 69	bitrdi	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in A \land H (z) \in (y, +∞)) \leftrightarrow ((z \in A \land F (z) \in (y, +∞)) \lor (z \in A \land G (z) \in (y, +∞))))$
71	9	ffnd	$⊢ φ \to H Fn A$
72	71	adantr	$⊢ (φ \land y \in ℝ^{*}) \to H Fn A$
73		elpreima	$⊢ H Fn A \to (z \in H^{-1} [(y, +∞)] \leftrightarrow (z \in A \land H (z) \in (y, +∞)))$
74	72 73	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(y, +∞)] \leftrightarrow (z \in A \land H (z) \in (y, +∞)))$
75	10	ffnd	$⊢ (φ \land y \in ℝ^{*}) \to F Fn A$
76		elpreima	$⊢ F Fn A \to (z \in F^{-1} [(y, +∞)] \leftrightarrow (z \in A \land F (z) \in (y, +∞)))$
77	75 76	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in F^{-1} [(y, +∞)] \leftrightarrow (z \in A \land F (z) \in (y, +∞)))$
78	13	ffnd	$⊢ (φ \land y \in ℝ^{*}) \to G Fn A$
79		elpreima	$⊢ G Fn A \to (z \in G^{-1} [(y, +∞)] \leftrightarrow (z \in A \land G (z) \in (y, +∞)))$
80	78 79	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in G^{-1} [(y, +∞)] \leftrightarrow (z \in A \land G (z) \in (y, +∞)))$
81	77 80	orbi12d	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in F^{-1} [(y, +∞)] \lor z \in G^{-1} [(y, +∞)]) \leftrightarrow ((z \in A \land F (z) \in (y, +∞)) \lor (z \in A \land G (z) \in (y, +∞))))$
82	70 74 81	3bitr4d	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(y, +∞)] \leftrightarrow (z \in F^{-1} [(y, +∞)] \lor z \in G^{-1} [(y, +∞)]))$
83		elun	$⊢ z \in (F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)]) \leftrightarrow (z \in F^{-1} [(y, +∞)] \lor z \in G^{-1} [(y, +∞)])$
84	82 83	bitr4di	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(y, +∞)] \leftrightarrow z \in (F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)]))$
85	84	eqrdv	$⊢ (φ \land y \in ℝ^{*}) \to H^{-1} [(y, +∞)] = F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)]$
86		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(y, +∞)] \in dom vol$
87	2 1 86	syl2anc	$⊢ φ \to F^{-1} [(y, +∞)] \in dom vol$
88		mbfima	$⊢ (G \in MblFn \land G : A ⟶ ℝ) \to G^{-1} [(y, +∞)] \in dom vol$
89	4 3 88	syl2anc	$⊢ φ \to G^{-1} [(y, +∞)] \in dom vol$
90		unmbl	$⊢ (F^{-1} [(y, +∞)] \in dom vol \land G^{-1} [(y, +∞)] \in dom vol) \to F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)] \in dom vol$
91	87 89 90	syl2anc	$⊢ φ \to F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)] \in dom vol$
92	91	adantr	$⊢ (φ \land y \in ℝ^{*}) \to F^{-1} [(y, +∞)] \cup G^{-1} [(y, +∞)] \in dom vol$
93	85 92	eqeltrd	$⊢ (φ \land y \in ℝ^{*}) \to H^{-1} [(y, +∞)] \in dom vol$
94		xrmaxlt	$⊢ (F (z) \in ℝ^{} \land G (z) \in ℝ^{} \land y \in ℝ^{*}) \to (if (F (z) \leq G (z), G (z), F (z)) < y \leftrightarrow (F (z) < y \land G (z) < y))$
95	12 15 16 94	syl3anc	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) < y \leftrightarrow (F (z) < y \land G (z) < y))$
96		mnfxr	$⊢ −∞ \in ℝ^{*}$
97		elioo2	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{}) \to (if (F (z) \leq G (z), G (z), F (z)) \in (−∞, y) \leftrightarrow (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < y))$
98	96 16 97	sylancr	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in (−∞, y) \leftrightarrow (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < y))$
99		df-3an	$⊢ (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z)) \land if (F (z) \leq G (z), G (z), F (z)) < y) \leftrightarrow ((if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z))) \land if (F (z) \leq G (z), G (z), F (z)) < y)$
100	98 99	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in (−∞, y) \leftrightarrow ((if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z))) \land if (F (z) \leq G (z), G (z), F (z)) < y))$
101	35	eleq1d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (−∞, y) \leftrightarrow if (F (z) \leq G (z), G (z), F (z)) \in (−∞, y))$
102		mnflt	$⊢ if (F (z) \leq G (z), G (z), F (z)) \in ℝ \to −∞ < if (F (z) \leq G (z), G (z), F (z))$
103	37 102	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z)))$
104	103	biantrurd	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (if (F (z) \leq G (z), G (z), F (z)) < y \leftrightarrow ((if (F (z) \leq G (z), G (z), F (z)) \in ℝ \land −∞ < if (F (z) \leq G (z), G (z), F (z))) \land if (F (z) \leq G (z), G (z), F (z)) < y))$
105	100 101 104	3bitr4d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (−∞, y) \leftrightarrow if (F (z) \leq G (z), G (z), F (z)) < y)$
106		mnflt	$⊢ F (z) \in ℝ \to −∞ < F (z)$
107	11 106	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in ℝ \land −∞ < F (z))$
108		elioo2	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{}) \to (F (z) \in (−∞, y) \leftrightarrow (F (z) \in ℝ \land −∞ < F (z) \land F (z) < y))$
109	96 16 108	sylancr	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (−∞, y) \leftrightarrow (F (z) \in ℝ \land −∞ < F (z) \land F (z) < y))$
110		df-3an	$⊢ (F (z) \in ℝ \land −∞ < F (z) \land F (z) < y) \leftrightarrow ((F (z) \in ℝ \land −∞ < F (z)) \land F (z) < y)$
111	109 110	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (−∞, y) \leftrightarrow ((F (z) \in ℝ \land −∞ < F (z)) \land F (z) < y))$
112	107 111	mpbirand	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (F (z) \in (−∞, y) \leftrightarrow F (z) < y)$
113		mnflt	$⊢ G (z) \in ℝ \to −∞ < G (z)$
114	14 113	jccir	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in ℝ \land −∞ < G (z))$
115		elioo2	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{}) \to (G (z) \in (−∞, y) \leftrightarrow (G (z) \in ℝ \land −∞ < G (z) \land G (z) < y))$
116	96 16 115	sylancr	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (−∞, y) \leftrightarrow (G (z) \in ℝ \land −∞ < G (z) \land G (z) < y))$
117		df-3an	$⊢ (G (z) \in ℝ \land −∞ < G (z) \land G (z) < y) \leftrightarrow ((G (z) \in ℝ \land −∞ < G (z)) \land G (z) < y)$
118	116 117	bitrdi	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (−∞, y) \leftrightarrow ((G (z) \in ℝ \land −∞ < G (z)) \land G (z) < y))$
119	114 118	mpbirand	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (G (z) \in (−∞, y) \leftrightarrow G (z) < y)$
120	112 119	anbi12d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to ((F (z) \in (−∞, y) \land G (z) \in (−∞, y)) \leftrightarrow (F (z) < y \land G (z) < y))$
121	95 105 120	3bitr4d	$⊢ ((φ \land y \in ℝ^{*}) \land z \in A) \to (H (z) \in (−∞, y) \leftrightarrow (F (z) \in (−∞, y) \land G (z) \in (−∞, y)))$
122	121	pm5.32da	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in A \land H (z) \in (−∞, y)) \leftrightarrow (z \in A \land (F (z) \in (−∞, y) \land G (z) \in (−∞, y))))$
123		anandi	$⊢ (z \in A \land (F (z) \in (−∞, y) \land G (z) \in (−∞, y))) \leftrightarrow ((z \in A \land F (z) \in (−∞, y)) \land (z \in A \land G (z) \in (−∞, y)))$
124	122 123	bitrdi	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in A \land H (z) \in (−∞, y)) \leftrightarrow ((z \in A \land F (z) \in (−∞, y)) \land (z \in A \land G (z) \in (−∞, y))))$
125		elpreima	$⊢ H Fn A \to (z \in H^{-1} [(−∞, y)] \leftrightarrow (z \in A \land H (z) \in (−∞, y)))$
126	72 125	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(−∞, y)] \leftrightarrow (z \in A \land H (z) \in (−∞, y)))$
127		elpreima	$⊢ F Fn A \to (z \in F^{-1} [(−∞, y)] \leftrightarrow (z \in A \land F (z) \in (−∞, y)))$
128	75 127	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in F^{-1} [(−∞, y)] \leftrightarrow (z \in A \land F (z) \in (−∞, y)))$
129		elpreima	$⊢ G Fn A \to (z \in G^{-1} [(−∞, y)] \leftrightarrow (z \in A \land G (z) \in (−∞, y)))$
130	78 129	syl	$⊢ (φ \land y \in ℝ^{*}) \to (z \in G^{-1} [(−∞, y)] \leftrightarrow (z \in A \land G (z) \in (−∞, y)))$
131	128 130	anbi12d	$⊢ (φ \land y \in ℝ^{*}) \to ((z \in F^{-1} [(−∞, y)] \land z \in G^{-1} [(−∞, y)]) \leftrightarrow ((z \in A \land F (z) \in (−∞, y)) \land (z \in A \land G (z) \in (−∞, y))))$
132	124 126 131	3bitr4d	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(−∞, y)] \leftrightarrow (z \in F^{-1} [(−∞, y)] \land z \in G^{-1} [(−∞, y)]))$
133		elin	$⊢ z \in (F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)]) \leftrightarrow (z \in F^{-1} [(−∞, y)] \land z \in G^{-1} [(−∞, y)])$
134	132 133	bitr4di	$⊢ (φ \land y \in ℝ^{*}) \to (z \in H^{-1} [(−∞, y)] \leftrightarrow z \in (F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)]))$
135	134	eqrdv	$⊢ (φ \land y \in ℝ^{*}) \to H^{-1} [(−∞, y)] = F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)]$
136		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(−∞, y)] \in dom vol$
137	2 1 136	syl2anc	$⊢ φ \to F^{-1} [(−∞, y)] \in dom vol$
138		mbfima	$⊢ (G \in MblFn \land G : A ⟶ ℝ) \to G^{-1} [(−∞, y)] \in dom vol$
139	4 3 138	syl2anc	$⊢ φ \to G^{-1} [(−∞, y)] \in dom vol$
140		inmbl	$⊢ (F^{-1} [(−∞, y)] \in dom vol \land G^{-1} [(−∞, y)] \in dom vol) \to F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)] \in dom vol$
141	137 139 140	syl2anc	$⊢ φ \to F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)] \in dom vol$
142	141	adantr	$⊢ (φ \land y \in ℝ^{*}) \to F^{-1} [(−∞, y)] \cap G^{-1} [(−∞, y)] \in dom vol$
143	135 142	eqeltrd	$⊢ (φ \land y \in ℝ^{*}) \to H^{-1} [(−∞, y)] \in dom vol$
144	9 93 143	ismbfd	$⊢ φ \to H \in MblFn$

Metamath Proof Explorer

Theorem mbfmax

Proof