MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ismbf3d Structured version   Visualization version   GIF version

Theorem ismbf3d 24551
Description: Simplified form of ismbfd 24536. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypotheses
Ref Expression
ismbf3d.1 (𝜑𝐹:𝐴⟶ℝ)
ismbf3d.2 ((𝜑𝑥 ∈ ℝ) → (𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
Assertion
Ref Expression
ismbf3d (𝜑𝐹 ∈ MblFn)
Distinct variable groups:   𝑥,𝐹   𝜑,𝑥
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem ismbf3d
Dummy variables 𝑣 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ismbf3d.1 . 2 (𝜑𝐹:𝐴⟶ℝ)
2 fimacnv 6567 . . . 4 (𝐹:𝐴⟶ℝ → (𝐹 “ ℝ) = 𝐴)
31, 2syl 17 . . 3 (𝜑 → (𝐹 “ ℝ) = 𝐴)
4 imaiun 7058 . . . . 5 (𝐹 𝑦 ∈ ℕ (-𝑦(,)+∞)) = 𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞))
5 ioossre 12996 . . . . . . . . 9 (-𝑦(,)+∞) ⊆ ℝ
65rgenw 3073 . . . . . . . 8 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ
7 iunss 4954 . . . . . . . 8 ( 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ ↔ ∀𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ)
86, 7mpbir 234 . . . . . . 7 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ
9 renegcl 11141 . . . . . . . . . . 11 (𝑧 ∈ ℝ → -𝑧 ∈ ℝ)
10 arch 12087 . . . . . . . . . . 11 (-𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ -𝑧 < 𝑦)
119, 10syl 17 . . . . . . . . . 10 (𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ -𝑧 < 𝑦)
12 simpl 486 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑧 ∈ ℝ)
1312biantrurd 536 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑦 < 𝑧 ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
14 nnre 11837 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
15 ltnegcon1 11333 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧))
1614, 15sylan2 596 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧))
1714adantl 485 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
1817renegcld 11259 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈ ℝ)
1918rexrd 10883 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈ ℝ*)
20 elioopnf 13031 . . . . . . . . . . . . 13 (-𝑦 ∈ ℝ* → (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
2119, 20syl 17 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
2213, 16, 213bitr4d 314 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦𝑧 ∈ (-𝑦(,)+∞)))
2322rexbidva 3215 . . . . . . . . . 10 (𝑧 ∈ ℝ → (∃𝑦 ∈ ℕ -𝑧 < 𝑦 ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞)))
2411, 23mpbid 235 . . . . . . . . 9 (𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞))
25 eliun 4908 . . . . . . . . 9 (𝑧 𝑦 ∈ ℕ (-𝑦(,)+∞) ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞))
2624, 25sylibr 237 . . . . . . . 8 (𝑧 ∈ ℝ → 𝑧 𝑦 ∈ ℕ (-𝑦(,)+∞))
2726ssriv 3905 . . . . . . 7 ℝ ⊆ 𝑦 ∈ ℕ (-𝑦(,)+∞)
288, 27eqssi 3917 . . . . . 6 𝑦 ∈ ℕ (-𝑦(,)+∞) = ℝ
2928imaeq2i 5927 . . . . 5 (𝐹 𝑦 ∈ ℕ (-𝑦(,)+∞)) = (𝐹 “ ℝ)
304, 29eqtr3i 2767 . . . 4 𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞)) = (𝐹 “ ℝ)
31 ismbf3d.2 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
3231ralrimiva 3105 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ℝ (𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
3314renegcld 11259 . . . . . . 7 (𝑦 ∈ ℕ → -𝑦 ∈ ℝ)
34 oveq1 7220 . . . . . . . . . 10 (𝑥 = -𝑦 → (𝑥(,)+∞) = (-𝑦(,)+∞))
3534imaeq2d 5929 . . . . . . . . 9 (𝑥 = -𝑦 → (𝐹 “ (𝑥(,)+∞)) = (𝐹 “ (-𝑦(,)+∞)))
3635eleq1d 2822 . . . . . . . 8 (𝑥 = -𝑦 → ((𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol))
3736rspccva 3536 . . . . . . 7 ((∀𝑥 ∈ ℝ (𝐹 “ (𝑥(,)+∞)) ∈ dom vol ∧ -𝑦 ∈ ℝ) → (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
3832, 33, 37syl2an 599 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
3938ralrimiva 3105 . . . . 5 (𝜑 → ∀𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
40 iunmbl 24450 . . . . 5 (∀𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol → 𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
4139, 40syl 17 . . . 4 (𝜑 𝑦 ∈ ℕ (𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
4230, 41eqeltrrid 2843 . . 3 (𝜑 → (𝐹 “ ℝ) ∈ dom vol)
433, 42eqeltrrd 2839 . 2 (𝜑𝐴 ∈ dom vol)
44 imaiun 7058 . . . . . . 7 (𝐹 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦)))) = 𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦))))
45 eliun 4908 . . . . . . . . . 10 (𝑥 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) ↔ ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
46 3simpb 1151 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))))
47 simplr 769 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑧 ∈ ℝ)
48 nnrp 12597 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
4948ad2antrl 728 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑦 ∈ ℝ+)
5049rpreccld 12638 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (1 / 𝑦) ∈ ℝ+)
5147, 50ltsubrpd 12660 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) < 𝑧)
52 simprr 773 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ)
53 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ) → 𝑧 ∈ ℝ)
54 nnrecre 11872 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ → (1 / 𝑦) ∈ ℝ)
55 resubcl 11142 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ℝ ∧ (1 / 𝑦) ∈ ℝ) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
5653, 54, 55syl2an 599 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
5756adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
58 lelttr 10923 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧))
5952, 57, 47, 58syl3anc 1373 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧))
6051, 59mpan2d 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧))
6160anassrs 471 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧))
6261imdistanda 575 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
6346, 62syl5 34 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
64 mnfxr 10890 . . . . . . . . . . . . . . . 16 -∞ ∈ ℝ*
65 elioc2 12998 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 ≤ (𝑧 − (1 / 𝑦)))))
6664, 56, 65sylancr 590 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 ≤ (𝑧 − (1 / 𝑦)))))
67 rexr 10879 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ → 𝑧 ∈ ℝ*)
6867adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ ℝ) → 𝑧 ∈ ℝ*)
69 elioomnf 13032 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
7068, 69syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ ℝ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
7170adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
7263, 66, 713imtr4d 297 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧)))
7372rexlimdva 3203 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧)))
7473, 70sylibd 242 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
75 simprl 771 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 ∈ ℝ)
7675adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → 𝑥 ∈ ℝ)
7776mnfltd 12716 . . . . . . . . . . . . . . 15 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → -∞ < 𝑥)
7856ad2ant2r 747 . . . . . . . . . . . . . . . 16 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
7954ad2antrl 728 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → (1 / 𝑦) ∈ ℝ)
80 simplr 769 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑧 ∈ ℝ)
8180adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → 𝑧 ∈ ℝ)
82 simprr 773 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → (1 / 𝑦) < (𝑧𝑥))
8379, 81, 76, 82ltsub13d 11438 . . . . . . . . . . . . . . . 16 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → 𝑥 < (𝑧 − (1 / 𝑦)))
8476, 78, 83ltled 10980 . . . . . . . . . . . . . . 15 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → 𝑥 ≤ (𝑧 − (1 / 𝑦)))
8566ad2ant2r 747 . . . . . . . . . . . . . . 15 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 ≤ (𝑧 − (1 / 𝑦)))))
8676, 77, 84, 85mpbir3and 1344 . . . . . . . . . . . . . 14 ((((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧𝑥))) → 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
8780, 75resubcld 11260 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑧𝑥) ∈ ℝ)
88 simprr 773 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 < 𝑧)
8975, 80posdifd 11419 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑥 < 𝑧 ↔ 0 < (𝑧𝑥)))
9088, 89mpbid 235 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 0 < (𝑧𝑥))
91 nnrecl 12088 . . . . . . . . . . . . . . 15 (((𝑧𝑥) ∈ ℝ ∧ 0 < (𝑧𝑥)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧𝑥))
9287, 90, 91syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧𝑥))
9386, 92reximddv 3194 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
9493ex 416 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝑧) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦)))))
9574, 94impbid 215 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
9695, 70bitr4d 285 . . . . . . . . . 10 ((𝜑𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧)))
9745, 96syl5bb 286 . . . . . . . . 9 ((𝜑𝑧 ∈ ℝ) → (𝑥 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧)))
9897eqrdv 2735 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) = (-∞(,)𝑧))
9998imaeq2d 5929 . . . . . . 7 ((𝜑𝑧 ∈ ℝ) → (𝐹 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦)))) = (𝐹 “ (-∞(,)𝑧)))
10044, 99eqtr3id 2792 . . . . . 6 ((𝜑𝑧 ∈ ℝ) → 𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) = (𝐹 “ (-∞(,)𝑧)))
1011ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐹:𝐴⟶ℝ)
102 ffun 6548 . . . . . . . . . . 11 (𝐹:𝐴⟶ℝ → Fun 𝐹)
103 funcnvcnv 6447 . . . . . . . . . . 11 (Fun 𝐹 → Fun 𝐹)
104 imadif 6464 . . . . . . . . . . 11 (Fun 𝐹 → (𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((𝐹 “ ℝ) ∖ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))))
105101, 102, 103, 1044syl 19 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((𝐹 “ ℝ) ∖ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))))
10664a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ ∈ ℝ*)
10756rexrd 10883 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈ ℝ*)
108 pnfxr 10887 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
109108a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → +∞ ∈ ℝ*)
11056mnfltd 12716 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ < (𝑧 − (1 / 𝑦)))
11156ltpnfd 12713 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) < +∞)
112 df-ioc 12940 . . . . . . . . . . . . . . 15 (,] = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤𝑤𝑣)})
113 df-ioo 12939 . . . . . . . . . . . . . . 15 (,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤𝑤 < 𝑣)})
114 xrltnle 10900 . . . . . . . . . . . . . . 15 (((𝑧 − (1 / 𝑦)) ∈ ℝ*𝑥 ∈ ℝ*) → ((𝑧 − (1 / 𝑦)) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑧 − (1 / 𝑦))))
115 xrlelttr 12746 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞) → 𝑥 < +∞))
116 xrlttr 12730 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ*𝑥 ∈ ℝ*) → ((-∞ < (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑥) → -∞ < 𝑥))
117112, 113, 114, 113, 115, 116ixxun 12951 . . . . . . . . . . . . . 14 (((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞)) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,)+∞))
118106, 107, 109, 110, 111, 117syl32anc 1380 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,)+∞))
119 uncom 4067 . . . . . . . . . . . . 13 ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦))))
120 ioomax 13010 . . . . . . . . . . . . 13 (-∞(,)+∞) = ℝ
121118, 119, 1203eqtr3g 2801 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ)
122 ioossre 12996 . . . . . . . . . . . . 13 ((𝑧 − (1 / 𝑦))(,)+∞) ⊆ ℝ
123 incom 4115 . . . . . . . . . . . . . 14 (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞))
124112, 113, 114ixxdisj 12950 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
12564, 108, 124mp3an13 1454 . . . . . . . . . . . . . . 15 ((𝑧 − (1 / 𝑦)) ∈ ℝ* → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
126107, 125syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
127123, 126syl5eq 2790 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅)
128 uneqdifeq 4404 . . . . . . . . . . . . 13 ((((𝑧 − (1 / 𝑦))(,)+∞) ⊆ ℝ ∧ (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦)))))
129122, 127, 128sylancr 590 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦)))))
130121, 129mpbid 235 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦))))
131130imaeq2d 5929 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))))
132105, 131eqtr3d 2779 . . . . . . . . 9 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝐹 “ ℝ) ∖ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) = (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))))
13342ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝐹 “ ℝ) ∈ dom vol)
134 oveq1 7220 . . . . . . . . . . . . 13 (𝑥 = (𝑧 − (1 / 𝑦)) → (𝑥(,)+∞) = ((𝑧 − (1 / 𝑦))(,)+∞))
135134imaeq2d 5929 . . . . . . . . . . . 12 (𝑥 = (𝑧 − (1 / 𝑦)) → (𝐹 “ (𝑥(,)+∞)) = (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)))
136135eleq1d 2822 . . . . . . . . . . 11 (𝑥 = (𝑧 − (1 / 𝑦)) → ((𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol))
13732ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∀𝑥 ∈ ℝ (𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
138136, 137, 56rspcdva 3539 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol)
139 difmbl 24440 . . . . . . . . . 10 (((𝐹 “ ℝ) ∈ dom vol ∧ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol) → ((𝐹 “ ℝ) ∖ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom vol)
140133, 138, 139syl2anc 587 . . . . . . . . 9 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝐹 “ ℝ) ∖ (𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom vol)
141132, 140eqeltrrd 2839 . . . . . . . 8 (((𝜑𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
142141ralrimiva 3105 . . . . . . 7 ((𝜑𝑧 ∈ ℝ) → ∀𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
143 iunmbl 24450 . . . . . . 7 (∀𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol → 𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
144142, 143syl 17 . . . . . 6 ((𝜑𝑧 ∈ ℝ) → 𝑦 ∈ ℕ (𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
145100, 144eqeltrrd 2839 . . . . 5 ((𝜑𝑧 ∈ ℝ) → (𝐹 “ (-∞(,)𝑧)) ∈ dom vol)
146145ralrimiva 3105 . . . 4 (𝜑 → ∀𝑧 ∈ ℝ (𝐹 “ (-∞(,)𝑧)) ∈ dom vol)
147 oveq2 7221 . . . . . . 7 (𝑧 = 𝑥 → (-∞(,)𝑧) = (-∞(,)𝑥))
148147imaeq2d 5929 . . . . . 6 (𝑧 = 𝑥 → (𝐹 “ (-∞(,)𝑧)) = (𝐹 “ (-∞(,)𝑥)))
149148eleq1d 2822 . . . . 5 (𝑧 = 𝑥 → ((𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ (𝐹 “ (-∞(,)𝑥)) ∈ dom vol))
150149cbvralvw 3358 . . . 4 (∀𝑧 ∈ ℝ (𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ ∀𝑥 ∈ ℝ (𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
151146, 150sylib 221 . . 3 (𝜑 → ∀𝑥 ∈ ℝ (𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
152151r19.21bi 3130 . 2 ((𝜑𝑥 ∈ ℝ) → (𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
1531, 43, 31, 152ismbf2d 24537 1 (𝜑𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wral 3061  wrex 3062  cdif 3863  cun 3864  cin 3865  wss 3866  c0 4237   ciun 4904   class class class wbr 5053  ccnv 5550  dom cdm 5551  cima 5554  Fun wfun 6374  wf 6376  (class class class)co 7213  cr 10728  0cc0 10729  1c1 10730  +∞cpnf 10864  -∞cmnf 10865  *cxr 10866   < clt 10867  cle 10868  cmin 11062  -cneg 11063   / cdiv 11489  cn 11830  +crp 12586  (,)cioo 12935  (,]cioc 12936  volcvol 24360  MblFncmbf 24511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cc 10049  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-disj 5019  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-pm 8511  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-xadd 12705  df-ioo 12939  df-ioc 12940  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-rlim 15050  df-sum 15250  df-xmet 20356  df-met 20357  df-ovol 24361  df-vol 24362  df-mbf 24516
This theorem is referenced by:  mbfaddlem  24557  mbfsup  24561
  Copyright terms: Public domain W3C validator