Step | Hyp | Ref
| Expression |
1 | | ioof 12588 |
. . . . 5
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | | ffn 6293 |
. . . . 5
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
3 | | ovelrn 7089 |
. . . . 5
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑥 ∈ ℝ*
∃𝑦 ∈
ℝ* 𝑧 =
(𝑥(,)𝑦))) |
4 | 1, 2, 3 | mp2b 10 |
. . . 4
⊢ (𝑧 ∈ ran (,) ↔
∃𝑥 ∈
ℝ* ∃𝑦 ∈ ℝ* 𝑧 = (𝑥(,)𝑦)) |
5 | | simprl 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑥 ∈
ℝ*) |
6 | | pnfxr 10432 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ +∞ ∈ ℝ*) |
8 | | mnfxr 10436 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ -∞ ∈ ℝ*) |
10 | | simprr 763 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑦 ∈
ℝ*) |
11 | | iooin 12525 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (-∞ ∈
ℝ* ∧ 𝑦
∈ ℝ*)) → ((𝑥(,)+∞) ∩ (-∞(,)𝑦)) = (if(𝑥 ≤ -∞, -∞, 𝑥)(,)if(+∞ ≤ 𝑦, +∞, 𝑦))) |
12 | 5, 7, 9, 10, 11 | syl22anc 829 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((𝑥(,)+∞)
∩ (-∞(,)𝑦)) =
(if(𝑥 ≤ -∞,
-∞, 𝑥)(,)if(+∞
≤ 𝑦, +∞, 𝑦))) |
13 | | mnfle 12283 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ*
→ -∞ ≤ 𝑥) |
14 | | xrleid 12298 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ*
→ 𝑥 ≤ 𝑥) |
15 | | breq1 4891 |
. . . . . . . . . . . . . . 15
⊢ (-∞
= if(𝑥 ≤ -∞,
-∞, 𝑥) →
(-∞ ≤ 𝑥 ↔
if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥)) |
16 | | breq1 4891 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = if(𝑥 ≤ -∞, -∞, 𝑥) → (𝑥 ≤ 𝑥 ↔ if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥)) |
17 | 15, 16 | ifboth 4345 |
. . . . . . . . . . . . . 14
⊢
((-∞ ≤ 𝑥
∧ 𝑥 ≤ 𝑥) → if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥) |
18 | 13, 14, 17 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ*
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥) |
19 | 18 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥) |
20 | | xrmax1 12322 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ -∞ ∈ ℝ*) → 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)) |
21 | 5, 8, 20 | sylancl 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)) |
22 | | ifcl 4351 |
. . . . . . . . . . . . . 14
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → if(𝑥 ≤ -∞, -∞, 𝑥) ∈
ℝ*) |
23 | 8, 5, 22 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ∈
ℝ*) |
24 | | xrletri3 12301 |
. . . . . . . . . . . . 13
⊢
((if(𝑥 ≤
-∞, -∞, 𝑥)
∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (if(𝑥 ≤ -∞, -∞, 𝑥) = 𝑥 ↔ (if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥 ∧ 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)))) |
25 | 23, 5, 24 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (if(𝑥 ≤ -∞,
-∞, 𝑥) = 𝑥 ↔ (if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥 ∧ 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)))) |
26 | 19, 21, 25 | mpbir2and 703 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) = 𝑥) |
27 | | xrmin2 12325 |
. . . . . . . . . . . . 13
⊢
((+∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
if(+∞ ≤ 𝑦,
+∞, 𝑦) ≤ 𝑦) |
28 | 6, 10, 27 | sylancr 581 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) ≤ 𝑦) |
29 | | pnfge 12279 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
30 | | xrleid 12298 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤ 𝑦) |
31 | | breq2 4892 |
. . . . . . . . . . . . . . 15
⊢ (+∞
= if(+∞ ≤ 𝑦,
+∞, 𝑦) → (𝑦 ≤ +∞ ↔ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦))) |
32 | | breq2 4892 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(+∞ ≤ 𝑦, +∞, 𝑦) → (𝑦 ≤ 𝑦 ↔ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦))) |
33 | 31, 32 | ifboth 4345 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ≤ +∞ ∧ 𝑦 ≤ 𝑦) → 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦)) |
34 | 29, 30, 33 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤ if(+∞
≤ 𝑦, +∞, 𝑦)) |
35 | 34 | ad2antll 719 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑦 ≤ if(+∞
≤ 𝑦, +∞, 𝑦)) |
36 | | ifcl 4351 |
. . . . . . . . . . . . . 14
⊢
((+∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
if(+∞ ≤ 𝑦,
+∞, 𝑦) ∈
ℝ*) |
37 | 6, 10, 36 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) ∈
ℝ*) |
38 | | xrletri3 12301 |
. . . . . . . . . . . . 13
⊢
((if(+∞ ≤ 𝑦, +∞, 𝑦) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (if(+∞ ≤ 𝑦,
+∞, 𝑦) = 𝑦 ↔ (if(+∞ ≤ 𝑦, +∞, 𝑦) ≤ 𝑦 ∧ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦)))) |
39 | 37, 10, 38 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (if(+∞ ≤ 𝑦,
+∞, 𝑦) = 𝑦 ↔ (if(+∞ ≤ 𝑦, +∞, 𝑦) ≤ 𝑦 ∧ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦)))) |
40 | 28, 35, 39 | mpbir2and 703 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) = 𝑦) |
41 | 26, 40 | oveq12d 6942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (if(𝑥 ≤ -∞,
-∞, 𝑥)(,)if(+∞
≤ 𝑦, +∞, 𝑦)) = (𝑥(,)𝑦)) |
42 | 12, 41 | eqtrd 2814 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((𝑥(,)+∞)
∩ (-∞(,)𝑦)) =
(𝑥(,)𝑦)) |
43 | 42 | imaeq2d 5722 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = (◡𝐹 “ (𝑥(,)𝑦))) |
44 | | ismbfd.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
45 | 44 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝐹:𝐴⟶ℝ) |
46 | 45 | ffund 6297 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ Fun 𝐹) |
47 | | inpreima 6608 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
49 | 43, 48 | eqtr3d 2816 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)𝑦)) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
50 | | ismbfd.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) |
51 | 50 | adantrr 707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) |
52 | | ismbfd.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) |
53 | 52 | ralrimiva 3148 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ℝ* (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) |
54 | | oveq2 6932 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (-∞(,)𝑥) = (-∞(,)𝑦)) |
55 | 54 | imaeq2d 5722 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (◡𝐹 “ (-∞(,)𝑥)) = (◡𝐹 “ (-∞(,)𝑦))) |
56 | 55 | eleq1d 2844 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol ↔ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)) |
57 | 56 | rspccva 3510 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ* (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol ∧ 𝑦 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
58 | 53, 57 | sylan 575 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
59 | 58 | adantrl 706 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
60 | | inmbl 23750 |
. . . . . . . 8
⊢ (((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) → ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦))) ∈ dom vol) |
61 | 51, 59, 60 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦))) ∈ dom vol) |
62 | 49, 61 | eqeltrd 2859 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)𝑦)) ∈ dom vol) |
63 | | imaeq2 5718 |
. . . . . . 7
⊢ (𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) = (◡𝐹 “ (𝑥(,)𝑦))) |
64 | 63 | eleq1d 2844 |
. . . . . 6
⊢ (𝑧 = (𝑥(,)𝑦) → ((◡𝐹 “ 𝑧) ∈ dom vol ↔ (◡𝐹 “ (𝑥(,)𝑦)) ∈ dom vol)) |
65 | 62, 64 | syl5ibrcom 239 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
66 | 65 | rexlimdvva 3221 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ℝ* ∃𝑦 ∈ ℝ*
𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
67 | 4, 66 | syl5bi 234 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ran (,) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
68 | 67 | ralrimiv 3147 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol) |
69 | | ismbf 23836 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol)) |
70 | 44, 69 | syl 17 |
. 2
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol)) |
71 | 68, 70 | mpbird 249 |
1
⊢ (𝜑 → 𝐹 ∈ MblFn) |