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

Theorem mbfmax 23410
Description: The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypotheses
Ref Expression
mbfmax.1 (𝜑𝐹:𝐴⟶ℝ)
mbfmax.2 (𝜑𝐹 ∈ MblFn)
mbfmax.3 (𝜑𝐺:𝐴⟶ℝ)
mbfmax.4 (𝜑𝐺 ∈ MblFn)
mbfmax.5 𝐻 = (𝑥𝐴 ↦ if((𝐹𝑥) ≤ (𝐺𝑥), (𝐺𝑥), (𝐹𝑥)))
Assertion
Ref Expression
mbfmax (𝜑𝐻 ∈ MblFn)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥
Allowed substitution hint:   𝐻(𝑥)

Proof of Theorem mbfmax
Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfmax.3 . . . . 5 (𝜑𝐺:𝐴⟶ℝ)
21ffvelrnda 6357 . . . 4 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ ℝ)
3 mbfmax.1 . . . . 5 (𝜑𝐹:𝐴⟶ℝ)
43ffvelrnda 6357 . . . 4 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℝ)
52, 4ifcld 4129 . . 3 ((𝜑𝑥𝐴) → if((𝐹𝑥) ≤ (𝐺𝑥), (𝐺𝑥), (𝐹𝑥)) ∈ ℝ)
6 mbfmax.5 . . 3 𝐻 = (𝑥𝐴 ↦ if((𝐹𝑥) ≤ (𝐺𝑥), (𝐺𝑥), (𝐹𝑥)))
75, 6fmptd 6383 . 2 (𝜑𝐻:𝐴⟶ℝ)
83adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ*) → 𝐹:𝐴⟶ℝ)
98ffvelrnda 6357 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℝ)
109rexrd 10086 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℝ*)
111adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ*) → 𝐺:𝐴⟶ℝ)
1211ffvelrnda 6357 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝐺𝑧) ∈ ℝ)
1312rexrd 10086 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝐺𝑧) ∈ ℝ*)
14 simplr 792 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → 𝑦 ∈ ℝ*)
15 xrmaxle 12011 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ ℝ* ∧ (𝐺𝑧) ∈ ℝ*𝑦 ∈ ℝ*) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦 ↔ ((𝐹𝑧) ≤ 𝑦 ∧ (𝐺𝑧) ≤ 𝑦)))
1610, 13, 14, 15syl3anc 1325 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦 ↔ ((𝐹𝑧) ≤ 𝑦 ∧ (𝐺𝑧) ≤ 𝑦)))
1716notbid 308 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (¬ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦 ↔ ¬ ((𝐹𝑧) ≤ 𝑦 ∧ (𝐺𝑧) ≤ 𝑦)))
18 ianor 509 . . . . . . . . . 10 (¬ ((𝐹𝑧) ≤ 𝑦 ∧ (𝐺𝑧) ≤ 𝑦) ↔ (¬ (𝐹𝑧) ≤ 𝑦 ∨ ¬ (𝐺𝑧) ≤ 𝑦))
1917, 18syl6bb 276 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (¬ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦 ↔ (¬ (𝐹𝑧) ≤ 𝑦 ∨ ¬ (𝐺𝑧) ≤ 𝑦)))
20 pnfxr 10089 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
21 elioo2 12213 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞)))
2214, 20, 21sylancl 694 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (𝑦(,)+∞) ↔ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞)))
23 3anan12 1050 . . . . . . . . . . . 12 ((if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ 𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞) ↔ (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞)))
2422, 23syl6bb 276 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (𝑦(,)+∞) ↔ (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞))))
25 fveq2 6189 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
26 fveq2 6189 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
2725, 26breq12d 4664 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝐹𝑥) ≤ (𝐺𝑥) ↔ (𝐹𝑧) ≤ (𝐺𝑧)))
2827, 26, 25ifbieq12d 4111 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → if((𝐹𝑥) ≤ (𝐺𝑥), (𝐺𝑥), (𝐹𝑥)) = if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)))
29 fvex 6199 . . . . . . . . . . . . . . 15 (𝐺𝑧) ∈ V
30 fvex 6199 . . . . . . . . . . . . . . 15 (𝐹𝑧) ∈ V
3129, 30ifex 4154 . . . . . . . . . . . . . 14 if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ V
3228, 6, 31fvmpt 6280 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝐻𝑧) = if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)))
3332adantl 482 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝐻𝑧) = if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)))
3433eleq1d 2685 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (𝑦(,)+∞) ↔ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (𝑦(,)+∞)))
3512, 9ifcld 4129 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ)
36 ltpnf 11951 . . . . . . . . . . . . 13 (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ → if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞)
3735, 36jccir 562 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞))
3837biantrud 528 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ↔ (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < +∞))))
3924, 34, 383bitr4d 300 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (𝑦(,)+∞) ↔ 𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧))))
4035rexrd 10086 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ*)
41 xrltnle 10102 . . . . . . . . . . 11 ((𝑦 ∈ ℝ* ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ*) → (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ↔ ¬ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦))
4214, 40, 41syl2anc 693 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ↔ ¬ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦))
4339, 42bitrd 268 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (𝑦(,)+∞) ↔ ¬ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ≤ 𝑦))
44 elioo2 12213 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝐹𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹𝑧) ∈ ℝ ∧ 𝑦 < (𝐹𝑧) ∧ (𝐹𝑧) < +∞)))
4514, 20, 44sylancl 694 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹𝑧) ∈ ℝ ∧ 𝑦 < (𝐹𝑧) ∧ (𝐹𝑧) < +∞)))
46 3anan12 1050 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ ℝ ∧ 𝑦 < (𝐹𝑧) ∧ (𝐹𝑧) < +∞) ↔ (𝑦 < (𝐹𝑧) ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < +∞)))
4745, 46syl6bb 276 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐹𝑧) ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < +∞))))
48 ltpnf 11951 . . . . . . . . . . . . 13 ((𝐹𝑧) ∈ ℝ → (𝐹𝑧) < +∞)
499, 48jccir 562 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < +∞))
5049biantrud 528 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < (𝐹𝑧) ↔ (𝑦 < (𝐹𝑧) ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < +∞))))
51 xrltnle 10102 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ* ∧ (𝐹𝑧) ∈ ℝ*) → (𝑦 < (𝐹𝑧) ↔ ¬ (𝐹𝑧) ≤ 𝑦))
5214, 10, 51syl2anc 693 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < (𝐹𝑧) ↔ ¬ (𝐹𝑧) ≤ 𝑦))
5347, 50, 523bitr2d 296 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹𝑧) ≤ 𝑦))
54 elioo2 12213 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝐺𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺𝑧) ∈ ℝ ∧ 𝑦 < (𝐺𝑧) ∧ (𝐺𝑧) < +∞)))
5514, 20, 54sylancl 694 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐺𝑧) ∈ ℝ ∧ 𝑦 < (𝐺𝑧) ∧ (𝐺𝑧) < +∞)))
56 3anan12 1050 . . . . . . . . . . . 12 (((𝐺𝑧) ∈ ℝ ∧ 𝑦 < (𝐺𝑧) ∧ (𝐺𝑧) < +∞) ↔ (𝑦 < (𝐺𝑧) ∧ ((𝐺𝑧) ∈ ℝ ∧ (𝐺𝑧) < +∞)))
5755, 56syl6bb 276 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑦(,)+∞) ↔ (𝑦 < (𝐺𝑧) ∧ ((𝐺𝑧) ∈ ℝ ∧ (𝐺𝑧) < +∞))))
58 ltpnf 11951 . . . . . . . . . . . . 13 ((𝐺𝑧) ∈ ℝ → (𝐺𝑧) < +∞)
5912, 58jccir 562 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ ℝ ∧ (𝐺𝑧) < +∞))
6059biantrud 528 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < (𝐺𝑧) ↔ (𝑦 < (𝐺𝑧) ∧ ((𝐺𝑧) ∈ ℝ ∧ (𝐺𝑧) < +∞))))
61 xrltnle 10102 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ* ∧ (𝐺𝑧) ∈ ℝ*) → (𝑦 < (𝐺𝑧) ↔ ¬ (𝐺𝑧) ≤ 𝑦))
6214, 13, 61syl2anc 693 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (𝑦 < (𝐺𝑧) ↔ ¬ (𝐺𝑧) ≤ 𝑦))
6357, 60, 623bitr2d 296 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑦(,)+∞) ↔ ¬ (𝐺𝑧) ≤ 𝑦))
6453, 63orbi12d 746 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (((𝐹𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺𝑧) ∈ (𝑦(,)+∞)) ↔ (¬ (𝐹𝑧) ≤ 𝑦 ∨ ¬ (𝐺𝑧) ≤ 𝑦)))
6519, 43, 643bitr4d 300 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (𝑦(,)+∞) ↔ ((𝐹𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺𝑧) ∈ (𝑦(,)+∞))))
6665pm5.32da 673 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → ((𝑧𝐴 ∧ (𝐻𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ ((𝐹𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺𝑧) ∈ (𝑦(,)+∞)))))
67 andi 911 . . . . . . 7 ((𝑧𝐴 ∧ ((𝐹𝑧) ∈ (𝑦(,)+∞) ∨ (𝐺𝑧) ∈ (𝑦(,)+∞))) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑦(,)+∞))))
6866, 67syl6bb 276 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → ((𝑧𝐴 ∧ (𝐻𝑧) ∈ (𝑦(,)+∞)) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑦(,)+∞)))))
69 ffn 6043 . . . . . . . . 9 (𝐻:𝐴⟶ℝ → 𝐻 Fn 𝐴)
707, 69syl 17 . . . . . . . 8 (𝜑𝐻 Fn 𝐴)
7170adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → 𝐻 Fn 𝐴)
72 elpreima 6335 . . . . . . 7 (𝐻 Fn 𝐴 → (𝑧 ∈ (𝐻 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐻𝑧) ∈ (𝑦(,)+∞))))
7371, 72syl 17 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐻𝑧) ∈ (𝑦(,)+∞))))
74 ffn 6043 . . . . . . . . 9 (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴)
758, 74syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ*) → 𝐹 Fn 𝐴)
76 elpreima 6335 . . . . . . . 8 (𝐹 Fn 𝐴 → (𝑧 ∈ (𝐹 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (𝑦(,)+∞))))
7775, 76syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐹 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (𝑦(,)+∞))))
78 ffn 6043 . . . . . . . . 9 (𝐺:𝐴⟶ℝ → 𝐺 Fn 𝐴)
7911, 78syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ*) → 𝐺 Fn 𝐴)
80 elpreima 6335 . . . . . . . 8 (𝐺 Fn 𝐴 → (𝑧 ∈ (𝐺 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑦(,)+∞))))
8179, 80syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐺 “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑦(,)+∞))))
8277, 81orbi12d 746 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → ((𝑧 ∈ (𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (𝐺 “ (𝑦(,)+∞))) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (𝑦(,)+∞)) ∨ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑦(,)+∞)))))
8368, 73, 823bitr4d 300 . . . . 5 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (𝑦(,)+∞)) ↔ (𝑧 ∈ (𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (𝐺 “ (𝑦(,)+∞)))))
84 elun 3751 . . . . 5 (𝑧 ∈ ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞))) ↔ (𝑧 ∈ (𝐹 “ (𝑦(,)+∞)) ∨ 𝑧 ∈ (𝐺 “ (𝑦(,)+∞))))
8583, 84syl6bbr 278 . . . 4 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (𝑦(,)+∞)) ↔ 𝑧 ∈ ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞)))))
8685eqrdv 2619 . . 3 ((𝜑𝑦 ∈ ℝ*) → (𝐻 “ (𝑦(,)+∞)) = ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞))))
87 mbfmax.2 . . . . . 6 (𝜑𝐹 ∈ MblFn)
88 mbfima 23393 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
8987, 3, 88syl2anc 693 . . . . 5 (𝜑 → (𝐹 “ (𝑦(,)+∞)) ∈ dom vol)
90 mbfmax.4 . . . . . 6 (𝜑𝐺 ∈ MblFn)
91 mbfima 23393 . . . . . 6 ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
9290, 1, 91syl2anc 693 . . . . 5 (𝜑 → (𝐺 “ (𝑦(,)+∞)) ∈ dom vol)
93 unmbl 23299 . . . . 5 (((𝐹 “ (𝑦(,)+∞)) ∈ dom vol ∧ (𝐺 “ (𝑦(,)+∞)) ∈ dom vol) → ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
9489, 92, 93syl2anc 693 . . . 4 (𝜑 → ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
9594adantr 481 . . 3 ((𝜑𝑦 ∈ ℝ*) → ((𝐹 “ (𝑦(,)+∞)) ∪ (𝐺 “ (𝑦(,)+∞))) ∈ dom vol)
9686, 95eqeltrd 2700 . 2 ((𝜑𝑦 ∈ ℝ*) → (𝐻 “ (𝑦(,)+∞)) ∈ dom vol)
97 xrmaxlt 12009 . . . . . . . . . 10 (((𝐹𝑧) ∈ ℝ* ∧ (𝐺𝑧) ∈ ℝ*𝑦 ∈ ℝ*) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦 ↔ ((𝐹𝑧) < 𝑦 ∧ (𝐺𝑧) < 𝑦)))
9810, 13, 14, 97syl3anc 1325 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦 ↔ ((𝐹𝑧) < 𝑦 ∧ (𝐺𝑧) < 𝑦)))
99 mnfxr 10093 . . . . . . . . . . . 12 -∞ ∈ ℝ*
100 elioo2 12213 . . . . . . . . . . . 12 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦)))
10199, 14, 100sylancr 695 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (-∞(,)𝑦) ↔ (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦)))
102 df-3an 1039 . . . . . . . . . . 11 ((if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦) ↔ ((if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧))) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦))
103101, 102syl6bb 276 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (-∞(,)𝑦) ↔ ((if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧))) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦)))
10433eleq1d 2685 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ (-∞(,)𝑦)))
105 mnflt 11954 . . . . . . . . . . . 12 (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ → -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)))
10635, 105jccir 562 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧))))
107106biantrurd 529 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦 ↔ ((if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) ∈ ℝ ∧ -∞ < if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧))) ∧ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦)))
108103, 104, 1073bitr4d 300 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (-∞(,)𝑦) ↔ if((𝐹𝑧) ≤ (𝐺𝑧), (𝐺𝑧), (𝐹𝑧)) < 𝑦))
109 elioo2 12213 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*) → ((𝐹𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧) ∧ (𝐹𝑧) < 𝑦)))
11099, 14, 109sylancr 695 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧) ∧ (𝐹𝑧) < 𝑦)))
111 df-3an 1039 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧) ∧ (𝐹𝑧) < 𝑦) ↔ (((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧)) ∧ (𝐹𝑧) < 𝑦))
112110, 111syl6bb 276 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧)) ∧ (𝐹𝑧) < 𝑦)))
113 mnflt 11954 . . . . . . . . . . . . 13 ((𝐹𝑧) ∈ ℝ → -∞ < (𝐹𝑧))
1149, 113jccir 562 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧)))
115114biantrurd 529 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) < 𝑦 ↔ (((𝐹𝑧) ∈ ℝ ∧ -∞ < (𝐹𝑧)) ∧ (𝐹𝑧) < 𝑦)))
116112, 115bitr4d 271 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐹𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹𝑧) < 𝑦))
117 elioo2 12213 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*) → ((𝐺𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧) ∧ (𝐺𝑧) < 𝑦)))
11899, 14, 117sylancr 695 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧) ∧ (𝐺𝑧) < 𝑦)))
119 df-3an 1039 . . . . . . . . . . . 12 (((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧) ∧ (𝐺𝑧) < 𝑦) ↔ (((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧)) ∧ (𝐺𝑧) < 𝑦))
120118, 119syl6bb 276 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (-∞(,)𝑦) ↔ (((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧)) ∧ (𝐺𝑧) < 𝑦)))
121 mnflt 11954 . . . . . . . . . . . . 13 ((𝐺𝑧) ∈ ℝ → -∞ < (𝐺𝑧))
12212, 121jccir 562 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧)))
123122biantrurd 529 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) < 𝑦 ↔ (((𝐺𝑧) ∈ ℝ ∧ -∞ < (𝐺𝑧)) ∧ (𝐺𝑧) < 𝑦)))
124120, 123bitr4d 271 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (-∞(,)𝑦) ↔ (𝐺𝑧) < 𝑦))
125116, 124anbi12d 747 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → (((𝐹𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝐹𝑧) < 𝑦 ∧ (𝐺𝑧) < 𝑦)))
12698, 108, 1253bitr4d 300 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ*) ∧ 𝑧𝐴) → ((𝐻𝑧) ∈ (-∞(,)𝑦) ↔ ((𝐹𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺𝑧) ∈ (-∞(,)𝑦))))
127126pm5.32da 673 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → ((𝑧𝐴 ∧ (𝐻𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ ((𝐹𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺𝑧) ∈ (-∞(,)𝑦)))))
128 anandi 871 . . . . . . 7 ((𝑧𝐴 ∧ ((𝐹𝑧) ∈ (-∞(,)𝑦) ∧ (𝐺𝑧) ∈ (-∞(,)𝑦))) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (-∞(,)𝑦))))
129127, 128syl6bb 276 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → ((𝑧𝐴 ∧ (𝐻𝑧) ∈ (-∞(,)𝑦)) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (-∞(,)𝑦)))))
130 elpreima 6335 . . . . . . 7 (𝐻 Fn 𝐴 → (𝑧 ∈ (𝐻 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐻𝑧) ∈ (-∞(,)𝑦))))
13171, 130syl 17 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐻𝑧) ∈ (-∞(,)𝑦))))
132 elpreima 6335 . . . . . . . 8 (𝐹 Fn 𝐴 → (𝑧 ∈ (𝐹 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)𝑦))))
13375, 132syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐹 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)𝑦))))
134 elpreima 6335 . . . . . . . 8 (𝐺 Fn 𝐴 → (𝑧 ∈ (𝐺 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (-∞(,)𝑦))))
13579, 134syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐺 “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (-∞(,)𝑦))))
136133, 135anbi12d 747 . . . . . 6 ((𝜑𝑦 ∈ ℝ*) → ((𝑧 ∈ (𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (𝐺 “ (-∞(,)𝑦))) ↔ ((𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)𝑦)) ∧ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (-∞(,)𝑦)))))
137129, 131, 1363bitr4d 300 . . . . 5 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (-∞(,)𝑦)) ↔ (𝑧 ∈ (𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (𝐺 “ (-∞(,)𝑦)))))
138 elin 3794 . . . . 5 (𝑧 ∈ ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦))) ↔ (𝑧 ∈ (𝐹 “ (-∞(,)𝑦)) ∧ 𝑧 ∈ (𝐺 “ (-∞(,)𝑦))))
139137, 138syl6bbr 278 . . . 4 ((𝜑𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐻 “ (-∞(,)𝑦)) ↔ 𝑧 ∈ ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦)))))
140139eqrdv 2619 . . 3 ((𝜑𝑦 ∈ ℝ*) → (𝐻 “ (-∞(,)𝑦)) = ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦))))
141 mbfima 23393 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
14287, 3, 141syl2anc 693 . . . . 5 (𝜑 → (𝐹 “ (-∞(,)𝑦)) ∈ dom vol)
143 mbfima 23393 . . . . . 6 ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
14490, 1, 143syl2anc 693 . . . . 5 (𝜑 → (𝐺 “ (-∞(,)𝑦)) ∈ dom vol)
145 inmbl 23304 . . . . 5 (((𝐹 “ (-∞(,)𝑦)) ∈ dom vol ∧ (𝐺 “ (-∞(,)𝑦)) ∈ dom vol) → ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
146142, 144, 145syl2anc 693 . . . 4 (𝜑 → ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
147146adantr 481 . . 3 ((𝜑𝑦 ∈ ℝ*) → ((𝐹 “ (-∞(,)𝑦)) ∩ (𝐺 “ (-∞(,)𝑦))) ∈ dom vol)
148140, 147eqeltrd 2700 . 2 ((𝜑𝑦 ∈ ℝ*) → (𝐻 “ (-∞(,)𝑦)) ∈ dom vol)
1497, 96, 148ismbfd 23401 1 (𝜑𝐻 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1037   = wceq 1482  wcel 1989  cun 3570  cin 3571  ifcif 4084   class class class wbr 4651  cmpt 4727  ccnv 5111  dom cdm 5112  cima 5115   Fn wfn 5881  wf 5882  cfv 5886  (class class class)co 6647  cr 9932  +∞cpnf 10068  -∞cmnf 10069  *cxr 10070   < clt 10071  cle 10072  (,)cioo 12172  volcvol 23226  MblFncmbf 23377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-of 6894  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-inf 8346  df-oi 8412  df-card 8762  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-q 11786  df-rp 11830  df-xadd 11944  df-ioo 12176  df-ico 12178  df-icc 12179  df-fz 12324  df-fzo 12462  df-fl 12588  df-seq 12797  df-exp 12856  df-hash 13113  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-sum 14411  df-xmet 19733  df-met 19734  df-ovol 23227  df-vol 23228  df-mbf 23382
This theorem is referenced by:  mbfpos  23412
  Copyright terms: Public domain W3C validator