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 25157

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	ffvelcdmda 7083	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ)
3		mbfmax.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
4	3	ffvelcdmda 7083	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ)
5	2, 4	ifcld 4573	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ)
6		mbfmax.5	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))
7	5, 6	fmptd 7110	. 2 ⊢ (𝜑 → 𝐻:𝐴⟶ℝ)
8	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹:𝐴⟶ℝ)
9	8	ffvelcdmda 7083	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ)
10	9	rexrd 11260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ^)
11	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺:𝐴⟶ℝ)
12	11	ffvelcdmda 7083	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
13	12	rexrd 11260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ^)
14		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ^)
15		xrmaxle 13158	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
16	10, 13, 14, 15	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
17	16	notbid 317	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
18		ianor 980	. . . . . . . . . 10 ⊢ (¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))
19	17, 18	bitrdi 286	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
20		pnfxr 11264	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
21		elioo2 13361	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
22	14, 20, 21	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
23		3anan12 1096	. . . . . . . . . . . 12 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
24	22, 23	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
25		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
26		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
27	25, 26	breq12d 5160	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧)))
28	27, 26, 25	ifbieq12d 4555	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
29		fvex 6901	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘𝑧) ∈ V
30		fvex 6901	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑧) ∈ V
31	29, 30	ifex 4577	. . . . . . . . . . . . . 14 ⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V
32	28, 6, 31	fvmpt 6995	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
33	32	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
34	33	eleq1d 2818	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞)))
35	12, 9	ifcld 4573	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ)
36		ltpnf 13096	. . . . . . . . . . . . 13 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)
37	35, 36	jccir 522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))
38	37	biantrud 532	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
39	24, 34, 38	3bitr4d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
40	35	rexrd 11260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^)
41		xrltnle 11277	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
42	14, 40, 41	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
43	39, 42	bitrd 278	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
44		elioo2 13361	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
45	14, 20, 44	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
46		3anan12 1096	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))
47	45, 46	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
48		ltpnf 13096	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞)
49	9, 48	jccir 522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))
50	49	biantrud 532	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
51		xrltnle 11277	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐹‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
52	14, 10, 51	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
53	47, 50, 52	3bitr2d 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
54		elioo2 13361	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
55	14, 20, 54	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
56		3anan12 1096	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))
57	55, 56	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
58		ltpnf 13096	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞)
59	12, 58	jccir 522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))
60	59	biantrud 532	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
61		xrltnle 11277	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
62	14, 13, 61	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
63	57, 60, 62	3bitr2d 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
64	53, 63	orbi12d 917	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
65	19, 43, 64	3bitr4d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
66	65	pm5.32da 579	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
67		andi 1006	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
68	66, 67	bitrdi 286	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
69	7	ffnd 6715	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn 𝐴)
70	69	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐻 Fn 𝐴)
71		elpreima 7056	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
72	70, 71	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
73	8	ffnd 6715	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹 Fn 𝐴)
74		elpreima 7056	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
75	73, 74	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
76	11	ffnd 6715	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺 Fn 𝐴)
77		elpreima 7056	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
78	76, 77	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
79	75, 78	orbi12d 917	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
80	68, 72, 79	3bitr4d 310	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)))))
81		elun 4147	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))))
82	80, 81	bitr4di 288	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞)))))
83	82	eqrdv 2730	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) = ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))))
84		mbfmax.2	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
85		mbfima 25138	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
86	84, 3, 85	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
87		mbfmax.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ MblFn)
88		mbfima 25138	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
89	87, 1, 88	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
90		unmbl 25045	. . . . 5 ⊢ (((^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
91	86, 89, 90	syl2anc 584	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
92	91	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
93	83, 92	eqeltrd 2833	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
94		xrmaxlt 13156	. . . . . . . . . 10 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
95	10, 13, 14, 94	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
96		mnfxr 11267	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
97		elioo2 13361	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
98	96, 14, 97	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
99		df-3an 1089	. . . . . . . . . . 11 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
100	98, 99	bitrdi 286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
101	33	eleq1d 2818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦)))
102		mnflt 13099	. . . . . . . . . . . 12 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
103	35, 102	jccir 522	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
104	103	biantrurd 533	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
105	100, 101, 104	3bitr4d 310	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
106		mnflt 13099	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧))
107	9, 106	jccir 522	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)))
108		elioo2 13361	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
109	96, 14, 108	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
110		df-3an 1089	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))
111	109, 110	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)))
112	107, 111	mpbirand 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦))
113		mnflt 13099	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧))
114	12, 113	jccir 522	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)))
115		elioo2 13361	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
116	96, 14, 115	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
117		df-3an 1089	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))
118	116, 117	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)))
119	114, 118	mpbirand 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦))
120	112, 119	anbi12d 631	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
121	95, 105, 120	3bitr4d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
122	121	pm5.32da 579	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
123		anandi 674	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
124	122, 123	bitrdi 286	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
125		elpreima 7056	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
126	70, 125	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
127		elpreima 7056	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
128	73, 127	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
129		elpreima 7056	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
130	76, 129	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
131	128, 130	anbi12d 631	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
132	124, 126, 131	3bitr4d 310	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)))))
133		elin 3963	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))))
134	132, 133	bitr4di 288	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦)))))
135	134	eqrdv 2730	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) = ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))))
136		mbfima 25138	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
137	84, 3, 136	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
138		mbfima 25138	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
139	87, 1, 138	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
140		inmbl 25050	. . . . 5 ⊢ (((^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
141	137, 139, 140	syl2anc 584	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
142	141	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
143	135, 142	eqeltrd 2833	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
144	7, 93, 143	ismbfd 25147	1 ⊢ (𝜑 → 𝐻 ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∪ cun 3945 ∩ cin 3946 ifcif 4527 class class class wbr 5147 ↦ cmpt 5230 ^◡ccnv 5674 dom cdm 5675 “ cima 5678 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ℝcr 11105 +∞cpnf 11241 -∞cmnf 11242 ℝ^*cxr 11243 < clt 11244 ≤ cle 11245 (,)cioo 13320 volcvol 24971 MblFncmbf 25122

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-z 12555 df-uz 12819 df-q 12929 df-rp 12971 df-xadd 13089 df-ioo 13324 df-ico 13326 df-icc 13327 df-fz 13481 df-fzo 13624 df-fl 13753 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629 df-xmet 20929 df-met 20930 df-ovol 24972 df-vol 24973 df-mbf 25127

This theorem is referenced by: mbfpos 25159

W3C validator