mbfmax - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfmax		Structured version Visualization version GIF version

Theorem mbfmax 24718

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

**Hypotheses**
Ref	Expression
mbfmax.1	⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
mbfmax.2	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfmax.3	⊢ (𝜑 → 𝐺:𝐴⟶ℝ)
mbfmax.4	⊢ (𝜑 → 𝐺 ∈ MblFn)
mbfmax.5	⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))

**Assertion**
Ref	Expression
mbfmax	⊢ (𝜑 → 𝐻 ∈ MblFn)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐹 𝑥,𝐺 𝜑,𝑥 Allowed substitution hint: 𝐻(𝑥)

Proof of Theorem mbfmax Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfmax.3	. . . . 5 ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)
2	1	ffvelrnda 6943	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ)
3		mbfmax.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
4	3	ffvelrnda 6943	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ)
5	2, 4	ifcld 4502	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ)
6		mbfmax.5	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))
7	5, 6	fmptd 6970	. 2 ⊢ (𝜑 → 𝐻:𝐴⟶ℝ)
8	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹:𝐴⟶ℝ)
9	8	ffvelrnda 6943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ)
10	9	rexrd 10956	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ^)
11	1	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺:𝐴⟶ℝ)
12	11	ffvelrnda 6943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
13	12	rexrd 10956	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ^)
14		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ^)
15		xrmaxle 12846	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
16	10, 13, 14, 15	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
17	16	notbid 317	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
18		ianor 978	. . . . . . . . . 10 ⊢ (¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))
19	17, 18	bitrdi 286	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
20		pnfxr 10960	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
21		elioo2 13049	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
22	14, 20, 21	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
23		3anan12 1094	. . . . . . . . . . . 12 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
24	22, 23	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
25		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
26		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
27	25, 26	breq12d 5083	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧)))
28	27, 26, 25	ifbieq12d 4484	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
29		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘𝑧) ∈ V
30		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑧) ∈ V
31	29, 30	ifex 4506	. . . . . . . . . . . . . 14 ⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V
32	28, 6, 31	fvmpt 6857	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
33	32	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
34	33	eleq1d 2823	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞)))
35	12, 9	ifcld 4502	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ)
36		ltpnf 12785	. . . . . . . . . . . . 13 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)
37	35, 36	jccir 521	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))
38	37	biantrud 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
39	24, 34, 38	3bitr4d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
40	35	rexrd 10956	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^)
41		xrltnle 10973	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
42	14, 40, 41	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
43	39, 42	bitrd 278	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
44		elioo2 13049	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
45	14, 20, 44	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
46		3anan12 1094	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))
47	45, 46	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
48		ltpnf 12785	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞)
49	9, 48	jccir 521	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))
50	49	biantrud 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
51		xrltnle 10973	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐹‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
52	14, 10, 51	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
53	47, 50, 52	3bitr2d 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
54		elioo2 13049	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
55	14, 20, 54	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
56		3anan12 1094	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))
57	55, 56	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
58		ltpnf 12785	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞)
59	12, 58	jccir 521	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))
60	59	biantrud 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
61		xrltnle 10973	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
62	14, 13, 61	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
63	57, 60, 62	3bitr2d 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
64	53, 63	orbi12d 915	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
65	19, 43, 64	3bitr4d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
66	65	pm5.32da 578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
67		andi 1004	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
68	66, 67	bitrdi 286	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
69	7	ffnd 6585	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn 𝐴)
70	69	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐻 Fn 𝐴)
71		elpreima 6917	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
72	70, 71	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
73	8	ffnd 6585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹 Fn 𝐴)
74		elpreima 6917	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
75	73, 74	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
76	11	ffnd 6585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺 Fn 𝐴)
77		elpreima 6917	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
78	76, 77	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
79	75, 78	orbi12d 915	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
80	68, 72, 79	3bitr4d 310	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)))))
81		elun 4079	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))))
82	80, 81	bitr4di 288	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞)))))
83	82	eqrdv 2736	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) = ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))))
84		mbfmax.2	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
85		mbfima 24699	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
86	84, 3, 85	syl2anc 583	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
87		mbfmax.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ MblFn)
88		mbfima 24699	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
89	87, 1, 88	syl2anc 583	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
90		unmbl 24606	. . . . 5 ⊢ (((^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
91	86, 89, 90	syl2anc 583	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
92	91	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
93	83, 92	eqeltrd 2839	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
94		xrmaxlt 12844	. . . . . . . . . 10 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
95	10, 13, 14, 94	syl3anc 1369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
96		mnfxr 10963	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
97		elioo2 13049	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
98	96, 14, 97	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
99		df-3an 1087	. . . . . . . . . . 11 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
100	98, 99	bitrdi 286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
101	33	eleq1d 2823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦)))
102		mnflt 12788	. . . . . . . . . . . 12 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
103	35, 102	jccir 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
104	103	biantrurd 532	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
105	100, 101, 104	3bitr4d 310	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
106		mnflt 12788	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧))
107	9, 106	jccir 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)))
108		elioo2 13049	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
109	96, 14, 108	sylancr 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
110		df-3an 1087	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))
111	109, 110	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)))
112	107, 111	mpbirand 703	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦))
113		mnflt 12788	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧))
114	12, 113	jccir 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)))
115		elioo2 13049	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
116	96, 14, 115	sylancr 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
117		df-3an 1087	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))
118	116, 117	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)))
119	114, 118	mpbirand 703	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦))
120	112, 119	anbi12d 630	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
121	95, 105, 120	3bitr4d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
122	121	pm5.32da 578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
123		anandi 672	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
124	122, 123	bitrdi 286	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
125		elpreima 6917	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
126	70, 125	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
127		elpreima 6917	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
128	73, 127	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
129		elpreima 6917	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
130	76, 129	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
131	128, 130	anbi12d 630	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
132	124, 126, 131	3bitr4d 310	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)))))
133		elin 3899	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))))
134	132, 133	bitr4di 288	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦)))))
135	134	eqrdv 2736	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) = ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))))
136		mbfima 24699	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
137	84, 3, 136	syl2anc 583	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
138		mbfima 24699	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
139	87, 1, 138	syl2anc 583	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
140		inmbl 24611	. . . . 5 ⊢ (((^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
141	137, 139, 140	syl2anc 583	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
142	141	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
143	135, 142	eqeltrd 2839	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
144	7, 93, 143	ismbfd 24708	1 ⊢ (𝜑 → 𝐻 ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∪ cun 3881 ∩ cin 3882 ifcif 4456 class class class wbr 5070 ↦ cmpt 5153 ^◡ccnv 5579 dom cdm 5580 “ cima 5583 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ℝcr 10801 +∞cpnf 10937 -∞cmnf 10938 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 (,)cioo 13008 volcvol 24532 MblFncmbf 24683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-xadd 12778 df-ioo 13012 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326 df-xmet 20503 df-met 20504 df-ovol 24533 df-vol 24534 df-mbf 24688

This theorem is referenced by: mbfpos 24720

W3C validator