Metamath Proof Explorer

Theorem mbfeqalem1

Description: Lemma for mbfeqalem2 . (Contributed by Mario Carneiro, 2-Sep-2014) (Revised 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 mbfeqalem1 ⊢ φ → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol

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 dfsymdif4 ⊢ x ∈ B ⟼ C -1 y ∆ x ∈ B ⟼ D -1 y = z | ¬ z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ x ∈ B ⟼ D -1 y
7 eldif ⊢ z ∈ B ∖ A ↔ z ∈ B ∧ ¬ z ∈ A
8 eldifi ⊢ x ∈ B ∖ A → x ∈ B
9 8 4 sylan2 ⊢ φ ∧ x ∈ B ∖ A → C ∈ ℝ
10 eqid ⊢ x ∈ B ⟼ C = x ∈ B ⟼ C
11 10 fvmpt2 ⊢ x ∈ B ∧ C ∈ ℝ → x ∈ B ⟼ C ⁡ x = C
12 8 9 11 syl2an2 ⊢ φ ∧ x ∈ B ∖ A → x ∈ B ⟼ C ⁡ x = C
13 8 5 sylan2 ⊢ φ ∧ x ∈ B ∖ A → D ∈ ℝ
14 eqid ⊢ x ∈ B ⟼ D = x ∈ B ⟼ D
15 14 fvmpt2 ⊢ x ∈ B ∧ D ∈ ℝ → x ∈ B ⟼ D ⁡ x = D
16 8 13 15 syl2an2 ⊢ φ ∧ x ∈ B ∖ A → x ∈ B ⟼ D ⁡ x = D
17 3 12 16 3eqtr4d ⊢ φ ∧ x ∈ B ∖ A → x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ D ⁡ x
18 17 ralrimiva ⊢ φ → ∀ x ∈ B ∖ A x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ D ⁡ x
19 nfv ⊢ Ⅎ z x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ D ⁡ x
20 nffvmpt1 ⊢ Ⅎ _ x x ∈ B ⟼ C ⁡ z
21 nffvmpt1 ⊢ Ⅎ _ x x ∈ B ⟼ D ⁡ z
22 20 21 nfeq ⊢ Ⅎ x x ∈ B ⟼ C ⁡ z = x ∈ B ⟼ D ⁡ z
23 fveq2 ⊢ x = z → x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ C ⁡ z
24 fveq2 ⊢ x = z → x ∈ B ⟼ D ⁡ x = x ∈ B ⟼ D ⁡ z
25 23 24 eqeq12d ⊢ x = z → x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ D ⁡ x ↔ x ∈ B ⟼ C ⁡ z = x ∈ B ⟼ D ⁡ z
26 19 22 25 cbvralw ⊢ ∀ x ∈ B ∖ A x ∈ B ⟼ C ⁡ x = x ∈ B ⟼ D ⁡ x ↔ ∀ z ∈ B ∖ A x ∈ B ⟼ C ⁡ z = x ∈ B ⟼ D ⁡ z
27 18 26 sylib ⊢ φ → ∀ z ∈ B ∖ A x ∈ B ⟼ C ⁡ z = x ∈ B ⟼ D ⁡ z
28 27 r19.21bi ⊢ φ ∧ z ∈ B ∖ A → x ∈ B ⟼ C ⁡ z = x ∈ B ⟼ D ⁡ z
29 28 eleq1d ⊢ φ ∧ z ∈ B ∖ A → x ∈ B ⟼ C ⁡ z ∈ y ↔ x ∈ B ⟼ D ⁡ z ∈ y
30 7 29 sylan2br ⊢ φ ∧ z ∈ B ∧ ¬ z ∈ A → x ∈ B ⟼ C ⁡ z ∈ y ↔ x ∈ B ⟼ D ⁡ z ∈ y
31 30 anass1rs ⊢ φ ∧ ¬ z ∈ A ∧ z ∈ B → x ∈ B ⟼ C ⁡ z ∈ y ↔ x ∈ B ⟼ D ⁡ z ∈ y
32 31 pm5.32da ⊢ φ ∧ ¬ z ∈ A → z ∈ B ∧ x ∈ B ⟼ C ⁡ z ∈ y ↔ z ∈ B ∧ x ∈ B ⟼ D ⁡ z ∈ y
33 4 fmpttd ⊢ φ → x ∈ B ⟼ C : B ⟶ ℝ
34 33 ffnd ⊢ φ → x ∈ B ⟼ C Fn B
35 34 adantr ⊢ φ ∧ ¬ z ∈ A → x ∈ B ⟼ C Fn B
36 elpreima ⊢ x ∈ B ⟼ C Fn B → z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ B ∧ x ∈ B ⟼ C ⁡ z ∈ y
37 35 36 syl ⊢ φ ∧ ¬ z ∈ A → z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ B ∧ x ∈ B ⟼ C ⁡ z ∈ y
38 5 fmpttd ⊢ φ → x ∈ B ⟼ D : B ⟶ ℝ
39 38 ffnd ⊢ φ → x ∈ B ⟼ D Fn B
40 39 adantr ⊢ φ ∧ ¬ z ∈ A → x ∈ B ⟼ D Fn B
41 elpreima ⊢ x ∈ B ⟼ D Fn B → z ∈ x ∈ B ⟼ D -1 y ↔ z ∈ B ∧ x ∈ B ⟼ D ⁡ z ∈ y
42 40 41 syl ⊢ φ ∧ ¬ z ∈ A → z ∈ x ∈ B ⟼ D -1 y ↔ z ∈ B ∧ x ∈ B ⟼ D ⁡ z ∈ y
43 32 37 42 3bitr4d ⊢ φ ∧ ¬ z ∈ A → z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ x ∈ B ⟼ D -1 y
44 43 ex ⊢ φ → ¬ z ∈ A → z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ x ∈ B ⟼ D -1 y
45 44 con1d ⊢ φ → ¬ z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ x ∈ B ⟼ D -1 y → z ∈ A
46 45 abssdv ⊢ φ → z | ¬ z ∈ x ∈ B ⟼ C -1 y ↔ z ∈ x ∈ B ⟼ D -1 y ⊆ A
47 6 46 eqsstrid ⊢ φ → x ∈ B ⟼ C -1 y ∆ x ∈ B ⟼ D -1 y ⊆ A
48 47 difsymssdifssd ⊢ φ → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ⊆ A
49 48 1 sstrd ⊢ φ → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ⊆ ℝ
50 ovolssnul ⊢ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ⊆ A ∧ A ⊆ ℝ ∧ vol * ⁡ A = 0 → vol * ⁡ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y = 0
51 48 1 2 50 syl3anc ⊢ φ → vol * ⁡ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y = 0
52 nulmbl ⊢ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ⊆ ℝ ∧ vol * ⁡ x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y = 0 → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol
53 49 51 52 syl2anc ⊢ φ → x ∈ B ⟼ C -1 y ∖ x ∈ B ⟼ D -1 y ∈ dom ⁡ vol