| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mbfmax.3 | . . . . 5
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) | 
| 2 | 1 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ) | 
| 3 |  | mbfmax.1 | . . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) | 
| 4 | 3 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) | 
| 5 | 2, 4 | ifcld 4571 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ) | 
| 6 |  | mbfmax.5 | . . 3
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥))) | 
| 7 | 5, 6 | fmptd 7133 | . 2
⊢ (𝜑 → 𝐻:𝐴⟶ℝ) | 
| 8 | 3 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐹:𝐴⟶ℝ) | 
| 9 | 8 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ) | 
| 10 | 9 | rexrd 11312 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈
ℝ*) | 
| 11 | 1 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐺:𝐴⟶ℝ) | 
| 12 | 11 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) | 
| 13 | 12 | rexrd 11312 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈
ℝ*) | 
| 14 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ*) | 
| 15 |  | xrmaxle 13226 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ* ∧ (𝐺‘𝑧) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) | 
| 16 | 10, 13, 14, 15 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) | 
| 17 | 16 | notbid 318 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) | 
| 18 |  | ianor 983 | . . . . . . . . . 10
⊢ (¬
((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)) | 
| 19 | 17, 18 | bitrdi 287 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))) | 
| 20 |  | pnfxr 11316 | . . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* | 
| 21 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) | 
| 22 | 14, 20, 21 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) | 
| 23 |  | 3anan12 1095 | . . . . . . . . . . . 12
⊢
((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) | 
| 24 | 22, 23 | bitrdi 287 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))) | 
| 25 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 26 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) | 
| 27 | 25, 26 | breq12d 5155 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧))) | 
| 28 | 27, 26, 25 | ifbieq12d 4553 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) | 
| 29 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (𝐺‘𝑧) ∈ V | 
| 30 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑧) ∈ V | 
| 31 | 29, 30 | ifex 4575 | . . . . . . . . . . . . . 14
⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V | 
| 32 | 28, 6, 31 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) | 
| 33 | 32 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) | 
| 34 | 33 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞))) | 
| 35 | 12, 9 | ifcld 4571 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ) | 
| 36 |  | ltpnf 13163 | . . . . . . . . . . . . 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 311 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))) | 
| 40 | 35 | rexrd 11312 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈
ℝ*) | 
| 41 |  | xrltnle 11329 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) | 
| 42 | 14, 40, 41 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) | 
| 43 | 39, 42 | bitrd 279 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) | 
| 44 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞))) | 
| 45 | 14, 20, 44 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞))) | 
| 46 |  | 3anan12 1095 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))) | 
| 47 | 45, 46 | bitrdi 287 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))) | 
| 48 |  | ltpnf 13163 | . . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞) | 
| 49 | 9, 48 | jccir 521 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)) | 
| 50 | 49 | biantrud 531 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))) | 
| 51 |  | xrltnle 11329 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ*
∧ (𝐹‘𝑧) ∈ ℝ*)
→ (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) | 
| 52 | 14, 10, 51 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) | 
| 53 | 47, 50, 52 | 3bitr2d 307 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) | 
| 54 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞))) | 
| 55 | 14, 20, 54 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞))) | 
| 56 |  | 3anan12 1095 | . . . . . . . . . . . 12
⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))) | 
| 57 | 55, 56 | bitrdi 287 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))) | 
| 58 |  | ltpnf 13163 | . . . . . . . . . . . . 13
⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞) | 
| 59 | 12, 58 | jccir 521 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)) | 
| 60 | 59 | biantrud 531 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))) | 
| 61 |  | xrltnle 11329 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ*
∧ (𝐺‘𝑧) ∈ ℝ*)
→ (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) | 
| 62 | 14, 13, 61 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) | 
| 63 | 57, 60, 62 | 3bitr2d 307 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) | 
| 64 | 53, 63 | orbi12d 918 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))) | 
| 65 | 19, 43, 64 | 3bitr4d 311 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 66 | 65 | pm5.32da 579 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) | 
| 67 |  | andi 1009 | . . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 68 | 66, 67 | bitrdi 287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) | 
| 69 | 7 | ffnd 6736 | . . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝐴) | 
| 70 | 69 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐻 Fn 𝐴) | 
| 71 |  | elpreima 7077 | . . . . . . 7
⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 72 | 70, 71 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 73 | 8 | ffnd 6736 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐹 Fn 𝐴) | 
| 74 |  | elpreima 7077 | . . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 75 | 73, 74 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 76 | 11 | ffnd 6736 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐺 Fn 𝐴) | 
| 77 |  | elpreima 7077 | . . . . . . . 8
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 78 | 76, 77 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) | 
| 79 | 75, 78 | orbi12d 918 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) | 
| 80 | 68, 72, 79 | 3bitr4d 311 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞))))) | 
| 81 |  | elun 4152 | . . . . 5
⊢ (𝑧 ∈ ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)))) | 
| 82 | 80, 81 | bitr4di 289 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))))) | 
| 83 | 82 | eqrdv 2734 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (𝑦(,)+∞)) = ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞)))) | 
| 84 |  | mbfmax.2 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ MblFn) | 
| 85 |  | mbfima 25666 | . . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝑦(,)+∞)) ∈ dom
vol) | 
| 86 | 84, 3, 85 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (◡𝐹 “ (𝑦(,)+∞)) ∈ dom
vol) | 
| 87 |  | mbfmax.4 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ MblFn) | 
| 88 |  | mbfima 25666 | . . . . . 6
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (◡𝐺 “ (𝑦(,)+∞)) ∈ dom
vol) | 
| 89 | 87, 1, 88 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (◡𝐺 “ (𝑦(,)+∞)) ∈ dom
vol) | 
| 90 |  | unmbl 25573 | . . . . 5
⊢ (((◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) | 
| 91 | 86, 89, 90 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) | 
| 92 | 91 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) | 
| 93 | 83, 92 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (𝑦(,)+∞)) ∈ dom
vol) | 
| 94 |  | xrmaxlt 13224 | . . . . . . . . . 10
⊢ (((𝐹‘𝑧) ∈ ℝ* ∧ (𝐺‘𝑧) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) | 
| 95 | 10, 13, 14, 94 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) | 
| 96 |  | mnfxr 11319 | . . . . . . . . . . . 12
⊢ -∞
∈ ℝ* | 
| 97 |  | elioo2 13429 | . . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
(if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) | 
| 98 | 96, 14, 97 | sylancr 587 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) | 
| 99 |  | df-3an 1088 | . . . . . . . . . . 11
⊢
((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)) | 
| 100 | 98, 99 | bitrdi 287 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) | 
| 101 | 33 | eleq1d 2825 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦))) | 
| 102 |  | mnflt 13166 | . . . . . . . . . . . 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 311 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)) | 
| 106 |  | mnflt 13166 | . . . . . . . . . . . 12
⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧)) | 
| 107 | 9, 106 | jccir 521 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧))) | 
| 108 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦))) | 
| 109 | 96, 14, 108 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦))) | 
| 110 |  | df-3an 1088 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)) | 
| 111 | 109, 110 | bitrdi 287 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))) | 
| 112 | 107, 111 | mpbirand 707 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦)) | 
| 113 |  | mnflt 13166 | . . . . . . . . . . . 12
⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧)) | 
| 114 | 12, 113 | jccir 521 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧))) | 
| 115 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦))) | 
| 116 | 96, 14, 115 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦))) | 
| 117 |  | df-3an 1088 | . . . . . . . . . . . 12
⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)) | 
| 118 | 116, 117 | bitrdi 287 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))) | 
| 119 | 114, 118 | mpbirand 707 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦)) | 
| 120 | 112, 119 | anbi12d 632 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) | 
| 121 | 95, 105, 120 | 3bitr4d 311 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 122 | 121 | pm5.32da 579 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) | 
| 123 |  | anandi 676 | . . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 124 | 122, 123 | bitrdi 287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) | 
| 125 |  | elpreima 7077 | . . . . . . 7
⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 126 | 70, 125 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 127 |  | elpreima 7077 | . . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 128 | 73, 127 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 129 |  | elpreima 7077 | . . . . . . . 8
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 130 | 76, 129 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) | 
| 131 | 128, 130 | anbi12d 632 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) | 
| 132 | 124, 126,
131 | 3bitr4d 311 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦))))) | 
| 133 |  | elin 3966 | . . . . 5
⊢ (𝑧 ∈ ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)))) | 
| 134 | 132, 133 | bitr4di 289 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))))) | 
| 135 | 134 | eqrdv 2734 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (-∞(,)𝑦)) = ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦)))) | 
| 136 |  | mbfima 25666 | . . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) | 
| 137 | 84, 3, 136 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) | 
| 138 |  | mbfima 25666 | . . . . . 6
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) | 
| 139 | 87, 1, 138 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) | 
| 140 |  | inmbl 25578 | . . . . 5
⊢ (((◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) | 
| 141 | 137, 139,
140 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) | 
| 142 | 141 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) | 
| 143 | 135, 142 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol) | 
| 144 | 7, 93, 143 | ismbfd 25675 | 1
⊢ (𝜑 → 𝐻 ∈ MblFn) |