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 25845

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 7086	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ)
3		mbfmax.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
4	3	ffvelcdmda 7086	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ)
5	2, 4	ifcld 4539	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ)
6		mbfmax.5	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))
7	5, 6	fmptd 7116	. 2 ⊢ (𝜑 → 𝐻:𝐴⟶ℝ)
8	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹:𝐴⟶ℝ)
9	8	ffvelcdmda 7086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ)
10	9	rexrd 11277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ^)
11	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺:𝐴⟶ℝ)
12	11	ffvelcdmda 7086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
13	12	rexrd 11277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ^)
14		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ^)
15		xrmaxle 13227	. . . . . . . . . . . 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 11281	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
21		elioo2 13431	. . . . . . . . . . . . 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 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
26		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
27	25, 26	breq12d 5127	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧)))
28	27, 26, 25	ifbieq12d 4521	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
29		fvex 6901	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘𝑧) ∈ V
30		fvex 6901	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑧) ∈ V
31	29, 30	ifex 4543	. . . . . . . . . . . . . 14 ⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V
32	28, 6, 31	fvmpt 6996	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
33	32	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))
34	33	eleq1d 2851	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞)))
35	12, 9	ifcld 4539	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ)
36		ltpnf 13163	. . . . . . . . . . . . 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 11277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^)
41		xrltnle 11294	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ^*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
42	14, 40, 41	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
43	39, 42	bitrd 282	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦))
44		elioo2 13431	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
45	14, 20, 44	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞)))
46		3anan12 1112	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))
47	45, 46	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
48		ltpnf 13163	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞)
49	9, 48	jccir 531	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))
50	49	biantrud 541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))))
51		xrltnle 11294	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ^* ∧ (𝐹‘𝑧) ∈ ℝ^*) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
52	14, 10, 51	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
53	47, 50, 52	3bitr2d 310	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦))
54		elioo2 13431	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
55	14, 20, 54	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞)))
56		3anan12 1112	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))
57	55, 56	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
58		ltpnf 13163	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞)
59	12, 58	jccir 531	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))
60	59	biantrud 541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))))
61		xrltnle 11294	. . . . . . . . . . . 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 6713	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn 𝐴)
70	69	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐻 Fn 𝐴)
71		elpreima 7060	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
72	70, 71	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞))))
73	8	ffnd 6713	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐹 Fn 𝐴)
74		elpreima 7060	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
75	73, 74	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞))))
76	11	ffnd 6713	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → 𝐺 Fn 𝐴)
77		elpreima 7060	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
78	76, 77	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))
79	75, 78	orbi12d 932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))))
80	68, 72, 79	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞)))))
81		elun 4110	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (^◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (^◡𝐺 “ (𝑦(,)+∞))))
82	80, 81	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞)))))
83	82	eqrdv 2764	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) = ((^◡𝐹 “ (𝑦(,)+∞)) ∪ (^◡𝐺 “ (𝑦(,)+∞))))
84		mbfmax.2	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
85		mbfima 25826	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
86	84, 3, 85	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
87		mbfmax.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ MblFn)
88		mbfima 25826	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
89	87, 1, 88	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
90		unmbl 25733	. . . . 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 2866	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
94		xrmaxlt 13225	. . . . . . . . . 10 ⊢ (((𝐹‘𝑧) ∈ ℝ^* ∧ (𝐺‘𝑧) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
95	10, 13, 14, 94	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦)))
96		mnfxr 11284	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
97		elioo2 13431	. . . . . . . . . . . 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 2851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦)))
102		mnflt 13166	. . . . . . . . . . . 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 13166	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧))
107	9, 106	jccir 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)))
108		elioo2 13431	. . . . . . . . . . . . 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 13166	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧))
114	12, 113	jccir 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ^*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)))
115		elioo2 13431	. . . . . . . . . . . . 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 7060	. . . . . . 7 ⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
126	70, 125	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦))))
127		elpreima 7060	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
128	73, 127	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦))))
129		elpreima 7060	. . . . . . . 8 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
130	76, 129	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))
131	128, 130	anbi12d 644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → ((𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))))
132	124, 126, 131	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦)))))
133		elin 3924	. . . . 5 ⊢ (𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (^◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (^◡𝐺 “ (-∞(,)𝑦))))
134	132, 133	bitr4di 292	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (𝑧 ∈ (^◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦)))))
135	134	eqrdv 2764	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) = ((^◡𝐹 “ (-∞(,)𝑦)) ∩ (^◡𝐺 “ (-∞(,)𝑦))))
136		mbfima 25826	. . . . . 6 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
137	84, 3, 136	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
138		mbfima 25826	. . . . . 6 ⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
139	87, 1, 138	syl2anc 596	. . . . 5 ⊢ (𝜑 → (^◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
140		inmbl 25738	. . . . 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 2866	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ^*) → (^◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
144	7, 93, 143	ismbfd 25835	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 1570 ∈ wcel 2146 ∪ cun 3906 ∩ cin 3907 ifcif 4492 class class class wbr 5114 ↦ cmpt 5197 ^◡ccnv 5665 dom cdm 5666 “ cima 5669 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ℝcr 11117 +∞cpnf 11258 -∞cmnf 11259 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 (,)cioo 13390 volcvol 25659 MblFncmbf 25810

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-er 8703 df-map 8835 df-pm 8836 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-q 12991 df-rp 13035 df-xadd 13156 df-ioo 13394 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-xmet 21552 df-met 21553 df-ovol 25660 df-vol 25661 df-mbf 25815

This theorem is used by: mbfpos 25847

W3C validator