mbfeqalem1

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

	Ref	Expression
Hypotheses	mbfeqa.1	$⊢ φ \to A \subseteq ℝ$
	mbfeqa.2	$⊢ φ \to {vol}^{*} (A) = 0$
	mbfeqa.3	$⊢ (φ \land x \in (B ∖ A)) \to C = D$
	mbfeqalem.4	$⊢ (φ \land x \in B) \to C \in ℝ$
	mbfeqalem.5	$⊢ (φ \land x \in B) \to D \in ℝ$
Assertion	mbfeqalem1	$⊢ φ \to {(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y] \in dom vol$

Proof

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

Metamath Proof Explorer

Theorem mbfeqalem1

Proof