# Metamath Proof Explorer

## Theorem mbfmax

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

Ref Expression
Hypotheses mbfmax.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
mbfmax.2 ${⊢}{\phi }\to {F}\in MblFn$
mbfmax.3 ${⊢}{\phi }\to {G}:{A}⟶ℝ$
mbfmax.4 ${⊢}{\phi }\to {G}\in MblFn$
mbfmax.5 ${⊢}{H}=\left({x}\in {A}⟼if\left({F}\left({x}\right)\le {G}\left({x}\right),{G}\left({x}\right),{F}\left({x}\right)\right)\right)$
Assertion mbfmax ${⊢}{\phi }\to {H}\in MblFn$

### Proof

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