mbfeqalem2

Description: Lemma for mbfeqa . (Contributed by Mario Carneiro, 2-Sep-2014) (Proof shortened 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	mbfeqalem2	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow (x \in B ⟼ D) \in MblFn)$

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		inundif	$⊢ ({(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y]) \cup ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y]) = {(x \in B ⟼ D)}^{-1} [y]$
7		incom	$⊢ {(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y] = {(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y]$
8		dfin4	$⊢ {(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y] = {(x \in B ⟼ C)}^{-1} [y] ∖ ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y])$
9	7 8	eqtri	$⊢ {(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y] = {(x \in B ⟼ C)}^{-1} [y] ∖ ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y])$
10		id	$⊢ {(x \in B ⟼ C)}^{-1} [y] \in dom vol \to {(x \in B ⟼ C)}^{-1} [y] \in dom vol$
11	1 2 3 4 5	mbfeqalem1	$⊢ φ \to {(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y] \in dom vol$
12		difmbl	$⊢ ({(x \in B ⟼ C)}^{-1} [y] \in dom vol \land {(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ C)}^{-1} [y] ∖ ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y]) \in dom vol$
13	10 11 12	syl2anr	$⊢ (φ \land {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ C)}^{-1} [y] ∖ ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y]) \in dom vol$
14	9 13	eqeltrid	$⊢ (φ \land {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y] \in dom vol$
15	3	eqcomd	$⊢ (φ \land x \in (B ∖ A)) \to D = C$
16	1 2 15 5 4	mbfeqalem1	$⊢ φ \to {(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y] \in dom vol$
17	16	adantr	$⊢ (φ \land {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y] \in dom vol$
18		unmbl	$⊢ ({(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y] \in dom vol \land {(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to ({(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y]) \cup ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y]) \in dom vol$
19	14 17 18	syl2anc	$⊢ (φ \land {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to ({(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y]) \cup ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y]) \in dom vol$
20	6 19	eqeltrrid	$⊢ (φ \land {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ D)}^{-1} [y] \in dom vol$
21		inundif	$⊢ ({(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y]) \cup ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y]) = {(x \in B ⟼ C)}^{-1} [y]$
22		incom	$⊢ {(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y] = {(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y]$
23		dfin4	$⊢ {(x \in B ⟼ D)}^{-1} [y] \cap {(x \in B ⟼ C)}^{-1} [y] = {(x \in B ⟼ D)}^{-1} [y] ∖ ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y])$
24	22 23	eqtri	$⊢ {(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y] = {(x \in B ⟼ D)}^{-1} [y] ∖ ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y])$
25		id	$⊢ {(x \in B ⟼ D)}^{-1} [y] \in dom vol \to {(x \in B ⟼ D)}^{-1} [y] \in dom vol$
26		difmbl	$⊢ ({(x \in B ⟼ D)}^{-1} [y] \in dom vol \land {(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ D)}^{-1} [y] ∖ ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y]) \in dom vol$
27	25 16 26	syl2anr	$⊢ (φ \land {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ D)}^{-1} [y] ∖ ({(x \in B ⟼ D)}^{-1} [y] ∖ {(x \in B ⟼ C)}^{-1} [y]) \in dom vol$
28	24 27	eqeltrid	$⊢ (φ \land {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y] \in dom vol$
29	11	adantr	$⊢ (φ \land {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y] \in dom vol$
30		unmbl	$⊢ ({(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y] \in dom vol \land {(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to ({(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y]) \cup ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y]) \in dom vol$
31	28 29 30	syl2anc	$⊢ (φ \land {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to ({(x \in B ⟼ C)}^{-1} [y] \cap {(x \in B ⟼ D)}^{-1} [y]) \cup ({(x \in B ⟼ C)}^{-1} [y] ∖ {(x \in B ⟼ D)}^{-1} [y]) \in dom vol$
32	21 31	eqeltrrid	$⊢ (φ \land {(x \in B ⟼ D)}^{-1} [y] \in dom vol) \to {(x \in B ⟼ C)}^{-1} [y] \in dom vol$
33	20 32	impbida	$⊢ φ \to ({(x \in B ⟼ C)}^{-1} [y] \in dom vol \leftrightarrow {(x \in B ⟼ D)}^{-1} [y] \in dom vol)$
34	33	ralbidv	$⊢ φ \to (\forall y \in ran (.) {(x \in B ⟼ C)}^{-1} [y] \in dom vol \leftrightarrow \forall y \in ran (.) {(x \in B ⟼ D)}^{-1} [y] \in dom vol)$
35	4	fmpttd	$⊢ φ \to (x \in B ⟼ C) : B ⟶ ℝ$
36		ismbf	$⊢ (x \in B ⟼ C) : B ⟶ ℝ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow \forall y \in ran (.) {(x \in B ⟼ C)}^{-1} [y] \in dom vol)$
37	35 36	syl	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow \forall y \in ran (.) {(x \in B ⟼ C)}^{-1} [y] \in dom vol)$
38	5	fmpttd	$⊢ φ \to (x \in B ⟼ D) : B ⟶ ℝ$
39		ismbf	$⊢ (x \in B ⟼ D) : B ⟶ ℝ \to ((x \in B ⟼ D) \in MblFn \leftrightarrow \forall y \in ran (.) {(x \in B ⟼ D)}^{-1} [y] \in dom vol)$
40	38 39	syl	$⊢ φ \to ((x \in B ⟼ D) \in MblFn \leftrightarrow \forall y \in ran (.) {(x \in B ⟼ D)}^{-1} [y] \in dom vol)$
41	34 37 40	3bitr4d	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow (x \in B ⟼ D) \in MblFn)$

Metamath Proof Explorer

Theorem mbfeqalem2

Proof