Metamath Proof Explorer

Theorem mbfposadd

Description: If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018)

Ref Expression
Hypotheses mbfposadd.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
mbfposadd.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
mbfposadd.3 ⊢ φ → x ∈ A ⟼ C ∈ MblFn
mbfposadd.4 ⊢ φ ∧ x ∈ A → C ∈ ℝ
mbfposadd.5 ⊢ φ → x ∈ A ⟼ B + C ∈ MblFn
Assertion mbfposadd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ MblFn

Proof

Step Hyp Ref Expression
1 mbfposadd.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
2 mbfposadd.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 mbfposadd.3 ⊢ φ → x ∈ A ⟼ C ∈ MblFn
4 mbfposadd.4 ⊢ φ ∧ x ∈ A → C ∈ ℝ
5 mbfposadd.5 ⊢ φ → x ∈ A ⟼ B + C ∈ MblFn
6 0re ⊢ 0 ∈ ℝ
7 ifcl ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ B B 0 ∈ ℝ
8 2 6 7 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℝ
9 ifcl ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ C C 0 ∈ ℝ
10 4 6 9 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℝ
11 8 10 readdcld ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℝ
12 11 fmpttd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 : A ⟶ ℝ
13 ssrab2 ⊢ x ∈ A | 0 ≤ C ⊆ A
14 fssres ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 : A ⟶ ℝ ∧ x ∈ A | 0 ≤ C ⊆ A → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C : x ∈ A | 0 ≤ C ⟶ ℝ
15 12 13 14 sylancl ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C : x ∈ A | 0 ≤ C ⟶ ℝ
16 inss2 ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | 0 ≤ C
17 resabs1 ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | 0 ≤ C → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
18 16 17 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
19 elin ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ x ∈ x ∈ A | 0 ≤ B ∧ x ∈ x ∈ A | 0 ≤ C
20 rabid ⊢ x ∈ x ∈ A | 0 ≤ B ↔ x ∈ A ∧ 0 ≤ B
21 rabid ⊢ x ∈ x ∈ A | 0 ≤ C ↔ x ∈ A ∧ 0 ≤ C
22 20 21 anbi12i ⊢ x ∈ x ∈ A | 0 ≤ B ∧ x ∈ x ∈ A | 0 ≤ C ↔ x ∈ A ∧ 0 ≤ B ∧ x ∈ A ∧ 0 ≤ C
23 19 22 bitri ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ x ∈ A ∧ 0 ≤ B ∧ x ∈ A ∧ 0 ≤ C
24 iftrue ⊢ 0 ≤ B → if 0 ≤ B B 0 = B
25 iftrue ⊢ 0 ≤ C → if 0 ≤ C C 0 = C
26 24 25 oveqan12d ⊢ 0 ≤ B ∧ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = B + C
27 26 ad2ant2l ⊢ x ∈ A ∧ 0 ≤ B ∧ x ∈ A ∧ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = B + C
28 23 27 sylbi ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = B + C
29 28 mpteq2ia ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ B + C
30 inss1 ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | 0 ≤ B
31 ssrab2 ⊢ x ∈ A | 0 ≤ B ⊆ A
32 30 31 sstri ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A
33 resmpt ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
34 nfcv ⊢ Ⅎ _ y if 0 ≤ B B 0 + if 0 ≤ C C 0
35 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
36 csbeq1a ⊢ x = y → if 0 ≤ B B 0 + if 0 ≤ C C 0 = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
37 34 35 36 cbvmpt ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
38 37 reseq1i ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
39 nfv ⊢ Ⅎ y x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
40 nfrab1 ⊢ Ⅎ _ x x ∈ A | 0 ≤ B
41 nfrab1 ⊢ Ⅎ _ x x ∈ A | 0 ≤ C
42 40 41 nfin ⊢ Ⅎ _ x x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
43 42 nfcri ⊢ Ⅎ x y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
44 35 nfeq2 ⊢ Ⅎ x z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
45 43 44 nfan ⊢ Ⅎ x y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
46 eleq1w ⊢ x = y → x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
47 36 eqeq2d ⊢ x = y → z = if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
48 46 47 anbi12d ⊢ x = y → x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
49 39 45 48 cbvopab1 ⊢ x z | x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
50 df-mpt ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x z | x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
51 df-mpt ⊢ y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
52 49 50 51 3eqtr4i ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
53 33 38 52 3eqtr4g ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
54 32 53 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
55 resmpt ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ B + C
56 nfcv ⊢ Ⅎ _ y B + C
57 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B + C
58 csbeq1a ⊢ x = y → B + C = ⦋ y / x⦌ B + C
59 56 57 58 cbvmpt ⊢ x ∈ A ⟼ B + C = y ∈ A ⟼ ⦋ y / x⦌ B + C
60 59 reseq1i ⊢ x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
61 nfv ⊢ Ⅎ y x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = B + C
62 57 nfeq2 ⊢ Ⅎ x z = ⦋ y / x⦌ B + C
63 43 62 nfan ⊢ Ⅎ x y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ B + C
64 58 eqeq2d ⊢ x = y → z = B + C ↔ z = ⦋ y / x⦌ B + C
65 46 64 anbi12d ⊢ x = y → x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = B + C ↔ y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ B + C
66 61 63 65 cbvopab1 ⊢ x z | x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = B + C = y z | y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ B + C
67 df-mpt ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ B + C = x z | x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = B + C
68 df-mpt ⊢ y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ B + C = y z | y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ B + C
69 66 67 68 3eqtr4i ⊢ x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ B + C = y ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ B + C
70 55 60 69 3eqtr4g ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ B + C
71 32 70 ax-mp ⊢ x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ B + C
72 29 54 71 3eqtr4i ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
73 18 72 eqtri ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C
74 2 biantrurd ⊢ φ ∧ x ∈ A → 0 ≤ B ↔ B ∈ ℝ ∧ 0 ≤ B
75 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
76 74 75 bitr4di ⊢ φ ∧ x ∈ A → 0 ≤ B ↔ B ∈ 0 +∞
77 76 rabbidva ⊢ φ → x ∈ A | 0 ≤ B = x ∈ A | B ∈ 0 +∞
78 0xr ⊢ 0 ∈ ℝ *
79 pnfxr ⊢ +∞ ∈ ℝ *
80 0ltpnf ⊢ 0 < +∞
81 snunioo ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 0 < +∞ → 0 ∪ 0 +∞ = 0 +∞
82 78 79 80 81 mp3an ⊢ 0 ∪ 0 +∞ = 0 +∞
83 82 imaeq2i ⊢ x ∈ A ⟼ B -1 0 ∪ 0 +∞ = x ∈ A ⟼ B -1 0 +∞
84 imaundi ⊢ x ∈ A ⟼ B -1 0 ∪ 0 +∞ = x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞
85 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
86 85 mptpreima ⊢ x ∈ A ⟼ B -1 0 +∞ = x ∈ A | B ∈ 0 +∞
87 83 84 86 3eqtr3ri ⊢ x ∈ A | B ∈ 0 +∞ = x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞
88 77 87 eqtrdi ⊢ φ → x ∈ A | 0 ≤ B = x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞
89 2 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ
90 mbfimasn ⊢ x ∈ A ⟼ B ∈ MblFn ∧ x ∈ A ⟼ B : A ⟶ ℝ ∧ 0 ∈ ℝ → x ∈ A ⟼ B -1 0 ∈ dom ⁡ vol
91 6 90 mp3an3 ⊢ x ∈ A ⟼ B ∈ MblFn ∧ x ∈ A ⟼ B : A ⟶ ℝ → x ∈ A ⟼ B -1 0 ∈ dom ⁡ vol
92 mbfima ⊢ x ∈ A ⟼ B ∈ MblFn ∧ x ∈ A ⟼ B : A ⟶ ℝ → x ∈ A ⟼ B -1 0 +∞ ∈ dom ⁡ vol
93 unmbl ⊢ x ∈ A ⟼ B -1 0 ∈ dom ⁡ vol ∧ x ∈ A ⟼ B -1 0 +∞ ∈ dom ⁡ vol → x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞ ∈ dom ⁡ vol
94 91 92 93 syl2anc ⊢ x ∈ A ⟼ B ∈ MblFn ∧ x ∈ A ⟼ B : A ⟶ ℝ → x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞ ∈ dom ⁡ vol
95 1 89 94 syl2anc ⊢ φ → x ∈ A ⟼ B -1 0 ∪ x ∈ A ⟼ B -1 0 +∞ ∈ dom ⁡ vol
96 88 95 eqeltrd ⊢ φ → x ∈ A | 0 ≤ B ∈ dom ⁡ vol
97 4 biantrurd ⊢ φ ∧ x ∈ A → 0 ≤ C ↔ C ∈ ℝ ∧ 0 ≤ C
98 elrege0 ⊢ C ∈ 0 +∞ ↔ C ∈ ℝ ∧ 0 ≤ C
99 97 98 bitr4di ⊢ φ ∧ x ∈ A → 0 ≤ C ↔ C ∈ 0 +∞
100 99 rabbidva ⊢ φ → x ∈ A | 0 ≤ C = x ∈ A | C ∈ 0 +∞
101 82 imaeq2i ⊢ x ∈ A ⟼ C -1 0 ∪ 0 +∞ = x ∈ A ⟼ C -1 0 +∞
102 imaundi ⊢ x ∈ A ⟼ C -1 0 ∪ 0 +∞ = x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞
103 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
104 103 mptpreima ⊢ x ∈ A ⟼ C -1 0 +∞ = x ∈ A | C ∈ 0 +∞
105 101 102 104 3eqtr3ri ⊢ x ∈ A | C ∈ 0 +∞ = x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞
106 100 105 eqtrdi ⊢ φ → x ∈ A | 0 ≤ C = x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞
107 4 fmpttd ⊢ φ → x ∈ A ⟼ C : A ⟶ ℝ
108 mbfimasn ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A ⟼ C : A ⟶ ℝ ∧ 0 ∈ ℝ → x ∈ A ⟼ C -1 0 ∈ dom ⁡ vol
109 6 108 mp3an3 ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A ⟼ C : A ⟶ ℝ → x ∈ A ⟼ C -1 0 ∈ dom ⁡ vol
110 mbfima ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A ⟼ C : A ⟶ ℝ → x ∈ A ⟼ C -1 0 +∞ ∈ dom ⁡ vol
111 unmbl ⊢ x ∈ A ⟼ C -1 0 ∈ dom ⁡ vol ∧ x ∈ A ⟼ C -1 0 +∞ ∈ dom ⁡ vol → x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞ ∈ dom ⁡ vol
112 109 110 111 syl2anc ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A ⟼ C : A ⟶ ℝ → x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞ ∈ dom ⁡ vol
113 3 107 112 syl2anc ⊢ φ → x ∈ A ⟼ C -1 0 ∪ x ∈ A ⟼ C -1 0 +∞ ∈ dom ⁡ vol
114 106 113 eqeltrd ⊢ φ → x ∈ A | 0 ≤ C ∈ dom ⁡ vol
115 inmbl ⊢ x ∈ A | 0 ≤ B ∈ dom ⁡ vol ∧ x ∈ A | 0 ≤ C ∈ dom ⁡ vol → x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol
116 96 114 115 syl2anc ⊢ φ → x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol
117 mbfres ⊢ x ∈ A ⟼ B + C ∈ MblFn ∧ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol → x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
118 5 116 117 syl2anc ⊢ φ → x ∈ A ⟼ B + C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
119 73 118 eqeltrid ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
120 inss2 ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | 0 ≤ C
121 resabs1 ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | 0 ≤ C → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
122 120 121 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
123 rabid ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ↔ x ∈ A ∧ ¬ 0 ≤ B
124 123 21 anbi12i ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∧ x ∈ x ∈ A | 0 ≤ C ↔ x ∈ A ∧ ¬ 0 ≤ B ∧ x ∈ A ∧ 0 ≤ C
125 elin ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ x ∈ x ∈ A | ¬ 0 ≤ B ∧ x ∈ x ∈ A | 0 ≤ C
126 anandi ⊢ x ∈ A ∧ ¬ 0 ≤ B ∧ 0 ≤ C ↔ x ∈ A ∧ ¬ 0 ≤ B ∧ x ∈ A ∧ 0 ≤ C
127 124 125 126 3bitr4i ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ x ∈ A ∧ ¬ 0 ≤ B ∧ 0 ≤ C
128 iffalse ⊢ ¬ 0 ≤ B → if 0 ≤ B B 0 = 0
129 128 25 oveqan12d ⊢ ¬ 0 ≤ B ∧ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = 0 + C
130 129 ad2antll ⊢ φ ∧ x ∈ A ∧ ¬ 0 ≤ B ∧ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = 0 + C
131 4 recnd ⊢ φ ∧ x ∈ A → C ∈ ℂ
132 131 addlidd ⊢ φ ∧ x ∈ A → 0 + C = C
133 132 adantrr ⊢ φ ∧ x ∈ A ∧ ¬ 0 ≤ B ∧ 0 ≤ C → 0 + C = C
134 130 133 eqtrd ⊢ φ ∧ x ∈ A ∧ ¬ 0 ≤ B ∧ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = C
135 127 134 sylan2b ⊢ φ ∧ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = C
136 135 mpteq2dva ⊢ φ → x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ C
137 inss1 ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ x ∈ A | ¬ 0 ≤ B
138 ssrab2 ⊢ x ∈ A | ¬ 0 ≤ B ⊆ A
139 137 138 sstri ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A
140 resmpt ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
141 37 reseq1i ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
142 nfv ⊢ Ⅎ y x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
143 nfrab1 ⊢ Ⅎ _ x x ∈ A | ¬ 0 ≤ B
144 143 41 nfin ⊢ Ⅎ _ x x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
145 144 nfcri ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
146 145 44 nfan ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
147 eleq1w ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ↔ y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
148 147 47 anbi12d ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
149 142 146 148 cbvopab1 ⊢ x z | x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
150 df-mpt ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x z | x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
151 df-mpt ⊢ y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
152 149 150 151 3eqtr4i ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
153 140 141 152 3eqtr4g ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
154 139 153 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
155 resmpt ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ C
156 nfcv ⊢ Ⅎ _ y C
157 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
158 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
159 156 157 158 cbvmpt ⊢ x ∈ A ⟼ C = y ∈ A ⟼ ⦋ y / x⦌ C
160 159 reseq1i ⊢ x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
161 nfv ⊢ Ⅎ y x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = C
162 157 nfeq2 ⊢ Ⅎ x z = ⦋ y / x⦌ C
163 145 162 nfan ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ C
164 158 eqeq2d ⊢ x = y → z = C ↔ z = ⦋ y / x⦌ C
165 147 164 anbi12d ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = C ↔ y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ C
166 161 163 165 cbvopab1 ⊢ x z | x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = C = y z | y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ C
167 df-mpt ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ C = x z | x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = C
168 df-mpt ⊢ y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ C = y z | y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∧ z = ⦋ y / x⦌ C
169 166 167 168 3eqtr4i ⊢ x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ C = y ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ ⦋ y / x⦌ C
170 155 160 169 3eqtr4g ⊢ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⊆ A → x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ C
171 139 170 ax-mp ⊢ x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ⟼ C
172 136 154 171 3eqtr4g ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
173 122 172 eqtrid ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
174 85 mptpreima ⊢ x ∈ A ⟼ B -1 −∞ 0 = x ∈ A | B ∈ −∞ 0
175 elioomnf ⊢ 0 ∈ ℝ * → B ∈ −∞ 0 ↔ B ∈ ℝ ∧ B < 0
176 78 175 ax-mp ⊢ B ∈ −∞ 0 ↔ B ∈ ℝ ∧ B < 0
177 2 biantrurd ⊢ φ ∧ x ∈ A → B < 0 ↔ B ∈ ℝ ∧ B < 0
178 ltnle ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → B < 0 ↔ ¬ 0 ≤ B
179 2 6 178 sylancl ⊢ φ ∧ x ∈ A → B < 0 ↔ ¬ 0 ≤ B
180 177 179 bitr3d ⊢ φ ∧ x ∈ A → B ∈ ℝ ∧ B < 0 ↔ ¬ 0 ≤ B
181 176 180 bitrid ⊢ φ ∧ x ∈ A → B ∈ −∞ 0 ↔ ¬ 0 ≤ B
182 181 rabbidva ⊢ φ → x ∈ A | B ∈ −∞ 0 = x ∈ A | ¬ 0 ≤ B
183 174 182 eqtrid ⊢ φ → x ∈ A ⟼ B -1 −∞ 0 = x ∈ A | ¬ 0 ≤ B
184 mbfima ⊢ x ∈ A ⟼ B ∈ MblFn ∧ x ∈ A ⟼ B : A ⟶ ℝ → x ∈ A ⟼ B -1 −∞ 0 ∈ dom ⁡ vol
185 1 89 184 syl2anc ⊢ φ → x ∈ A ⟼ B -1 −∞ 0 ∈ dom ⁡ vol
186 183 185 eqeltrrd ⊢ φ → x ∈ A | ¬ 0 ≤ B ∈ dom ⁡ vol
187 inmbl ⊢ x ∈ A | ¬ 0 ≤ B ∈ dom ⁡ vol ∧ x ∈ A | 0 ≤ C ∈ dom ⁡ vol → x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol
188 186 114 187 syl2anc ⊢ φ → x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol
189 mbfres ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ dom ⁡ vol → x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
190 3 188 189 syl2anc ⊢ φ → x ∈ A ⟼ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
191 173 190 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ↾ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C ∈ MblFn
192 ssid ⊢ A ⊆ A
193 dfrab3ss ⊢ A ⊆ A → x ∈ A | 0 ≤ C = A ∩ x ∈ A | 0 ≤ C
194 192 193 ax-mp ⊢ x ∈ A | 0 ≤ C = A ∩ x ∈ A | 0 ≤ C
195 rabxm ⊢ A = x ∈ A | 0 ≤ B ∪ x ∈ A | ¬ 0 ≤ B
196 195 ineq1i ⊢ A ∩ x ∈ A | 0 ≤ C = x ∈ A | 0 ≤ B ∪ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
197 indir ⊢ x ∈ A | 0 ≤ B ∪ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C
198 194 196 197 3eqtrri ⊢ x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A | 0 ≤ C
199 198 a1i ⊢ φ → x ∈ A | 0 ≤ B ∩ x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ B ∩ x ∈ A | 0 ≤ C = x ∈ A | 0 ≤ C
200 15 119 191 199 mbfres2 ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | 0 ≤ C ∈ MblFn
201 rabid ⊢ x ∈ x ∈ A | ¬ 0 ≤ C ↔ x ∈ A ∧ ¬ 0 ≤ C
202 iffalse ⊢ ¬ 0 ≤ C → if 0 ≤ C C 0 = 0
203 202 oveq2d ⊢ ¬ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B B 0 + 0
204 8 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℂ
205 204 addridd ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + 0 = if 0 ≤ B B 0
206 203 205 sylan9eqr ⊢ φ ∧ x ∈ A ∧ ¬ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B B 0
207 206 anasss ⊢ φ ∧ x ∈ A ∧ ¬ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B B 0
208 201 207 sylan2b ⊢ φ ∧ x ∈ x ∈ A | ¬ 0 ≤ C → if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B B 0
209 208 mpteq2dva ⊢ φ → x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0
210 ssrab2 ⊢ x ∈ A | ¬ 0 ≤ C ⊆ A
211 resmpt ⊢ x ∈ A | ¬ 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C = y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
212 37 reseq1i ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C
213 nfv ⊢ Ⅎ y x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
214 nfrab1 ⊢ Ⅎ _ x x ∈ A | ¬ 0 ≤ C
215 214 nfcri ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ C
216 215 44 nfan ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
217 eleq1w ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ C ↔ y ∈ x ∈ A | ¬ 0 ≤ C
218 217 47 anbi12d ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
219 213 216 218 cbvopab1 ⊢ x z | x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
220 df-mpt ⊢ x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = x z | x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 + if 0 ≤ C C 0
221 df-mpt ⊢ y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
222 219 220 221 3eqtr4i ⊢ x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 = y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 + if 0 ≤ C C 0
223 211 212 222 3eqtr4g ⊢ x ∈ A | ¬ 0 ≤ C ⊆ A → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
224 210 223 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0
225 resmpt ⊢ x ∈ A | ¬ 0 ≤ C ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C = y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0
226 nfcv ⊢ Ⅎ _ y if 0 ≤ B B 0
227 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ if 0 ≤ B B 0
228 csbeq1a ⊢ x = y → if 0 ≤ B B 0 = ⦋ y / x⦌ if 0 ≤ B B 0
229 226 227 228 cbvmpt ⊢ x ∈ A ⟼ if 0 ≤ B B 0 = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0
230 229 reseq1i ⊢ x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C = y ∈ A ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C
231 nfv ⊢ Ⅎ y x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0
232 227 nfeq2 ⊢ Ⅎ x z = ⦋ y / x⦌ if 0 ≤ B B 0
233 215 232 nfan ⊢ Ⅎ x y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0
234 228 eqeq2d ⊢ x = y → z = if 0 ≤ B B 0 ↔ z = ⦋ y / x⦌ if 0 ≤ B B 0
235 217 234 anbi12d ⊢ x = y → x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 ↔ y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0
236 231 233 235 cbvopab1 ⊢ x z | x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0
237 df-mpt ⊢ x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 = x z | x ∈ x ∈ A | ¬ 0 ≤ C ∧ z = if 0 ≤ B B 0
238 df-mpt ⊢ y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0 = y z | y ∈ x ∈ A | ¬ 0 ≤ C ∧ z = ⦋ y / x⦌ if 0 ≤ B B 0
239 236 237 238 3eqtr4i ⊢ x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0 = y ∈ x ∈ A | ¬ 0 ≤ C ⟼ ⦋ y / x⦌ if 0 ≤ B B 0
240 225 230 239 3eqtr4g ⊢ x ∈ A | ¬ 0 ≤ C ⊆ A → x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0
241 210 240 ax-mp ⊢ x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C = x ∈ x ∈ A | ¬ 0 ≤ C ⟼ if 0 ≤ B B 0
242 209 224 241 3eqtr4g ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C = x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C
243 2 1 mbfpos ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
244 103 mptpreima ⊢ x ∈ A ⟼ C -1 −∞ 0 = x ∈ A | C ∈ −∞ 0
245 elioomnf ⊢ 0 ∈ ℝ * → C ∈ −∞ 0 ↔ C ∈ ℝ ∧ C < 0
246 78 245 ax-mp ⊢ C ∈ −∞ 0 ↔ C ∈ ℝ ∧ C < 0
247 4 biantrurd ⊢ φ ∧ x ∈ A → C < 0 ↔ C ∈ ℝ ∧ C < 0
248 ltnle ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → C < 0 ↔ ¬ 0 ≤ C
249 4 6 248 sylancl ⊢ φ ∧ x ∈ A → C < 0 ↔ ¬ 0 ≤ C
250 247 249 bitr3d ⊢ φ ∧ x ∈ A → C ∈ ℝ ∧ C < 0 ↔ ¬ 0 ≤ C
251 246 250 bitrid ⊢ φ ∧ x ∈ A → C ∈ −∞ 0 ↔ ¬ 0 ≤ C
252 251 rabbidva ⊢ φ → x ∈ A | C ∈ −∞ 0 = x ∈ A | ¬ 0 ≤ C
253 244 252 eqtrid ⊢ φ → x ∈ A ⟼ C -1 −∞ 0 = x ∈ A | ¬ 0 ≤ C
254 mbfima ⊢ x ∈ A ⟼ C ∈ MblFn ∧ x ∈ A ⟼ C : A ⟶ ℝ → x ∈ A ⟼ C -1 −∞ 0 ∈ dom ⁡ vol
255 3 107 254 syl2anc ⊢ φ → x ∈ A ⟼ C -1 −∞ 0 ∈ dom ⁡ vol
256 253 255 eqeltrrd ⊢ φ → x ∈ A | ¬ 0 ≤ C ∈ dom ⁡ vol
257 mbfres ⊢ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A | ¬ 0 ≤ C ∈ dom ⁡ vol → x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C ∈ MblFn
258 243 256 257 syl2anc ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ↾ x ∈ A | ¬ 0 ≤ C ∈ MblFn
259 242 258 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↾ x ∈ A | ¬ 0 ≤ C ∈ MblFn
260 rabxm ⊢ A = x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ C
261 260 eqcomi ⊢ x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ C = A
262 261 a1i ⊢ φ → x ∈ A | 0 ≤ C ∪ x ∈ A | ¬ 0 ≤ C = A
263 12 200 259 262 mbfres2 ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ MblFn