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 25975

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 7084	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ)
3		mbfmax.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
4	3	ffvelcdmda 7084	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ)
5	2, 4	ifcld 4528	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ)
6		mbfmax.5	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))
7	5, 6	fmptd 7114	. 2 ⊢ (𝜑 → 𝐻:𝐴⟶ℝ)
8	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹:𝐴⟶ℝ)
9	8	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ)
10	9	rexrd 11362	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ^)
11	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺:𝐴⟶ℝ)
12	11	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
13	12	rexrd 11362	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ^)
14		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ^)
15		xrmaxle 13316	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
16	10, 13, 14, 15	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
17	16	notbid 321	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦)))
18		ianor 997	. . . . . . . . . 10 ⊢ (¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))
19	17, 18	bitrdi 290	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
20		pnfxr 11366	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
21		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
22	14, 20, 21	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
23		3anan12 1112	. . . . . . . . . . . 12 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))
24	22, 23	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
25		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
26		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
27	25, 26	breq12d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧)))
28	27, 26, 25	ifbieq12d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
29		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘𝑧) ∈ V
30		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑧) ∈ V
31	29, 30	ifex 4532	. . . . . . . . . . . . . 14 ⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V
32	28, 6, 31	fvmpt 6993	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
33	32	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
34	33	eleq1d 2845	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞)))
35	12, 9	ifcld 4528	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ)
36		ltpnf 13252	. . . . . . . . . . . . 13 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)
37	35, 36	jccir 531	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))
38	37	biantrud 541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))))
39	24, 34, 38	3bitr4d 314	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
40	35	rexrd 11362	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^)
41		xrltnle 11379	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
42	14, 40, 41	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
43	39, 42	bitrd 282	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
44		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
45	14, 20, 44	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
46		3anan12 1112	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))
47	45, 46	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
48		ltpnf 13252	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞)
49	9, 48	jccir 531	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))
50	49	biantrud 541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
51		xrltnle 11379	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐹‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
52	14, 10, 51	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
53	47, 50, 52	3bitr2d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
54		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
55	14, 20, 54	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
56		3anan12 1112	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))
57	55, 56	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
58		ltpnf 13252	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞)
59	12, 58	jccir 531	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))
60	59	biantrud 541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
61		xrltnle 11379	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
62	14, 13, 61	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
63	57, 60, 62	3bitr2d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦))
64	53, 63	orbi12d 932	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)))
65	19, 43, 64	3bitr4d 314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
66	65	pm5.32da 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
67		andi 1025	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
68	66, 67	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
69	7	ffnd 6710	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn 𝐴)
70	69	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐻 Fn 𝐴)
71		elpreima 7057	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
72	70, 71	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
73	8	ffnd 6710	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹 Fn 𝐴)
74		elpreima 7057	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
75	73, 74	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
76	11	ffnd 6710	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺 Fn 𝐴)
77		elpreima 7057	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
78	76, 77	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
79	75, 78	orbi12d 932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
80	68, 72, 79	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)))))
81		elun 4152	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))))
82	80, 81	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞)))))
83	82	eqrdv 2758	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) = ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))))
84		mbfmax.2	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
85		mbfima 25956	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
86	84, 3, 85	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
87		mbfmax.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ MblFn)
88		mbfima 25956	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
89	87, 1, 88	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
90		unmbl 25863	. . . . 5 ⊢ (((^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
91	86, 89, 90	syl2anc 596	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
92	91	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
93	83, 92	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
94		xrmaxlt 13314	. . . . . . . . . 10 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
95	10, 13, 14, 94	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
96		mnfxr 11369	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
97		elioo2 13520	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
98	96, 14, 97	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
99		df-3an 1105	. . . . . . . . . . 11 ⊢ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
100	98, 99	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
101	33	eleq1d 2845	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦)))
102		mnflt 13255	. . . . . . . . . . . 12 ⊢ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
103	35, 102	jccir 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))))
104	103	biantrurd 542	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)))
105	100, 101, 104	3bitr4d 314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))
106		mnflt 13255	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧))
107	9, 106	jccir 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)))
108		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
109	96, 14, 108	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦)))
110		df-3an 1105	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))
111	109, 110	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)))
112	107, 111	mpbirand 720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦))
113		mnflt 13255	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧))
114	12, 113	jccir 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)))
115		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
116	96, 14, 115	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦)))
117		df-3an 1105	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))
118	116, 117	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)))
119	114, 118	mpbirand 720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦))
120	112, 119	anbi12d 644	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
121	95, 105, 120	3bitr4d 314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
122	121	pm5.32da 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
123		anandi 689	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
124	122, 123	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
125		elpreima 7057	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
126	70, 125	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
127		elpreima 7057	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
128	73, 127	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
129		elpreima 7057	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
130	76, 129	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
131	128, 130	anbi12d 644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
132	124, 126, 131	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)))))
133		elin 4093	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))))
134	132, 133	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦)))))
135	134	eqrdv 2758	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) = ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))))
136		mbfima 25956	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
137	84, 3, 136	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
138		mbfima 25956	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
139	87, 1, 138	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
140		inmbl 25868	. . . . 5 ⊢ (((^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
141	137, 139, 140	syl2anc 596	. . . 4 ⊢ (𝜑 → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
142	141	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
143	135, 142	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
144	7, 93, 143	ismbfd 25965	1 ⊢ (𝜑 → 𝐻 ∈ MblFn)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∩ cin 4089 ∪ cun 4149 ifcif 4481 class class class wbr 5102 ↦ cmpt 5185 ^◡ccnv 5649 dom cdm 5650 “ cima 5653 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℝcr 11202 +∞cpnf 11343 -∞cmnf 11344 ℝ^*cxr 11345 < clt 11346 ≤ cle 11347 (,)cioo 13479 volcvol 25789 MblFncmbf 25940

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-map 8852 df-pm 8853 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-sup 9437 df-inf 9438 df-oi 9507 df-dju 9985 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-n0 12610 df-z 12697 df-uz 12969 df-q 13079 df-rp 13124 df-xadd 13245 df-ioo 13483 df-ico 13485 df-icc 13486 df-fz 13643 df-fzo 13792 df-fl 13935 df-seq 14148 df-exp 14208 df-hash 14478 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-clim 15660 df-sum 15859 df-xmet 21676 df-met 21677 df-ovol 25790 df-vol 25791 df-mbf 25945

This theorem is used by: mbfpos 25977

W3C validator