# 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 ${⊢}{\phi }\to {A}\subseteq ℝ$
mbfeqa.2 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
mbfeqa.3 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to {C}={D}$
mbfeqalem.4 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in ℝ$
mbfeqalem.5 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {D}\in ℝ$
Assertion mbfeqalem1 ${⊢}{\phi }\to {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$

### Proof

Step Hyp Ref Expression
1 mbfeqa.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 mbfeqa.2 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
3 mbfeqa.3 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to {C}={D}$
4 mbfeqalem.4 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in ℝ$
5 mbfeqalem.5 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {D}\in ℝ$
6 dfsymdif4 ${⊢}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]∆{\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)=\left\{{z}|¬\left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔{z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)\right\}$
7 eldif ${⊢}{z}\in \left({B}\setminus {A}\right)↔\left({z}\in {B}\wedge ¬{z}\in {A}\right)$
8 eldifi ${⊢}{x}\in \left({B}\setminus {A}\right)\to {x}\in {B}$
9 8 4 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to {C}\in ℝ$
10 eqid ${⊢}\left({x}\in {B}⟼{C}\right)=\left({x}\in {B}⟼{C}\right)$
11 10 fvmpt2 ${⊢}\left({x}\in {B}\wedge {C}\in ℝ\right)\to \left({x}\in {B}⟼{C}\right)\left({x}\right)={C}$
12 8 9 11 syl2an2 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to \left({x}\in {B}⟼{C}\right)\left({x}\right)={C}$
13 8 5 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to {D}\in ℝ$
14 eqid ${⊢}\left({x}\in {B}⟼{D}\right)=\left({x}\in {B}⟼{D}\right)$
15 14 fvmpt2 ${⊢}\left({x}\in {B}\wedge {D}\in ℝ\right)\to \left({x}\in {B}⟼{D}\right)\left({x}\right)={D}$
16 8 13 15 syl2an2 ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to \left({x}\in {B}⟼{D}\right)\left({x}\right)={D}$
17 3 12 16 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in \left({B}\setminus {A}\right)\right)\to \left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({x}\right)$
18 17 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left({B}\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({x}\right)$
19 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({x}\right)$
20 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({z}\right)$
21 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{D}\right)\left({z}\right)$
22 20 21 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({z}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)$
23 fveq2 ${⊢}{x}={z}\to \left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{C}\right)\left({z}\right)$
24 fveq2 ${⊢}{x}={z}\to \left({x}\in {B}⟼{D}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)$
25 23 24 eqeq12d ${⊢}{x}={z}\to \left(\left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({x}\right)↔\left({x}\in {B}⟼{C}\right)\left({z}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)\right)$
26 19 22 25 cbvralw ${⊢}\forall {x}\in \left({B}\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({x}\right)=\left({x}\in {B}⟼{D}\right)\left({x}\right)↔\forall {z}\in \left({B}\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({z}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)$
27 18 26 sylib ${⊢}{\phi }\to \forall {z}\in \left({B}\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{C}\right)\left({z}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)$
28 27 r19.21bi ${⊢}\left({\phi }\wedge {z}\in \left({B}\setminus {A}\right)\right)\to \left({x}\in {B}⟼{C}\right)\left({z}\right)=\left({x}\in {B}⟼{D}\right)\left({z}\right)$
29 28 eleq1d ${⊢}\left({\phi }\wedge {z}\in \left({B}\setminus {A}\right)\right)\to \left(\left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}↔\left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)$
30 7 29 sylan2br ${⊢}\left({\phi }\wedge \left({z}\in {B}\wedge ¬{z}\in {A}\right)\right)\to \left(\left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}↔\left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)$
31 30 anass1rs ${⊢}\left(\left({\phi }\wedge ¬{z}\in {A}\right)\wedge {z}\in {B}\right)\to \left(\left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}↔\left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)$
32 31 pm5.32da ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left(\left({z}\in {B}\wedge \left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}\right)↔\left({z}\in {B}\wedge \left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)\right)$
33 4 fmpttd ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right):{B}⟶ℝ$
34 33 ffnd ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)Fn{B}$
35 34 adantr ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left({x}\in {B}⟼{C}\right)Fn{B}$
36 elpreima ${⊢}\left({x}\in {B}⟼{C}\right)Fn{B}\to \left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔\left({z}\in {B}\wedge \left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}\right)\right)$
37 35 36 syl ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔\left({z}\in {B}\wedge \left({x}\in {B}⟼{C}\right)\left({z}\right)\in {y}\right)\right)$
38 5 fmpttd ${⊢}{\phi }\to \left({x}\in {B}⟼{D}\right):{B}⟶ℝ$
39 38 ffnd ${⊢}{\phi }\to \left({x}\in {B}⟼{D}\right)Fn{B}$
40 39 adantr ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left({x}\in {B}⟼{D}\right)Fn{B}$
41 elpreima ${⊢}\left({x}\in {B}⟼{D}\right)Fn{B}\to \left({z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]↔\left({z}\in {B}\wedge \left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)\right)$
42 40 41 syl ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left({z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]↔\left({z}\in {B}\wedge \left({x}\in {B}⟼{D}\right)\left({z}\right)\in {y}\right)\right)$
43 32 37 42 3bitr4d ${⊢}\left({\phi }\wedge ¬{z}\in {A}\right)\to \left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔{z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)$
44 43 ex ${⊢}{\phi }\to \left(¬{z}\in {A}\to \left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔{z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)\right)$
45 44 con1d ${⊢}{\phi }\to \left(¬\left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔{z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)\to {z}\in {A}\right)$
46 45 abssdv ${⊢}{\phi }\to \left\{{z}|¬\left({z}\in {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]↔{z}\in {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)\right\}\subseteq {A}$
47 6 46 eqsstrid ${⊢}{\phi }\to \left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]∆{\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)\subseteq {A}$
48 47 difsymssdifssd ${⊢}{\phi }\to {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\subseteq {A}$
49 48 1 sstrd ${⊢}{\phi }\to {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\subseteq ℝ$
50 ovolssnul ${⊢}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\subseteq {A}\wedge {A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)=0\right)\to {vol}^{*}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)=0$
51 48 1 2 50 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)=0$
52 nulmbl ${⊢}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\subseteq ℝ\wedge {vol}^{*}\left({\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\right)=0\right)\to {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
53 49 51 52 syl2anc ${⊢}{\phi }\to {\left({x}\in {B}⟼{C}\right)}^{-1}\left[{y}\right]\setminus {\left({x}\in {B}⟼{D}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$