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 25769

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 7069	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ)
3		mbfmax.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
4	3	ffvelcdmda 7069	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ)
5	2, 4	ifcld 4530	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ)
6		mbfmax.5	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))
7	5, 6	fmptd 7099	. 2 ⊢ (𝜑 → 𝐻:𝐴⟶ℝ)
8	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹:𝐴⟶ℝ)
9	8	ffvelcdmda 7069	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ)
10	9	rexrd 11247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ^)
11	1	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺:𝐴⟶ℝ)
12	11	ffvelcdmda 7069	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
13	12	rexrd 11247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ^)
14		simplr 780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ^)
15		xrmaxle 13200	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
16	10, 13, 14, 15	syl3anc 1394	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
17	16	notbid 321	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
18		ianor 997	. . . . . . . . . 10 ⊢ (¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))
19	17, 18	bitrdi 290	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
20		pnfxr 11251	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
21		elioo2 13404	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
22	14, 20, 21	sylancl 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
23		3anan12 1110	. . . . . . . . . . . 12 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
24	22, 23	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
25		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
26		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
27	25, 26	breq12d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧)))
28	27, 26, 25	ifbieq12d 4512	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
29		fvex 6884	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘𝑧) ∈ V
30		fvex 6884	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑧) ∈ V
31	29, 30	ifex 4534	. . . . . . . . . . . . . 14 ⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V
32	28, 6, 31	fvmpt 6979	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
33	32	adantl 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
34	33	eleq1d 2850	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞)))
35	12, 9	ifcld 4530	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ)
36		ltpnf 13136	. . . . . . . . . . . . 13 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)
37	35, 36	jccir 530	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))
38	37	biantrud 540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
39	24, 34, 38	3bitr4d 314	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
40	35	rexrd 11247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^)
41		xrltnle 11264	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
42	14, 40, 41	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
43	39, 42	bitrd 282	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
44		elioo2 13404	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
45	14, 20, 44	sylancl 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
46		3anan12 1110	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))
47	45, 46	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
48		ltpnf 13136	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞)
49	9, 48	jccir 530	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))
50	49	biantrud 540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
51		xrltnle 11264	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐹‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
52	14, 10, 51	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
53	47, 50, 52	3bitr2d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
54		elioo2 13404	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
55	14, 20, 54	sylancl 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
56		3anan12 1110	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))
57	55, 56	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
58		ltpnf 13136	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞)
59	12, 58	jccir 530	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))
60	59	biantrud 540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
61		xrltnle 11264	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
62	14, 13, 61	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
63	57, 60, 62	3bitr2d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
64	53, 63	orbi12d 931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
65	19, 43, 64	3bitr4d 314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
66	65	pm5.32da 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
67		andi 1023	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
68	66, 67	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
69	7	ffnd 6696	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn 𝐴)
70	69	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐻 Fn 𝐴)
71		elpreima 7043	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
72	70, 71	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
73	8	ffnd 6696	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹 Fn 𝐴)
74		elpreima 7043	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
75	73, 74	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
76	11	ffnd 6696	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺 Fn 𝐴)
77		elpreima 7043	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
78	76, 77	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
79	75, 78	orbi12d 931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
80	68, 72, 79	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)))))
81		elun 4109	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))))
82	80, 81	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞)))))
83	82	eqrdv 2763	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) = ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))))
84		mbfmax.2	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
85		mbfima 25750	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
86	84, 3, 85	syl2anc 595	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
87		mbfmax.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ MblFn)
88		mbfima 25750	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
89	87, 1, 88	syl2anc 595	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
90		unmbl 25657	. . . . 5 ⊢ (((^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
91	86, 89, 90	syl2anc 595	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
92	91	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
93	83, 92	eqeltrd 2865	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
94		xrmaxlt 13198	. . . . . . . . . 10 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
95	10, 13, 14, 94	syl3anc 1394	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
96		mnfxr 11254	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
97		elioo2 13404	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
98	96, 14, 97	sylancr 598	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
99		df-3an 1103	. . . . . . . . . . 11 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
100	98, 99	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
101	33	eleq1d 2850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦)))
102		mnflt 13139	. . . . . . . . . . . 12 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
103	35, 102	jccir 530	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
104	103	biantrurd 541	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
105	100, 101, 104	3bitr4d 314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
106		mnflt 13139	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧))
107	9, 106	jccir 530	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)))
108		elioo2 13404	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
109	96, 14, 108	sylancr 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
110		df-3an 1103	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))
111	109, 110	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)))
112	107, 111	mpbirand 719	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦))
113		mnflt 13139	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧))
114	12, 113	jccir 530	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)))
115		elioo2 13404	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
116	96, 14, 115	sylancr 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
117		df-3an 1103	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))
118	116, 117	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)))
119	114, 118	mpbirand 719	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦))
120	112, 119	anbi12d 643	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
121	95, 105, 120	3bitr4d 314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
122	121	pm5.32da 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
123		anandi 688	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
124	122, 123	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
125		elpreima 7043	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
126	70, 125	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
127		elpreima 7043	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
128	73, 127	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
129		elpreima 7043	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
130	76, 129	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
131	128, 130	anbi12d 643	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
132	124, 126, 131	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)))))
133		elin 3923	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))))
134	132, 133	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦)))))
135	134	eqrdv 2763	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) = ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))))
136		mbfima 25750	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
137	84, 3, 136	syl2anc 595	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
138		mbfima 25750	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
139	87, 1, 138	syl2anc 595	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
140		inmbl 25662	. . . . 5 ⊢ (((^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
141	137, 139, 140	syl2anc 595	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
142	141	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
143	135, 142	eqeltrd 2865	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
144	7, 93, 143	ismbfd 25759	1 ⊢ (𝜑 → 𝐻 ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∪ cun 3905 ∩ cin 3906 ifcif 4483 class class class wbr 5105 ↦ cmpt 5186 ^◡ccnv 5651 dom cdm 5652 “ cima 5655 Fn wfn 6520 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ℝcr 11087 +∞cpnf 11228 -∞cmnf 11229 ℝ^*cxr 11230 < clt 11231 ≤ cle 11232 (,)cioo 13363 volcvol 25583 MblFncmbf 25734

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-map 8814 df-pm 8815 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9875 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-n0 12496 df-z 12583 df-uz 12854 df-q 12964 df-rp 13008 df-xadd 13129 df-ioo 13367 df-ico 13369 df-icc 13370 df-fz 13527 df-fzo 13674 df-fl 13816 df-seq 14029 df-exp 14089 df-hash 14358 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-clim 15529 df-sum 15728 df-xmet 21475 df-met 21476 df-ovol 25584 df-vol 25585 df-mbf 25739

This theorem is referenced by: mbfpos 25771

W3C validator