| Step | Hyp | Ref
| Expression |
| 1 | | ioof 13487 |
. . . . 5
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 2 | | ffn 6736 |
. . . . 5
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 3 | | ovelrn 7609 |
. . . . 5
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑥 ∈ ℝ*
∃𝑦 ∈
ℝ* 𝑧 =
(𝑥(,)𝑦))) |
| 4 | 1, 2, 3 | mp2b 10 |
. . . 4
⊢ (𝑧 ∈ ran (,) ↔
∃𝑥 ∈
ℝ* ∃𝑦 ∈ ℝ* 𝑧 = (𝑥(,)𝑦)) |
| 5 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑥 ∈
ℝ*) |
| 6 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ +∞ ∈ ℝ*) |
| 8 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ -∞ ∈ ℝ*) |
| 10 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑦 ∈
ℝ*) |
| 11 | | iooin 13421 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (-∞ ∈
ℝ* ∧ 𝑦
∈ ℝ*)) → ((𝑥(,)+∞) ∩ (-∞(,)𝑦)) = (if(𝑥 ≤ -∞, -∞, 𝑥)(,)if(+∞ ≤ 𝑦, +∞, 𝑦))) |
| 12 | 5, 7, 9, 10, 11 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((𝑥(,)+∞)
∩ (-∞(,)𝑦)) =
(if(𝑥 ≤ -∞,
-∞, 𝑥)(,)if(+∞
≤ 𝑦, +∞, 𝑦))) |
| 13 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → if(𝑥 ≤ -∞, -∞, 𝑥) ∈
ℝ*) |
| 14 | 8, 5, 13 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ∈
ℝ*) |
| 15 | | mnfle 13177 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ*
→ -∞ ≤ 𝑥) |
| 16 | | xrleid 13193 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ*
→ 𝑥 ≤ 𝑥) |
| 17 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (-∞
= if(𝑥 ≤ -∞,
-∞, 𝑥) →
(-∞ ≤ 𝑥 ↔
if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥)) |
| 18 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = if(𝑥 ≤ -∞, -∞, 𝑥) → (𝑥 ≤ 𝑥 ↔ if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥)) |
| 19 | 17, 18 | ifboth 4565 |
. . . . . . . . . . . . . 14
⊢
((-∞ ≤ 𝑥
∧ 𝑥 ≤ 𝑥) → if(𝑥 ≤ -∞, -∞, 𝑥) ≤ 𝑥) |
| 20 | 15, 16, 19 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ*
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥) |
| 21 | 20 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) ≤ 𝑥) |
| 22 | | xrmax1 13217 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ -∞ ∈ ℝ*) → 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)) |
| 23 | 5, 8, 22 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑥 ≤ if(𝑥 ≤ -∞, -∞, 𝑥)) |
| 24 | 14, 5, 21, 23 | xrletrid 13197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(𝑥 ≤ -∞,
-∞, 𝑥) = 𝑥) |
| 25 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢
((+∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
if(+∞ ≤ 𝑦,
+∞, 𝑦) ∈
ℝ*) |
| 26 | 6, 10, 25 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) ∈
ℝ*) |
| 27 | | xrmin2 13220 |
. . . . . . . . . . . . 13
⊢
((+∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) →
if(+∞ ≤ 𝑦,
+∞, 𝑦) ≤ 𝑦) |
| 28 | 6, 10, 27 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) ≤ 𝑦) |
| 29 | | pnfge 13172 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
| 30 | | xrleid 13193 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤ 𝑦) |
| 31 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (+∞
= if(+∞ ≤ 𝑦,
+∞, 𝑦) → (𝑦 ≤ +∞ ↔ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦))) |
| 32 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(+∞ ≤ 𝑦, +∞, 𝑦) → (𝑦 ≤ 𝑦 ↔ 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦))) |
| 33 | 31, 32 | ifboth 4565 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ≤ +∞ ∧ 𝑦 ≤ 𝑦) → 𝑦 ≤ if(+∞ ≤ 𝑦, +∞, 𝑦)) |
| 34 | 29, 30, 33 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤ if(+∞
≤ 𝑦, +∞, 𝑦)) |
| 35 | 34 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝑦 ≤ if(+∞
≤ 𝑦, +∞, 𝑦)) |
| 36 | 26, 10, 28, 35 | xrletrid 13197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ if(+∞ ≤ 𝑦,
+∞, 𝑦) = 𝑦) |
| 37 | 24, 36 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (if(𝑥 ≤ -∞,
-∞, 𝑥)(,)if(+∞
≤ 𝑦, +∞, 𝑦)) = (𝑥(,)𝑦)) |
| 38 | 12, 37 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((𝑥(,)+∞)
∩ (-∞(,)𝑦)) =
(𝑥(,)𝑦)) |
| 39 | 38 | imaeq2d 6078 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = (◡𝐹 “ (𝑥(,)𝑦))) |
| 40 | | ismbfd.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
| 41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ 𝐹:𝐴⟶ℝ) |
| 42 | 41 | ffund 6740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ Fun 𝐹) |
| 43 | | inpreima 7084 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
| 44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ ((𝑥(,)+∞) ∩ (-∞(,)𝑦))) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
| 45 | 39, 44 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)𝑦)) = ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦)))) |
| 46 | | ismbfd.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) |
| 47 | 46 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) |
| 48 | | ismbfd.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) |
| 49 | 48 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ℝ* (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) |
| 50 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (-∞(,)𝑥) = (-∞(,)𝑦)) |
| 51 | 50 | imaeq2d 6078 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (◡𝐹 “ (-∞(,)𝑥)) = (◡𝐹 “ (-∞(,)𝑦))) |
| 52 | 51 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol ↔ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol)) |
| 53 | 52 | rspccva 3621 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ* (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol ∧ 𝑦 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
| 54 | 49, 53 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
| 55 | 54 | adantrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) |
| 56 | | inmbl 25577 |
. . . . . . . 8
⊢ (((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑦)) ∈ dom vol) → ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦))) ∈ dom vol) |
| 57 | 47, 55, 56 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ ((◡𝐹 “ (𝑥(,)+∞)) ∩ (◡𝐹 “ (-∞(,)𝑦))) ∈ dom vol) |
| 58 | 45, 57 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (◡𝐹 “ (𝑥(,)𝑦)) ∈ dom vol) |
| 59 | | imaeq2 6074 |
. . . . . . 7
⊢ (𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) = (◡𝐹 “ (𝑥(,)𝑦))) |
| 60 | 59 | eleq1d 2826 |
. . . . . 6
⊢ (𝑧 = (𝑥(,)𝑦) → ((◡𝐹 “ 𝑧) ∈ dom vol ↔ (◡𝐹 “ (𝑥(,)𝑦)) ∈ dom vol)) |
| 61 | 58, 60 | syl5ibrcom 247 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
→ (𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
| 62 | 61 | rexlimdvva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ℝ* ∃𝑦 ∈ ℝ*
𝑧 = (𝑥(,)𝑦) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
| 63 | 4, 62 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ran (,) → (◡𝐹 “ 𝑧) ∈ dom vol)) |
| 64 | 63 | ralrimiv 3145 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol) |
| 65 | | ismbf 25663 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol)) |
| 66 | 40, 65 | syl 17 |
. 2
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑧 ∈ ran (,)(◡𝐹 “ 𝑧) ∈ dom vol)) |
| 67 | 64, 66 | mpbird 257 |
1
⊢ (𝜑 → 𝐹 ∈ MblFn) |