Metamath Proof Explorer

Theorem mbfeqalem2

Description: Lemma for mbfeqa . (Contributed by Mario Carneiro, 2-Sep-2014) (Proof shortened by AV, 19-Aug-2022)

Ref Expression
Hypotheses mbfeqa.1 ⊢ φ → A ⊆ ℝ
mbfeqa.2 ⊢ φ → vol * ⁡ A = 0
mbfeqa.3 ⊢ φ ∧ x ∈ B ∖ A → C = D
mbfeqalem.4 ⊢ φ ∧ x ∈ B → C ∈ ℝ
mbfeqalem.5 ⊢ φ ∧ x ∈ B → D ∈ ℝ
Assertion mbfeqalem2 ⊢ φ → x ∈ B ⟼ C ∈ MblFn ↔ x ∈ B ⟼ D ∈ MblFn

Proof

Step Hyp Ref Expression
1 mbfeqa.1 ⊢ φ → A ⊆ ℝ
2 mbfeqa.2 ⊢ φ → vol * ⁡ A = 0
3 mbfeqa.3 ⊢ φ ∧ x ∈ B ∖ A → C = D
4 mbfeqalem.4 ⊢ φ ∧ x ∈ B → C ∈ ℝ
5 mbfeqalem.5 ⊢ φ ∧ x ∈ B → D ∈ ℝ
6 inundif ⊢ x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y ∪ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y = x ∈ B ⟼ D -1 y
7 incom ⊢ x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y = x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y
8 dfin4 ⊢ x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y = x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y
9 7 8 eqtri ⊢ x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y = x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y
10 id ⊢ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
11 1 2 3 4 5 mbfeqalem1 ⊢ φ → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
12 difmbl ⊢ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol ∧ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
13 10 11 12 syl2anr ⊢ φ ∧ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
14 9 13 eqeltrid ⊢ φ ∧ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
15 3 eqcomd ⊢ φ ∧ x ∈ B ∖ A → D = C
16 1 2 15 5 4 mbfeqalem1 ⊢ φ → x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
17 16 adantr ⊢ φ ∧ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
18 unmbl ⊢ x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol ∧ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y ∪ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
19 14 17 18 syl2anc ⊢ φ ∧ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y ∪ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
20 6 19 eqeltrrid ⊢ φ ∧ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
21 inundif ⊢ x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y ∪ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y = x ∈ B ⟼ C -1 y
22 incom ⊢ x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y = x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y
23 dfin4 ⊢ x ∈ B ⟼ D -1 y ∩ x ∈ B ⟼ C -1 y = x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y
24 22 23 eqtri ⊢ x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y = x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y
25 id ⊢ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
26 difmbl ⊢ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol ∧ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
27 25 16 26 syl2anr ⊢ φ ∧ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ D -1 y ∖ x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
28 24 27 eqeltrid ⊢ φ ∧ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
29 11 adantr ⊢ φ ∧ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
30 unmbl ⊢ x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol ∧ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y ∪ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
31 28 29 30 syl2anc ⊢ φ ∧ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∩ x ∈ B ⟼ D -1 y ∪ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
32 21 31 eqeltrrid ⊢ φ ∧ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol → x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
33 20 32 impbida ⊢ φ → x ∈ B ⟼ C -1 y ∈ dom ⁡ vol ↔ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
34 33 ralbidv ⊢ φ → ∀ y ∈ ran ⁡ . x ∈ B ⟼ C -1 y ∈ dom ⁡ vol ↔ ∀ y ∈ ran ⁡ . x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
35 4 fmpttd ⊢ φ → x ∈ B ⟼ C : B ⟶ ℝ
36 ismbf ⊢ x ∈ B ⟼ C : B ⟶ ℝ → x ∈ B ⟼ C ∈ MblFn ↔ ∀ y ∈ ran ⁡ . x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
37 35 36 syl ⊢ φ → x ∈ B ⟼ C ∈ MblFn ↔ ∀ y ∈ ran ⁡ . x ∈ B ⟼ C -1 y ∈ dom ⁡ vol
38 5 fmpttd ⊢ φ → x ∈ B ⟼ D : B ⟶ ℝ
39 ismbf ⊢ x ∈ B ⟼ D : B ⟶ ℝ → x ∈ B ⟼ D ∈ MblFn ↔ ∀ y ∈ ran ⁡ . x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
40 38 39 syl ⊢ φ → x ∈ B ⟼ D ∈ MblFn ↔ ∀ y ∈ ran ⁡ . x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
41 34 37 40 3bitr4d ⊢ φ → x ∈ B ⟼ C ∈ MblFn ↔ x ∈ B ⟼ D ∈ MblFn