Step | Hyp | Ref
| Expression |
1 | | mbfmax.3 |
. . . . 5
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
2 | 1 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ) |
3 | | mbfmax.1 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
4 | 3 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
5 | 2, 4 | ifcld 4131 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) ∈ ℝ) |
6 | | mbfmax.5 |
. . 3
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥))) |
7 | 5, 6 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝐻:𝐴⟶ℝ) |
8 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐹:𝐴⟶ℝ) |
9 | 8 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ) |
10 | 9 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈
ℝ*) |
11 | 1 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐺:𝐴⟶ℝ) |
12 | 11 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) |
13 | 12 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈
ℝ*) |
14 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
15 | | xrmaxle 12014 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ* ∧ (𝐺‘𝑧) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) |
16 | 10, 13, 14, 15 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) |
17 | 16 | notbid 308 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦))) |
18 | | ianor 509 |
. . . . . . . . . 10
⊢ (¬
((𝐹‘𝑧) ≤ 𝑦 ∧ (𝐺‘𝑧) ≤ 𝑦) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦)) |
19 | 17, 18 | syl6bb 276 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦 ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))) |
20 | | pnfxr 10092 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
21 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) |
22 | 14, 20, 21 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) |
23 | | 3anan12 1051 |
. . . . . . . . . . . 12
⊢
((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞))) |
24 | 22, 23 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))) |
25 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
26 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
27 | 25, 26 | breq12d 4666 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≤ (𝐺‘𝑥) ↔ (𝐹‘𝑧) ≤ (𝐺‘𝑧))) |
28 | 27, 26, 25 | ifbieq12d 4113 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) |
29 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘𝑧) ∈ V |
30 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑧) ∈ V |
31 | 29, 30 | ifex 4156 |
. . . . . . . . . . . . . 14
⊢ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ V |
32 | 28, 6, 31 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) |
33 | 32 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) |
34 | 33 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (𝑦(,)+∞))) |
35 | 12, 9 | ifcld 4131 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ) |
36 | | ltpnf 11954 |
. . . . . . . . . . . . 13
⊢
(if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞) |
37 | 35, 36 | jccir 562 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)) |
38 | 37 | biantrud 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < +∞)))) |
39 | 24, 34, 38 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))) |
40 | 35 | rexrd 10089 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈
ℝ*) |
41 | | xrltnle 10105 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ*) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) |
42 | 14, 40, 41 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) |
43 | 39, 42 | bitrd 268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ≤ 𝑦)) |
44 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞))) |
45 | 14, 20, 44 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞))) |
46 | | 3anan12 1051 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < +∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞))) |
47 | 45, 46 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))) |
48 | | ltpnf 11954 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) < +∞) |
49 | 9, 48 | jccir 562 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)) |
50 | 49 | biantrud 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ (𝑦 < (𝐹‘𝑧) ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < +∞)))) |
51 | | xrltnle 10105 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ*
∧ (𝐹‘𝑧) ∈ ℝ*)
→ (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) |
52 | 14, 10, 51 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐹‘𝑧) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) |
53 | 47, 50, 52 | 3bitr2d 296 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹‘𝑧) ≤ 𝑦)) |
54 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞))) |
55 | 14, 20, 54 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞))) |
56 | | 3anan12 1051 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑧) ∈ ℝ ∧ 𝑦 < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < +∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞))) |
57 | 55, 56 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))) |
58 | | ltpnf 11954 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑧) ∈ ℝ → (𝐺‘𝑧) < +∞) |
59 | 12, 58 | jccir 562 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)) |
60 | 59 | biantrud 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ (𝑦 < (𝐺‘𝑧) ∧ ((𝐺‘𝑧) ∈ ℝ ∧ (𝐺‘𝑧) < +∞)))) |
61 | | xrltnle 10105 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ*
∧ (𝐺‘𝑧) ∈ ℝ*)
→ (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) |
62 | 14, 13, 61 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (𝑦 < (𝐺‘𝑧) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) |
63 | 57, 60, 62 | 3bitr2d 296 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺‘𝑧) ≤ 𝑦)) |
64 | 53, 63 | orbi12d 746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹‘𝑧) ≤ 𝑦 ∨ ¬ (𝐺‘𝑧) ≤ 𝑦))) |
65 | 19, 43, 64 | 3bitr4d 300 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) |
66 | 65 | pm5.32da 673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) |
67 | | andi 911 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺‘𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) |
68 | 66, 67 | syl6bb 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) |
69 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐻:𝐴⟶ℝ → 𝐻 Fn 𝐴) |
70 | 7, 69 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝐴) |
71 | 70 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐻 Fn 𝐴) |
72 | | elpreima 6337 |
. . . . . . 7
⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)))) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (𝑦(,)+∞)))) |
74 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
75 | 8, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐹 Fn 𝐴) |
76 | | elpreima 6337 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)))) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)))) |
78 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐺:𝐴⟶ℝ → 𝐺 Fn 𝐴) |
79 | 11, 78 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐺 Fn 𝐴) |
80 | | elpreima 6337 |
. . . . . . . 8
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) |
81 | 79, 80 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞)))) |
82 | 77, 81 | orbi12d 746 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑦(,)+∞))))) |
83 | 68, 73, 82 | 3bitr4d 300 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞))))) |
84 | | elun 3753 |
. . . . 5
⊢ (𝑧 ∈ ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (◡𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (◡𝐺 “ (𝑦(,)+∞)))) |
85 | 83, 84 | syl6bbr 278 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))))) |
86 | 85 | eqrdv 2620 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (𝑦(,)+∞)) = ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞)))) |
87 | | mbfmax.2 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ MblFn) |
88 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝑦(,)+∞)) ∈ dom
vol) |
89 | 87, 3, 88 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (𝑦(,)+∞)) ∈ dom
vol) |
90 | | mbfmax.4 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ MblFn) |
91 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (◡𝐺 “ (𝑦(,)+∞)) ∈ dom
vol) |
92 | 90, 1, 91 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐺 “ (𝑦(,)+∞)) ∈ dom
vol) |
93 | | unmbl 23305 |
. . . . 5
⊢ (((◡𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (◡𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) |
94 | 89, 92, 93 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) |
95 | 94 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((◡𝐹 “ (𝑦(,)+∞)) ∪ (◡𝐺 “ (𝑦(,)+∞))) ∈ dom
vol) |
96 | 86, 95 | eqeltrd 2701 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (𝑦(,)+∞)) ∈ dom
vol) |
97 | | xrmaxlt 12012 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑧) ∈ ℝ* ∧ (𝐺‘𝑧) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) |
98 | 10, 13, 14, 97 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) |
99 | | mnfxr 10096 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
100 | | elioo2 12216 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
(if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) |
101 | 99, 14, 100 | sylancr 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) |
102 | | df-3an 1039 |
. . . . . . . . . . 11
⊢
((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)) |
103 | 101, 102 | syl6bb 276 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) |
104 | 33 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ (-∞(,)𝑦))) |
105 | | mnflt 11957 |
. . . . . . . . . . . 12
⊢
(if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ → -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) |
106 | 35, 105 | jccir 562 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)))) |
107 | 106 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦 ↔ ((if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) ∈ ℝ ∧ -∞ <
if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧))) ∧ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦))) |
108 | 103, 104,
107 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹‘𝑧) ≤ (𝐺‘𝑧), (𝐺‘𝑧), (𝐹‘𝑧)) < 𝑦)) |
109 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦))) |
110 | 99, 14, 109 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦))) |
111 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦)) |
112 | 110, 111 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))) |
113 | | mnflt 11957 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ℝ → -∞ < (𝐹‘𝑧)) |
114 | 9, 113 | jccir 562 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧))) |
115 | 114 | biantrurd 529 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) < 𝑦 ↔ (((𝐹‘𝑧) ∈ ℝ ∧ -∞ < (𝐹‘𝑧)) ∧ (𝐹‘𝑧) < 𝑦))) |
116 | 112, 115 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) < 𝑦)) |
117 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦))) |
118 | 99, 14, 117 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦))) |
119 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧) ∧ (𝐺‘𝑧) < 𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦)) |
120 | 118, 119 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))) |
121 | | mnflt 11957 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑧) ∈ ℝ → -∞ < (𝐺‘𝑧)) |
122 | 12, 121 | jccir 562 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧))) |
123 | 122 | biantrurd 529 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) < 𝑦 ↔ (((𝐺‘𝑧) ∈ ℝ ∧ -∞ < (𝐺‘𝑧)) ∧ (𝐺‘𝑧) < 𝑦))) |
124 | 120, 123 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺‘𝑧) < 𝑦)) |
125 | 116, 124 | anbi12d 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹‘𝑧) < 𝑦 ∧ (𝐺‘𝑧) < 𝑦))) |
126 | 98, 108, 125 | 3bitr4d 300 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) |
127 | 126 | pm5.32da 673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) |
128 | | anandi 871 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ ((𝐹‘𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) |
129 | 127, 128 | syl6bb 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) |
130 | | elpreima 6337 |
. . . . . . 7
⊢ (𝐻 Fn 𝐴 → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)))) |
131 | 71, 130 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐻‘𝑧) ∈ (-∞(,)𝑦)))) |
132 | | elpreima 6337 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)))) |
133 | 75, 132 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)))) |
134 | | elpreima 6337 |
. . . . . . . 8
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) |
135 | 79, 134 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦)))) |
136 | 133, 135 | anbi12d 747 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (-∞(,)𝑦))))) |
137 | 129, 131,
136 | 3bitr4d 300 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦))))) |
138 | | elin 3796 |
. . . . 5
⊢ (𝑧 ∈ ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (◡𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (◡𝐺 “ (-∞(,)𝑦)))) |
139 | 137, 138 | syl6bbr 278 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (◡𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))))) |
140 | 139 | eqrdv 2620 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (-∞(,)𝑦)) = ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦)))) |
141 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
142 | 87, 3, 141 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
143 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) |
144 | 90, 1, 143 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) |
145 | | inmbl 23310 |
. . . . 5
⊢ (((◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (◡𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) |
146 | 142, 144,
145 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) |
147 | 146 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → ((◡𝐹 “ (-∞(,)𝑦)) ∩ (◡𝐺 “ (-∞(,)𝑦))) ∈ dom vol) |
148 | 140, 147 | eqeltrd 2701 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐻 “ (-∞(,)𝑦)) ∈ dom vol) |
149 | 7, 96, 148 | ismbfd 23407 |
1
⊢ (𝜑 → 𝐻 ∈ MblFn) |