Theorem mbfeqalem1

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

	Ref	Expression
Hypotheses	mbfeqa.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	mbfeqa.2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	mbfeqa.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
	mbfeqalem.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
	mbfeqalem.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℝ )
Assertion	mbfeqalem1	⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		mbfeqa.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		mbfeqa.2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
3		mbfeqa.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
4		mbfeqalem.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
5		mbfeqalem.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℝ )
6		dfsymdif4	⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) △ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) = { 𝑧 ∣ ¬ ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) }
7		eldif	⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐴 ) )
8		eldifi	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝑥 ∈ 𝐵 )
9	8 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ℝ )
10		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
11	10	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
12	8 9 11	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
13	8 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐷 ∈ ℝ )
14		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐷 )
15	14	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐷 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) = 𝐷 )
16	8 13 15	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) = 𝐷 )
17	3 12 16	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) )
18	17	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) )
19		nfv	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 )
20		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 )
21		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 )
22	20 21	nfeq	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 )
23		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) )
24		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) )
25	23 24	eqeq12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ) )
26	19 22 25	cbvralw	⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ ( 𝐵 ∖ 𝐴 ) ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) )
27	18 26	sylib	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐵 ∖ 𝐴 ) ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) )
28	27	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) )
29	28	eleq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) )
30	7 29	sylan2br	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) )
31	30	anass1rs	⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) )
32	31	pm5.32da	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
33	4	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℝ )
34	33	ffnd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) Fn 𝐵 )
35	34	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) Fn 𝐵 )
36		elpreima	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) Fn 𝐵 → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
37	35 36	syl	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
38	5	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) : 𝐵 ⟶ ℝ )
39	38	ffnd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
40	39	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
41		elpreima	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
42	40 41	syl	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
43	32 37 42	3bitr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) )
44	43	ex	⊢ ( 𝜑 → ( ¬ 𝑧 ∈ 𝐴 → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) )
45	44	con1d	⊢ ( 𝜑 → ( ¬ ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) → 𝑧 ∈ 𝐴 ) )
46	45	abssdv	⊢ ( 𝜑 → { 𝑧 ∣ ¬ ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ↔ 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) } ⊆ 𝐴 )
47	6 46	eqsstrid	⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) △ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ⊆ 𝐴 )
48	47	difsymssdifssd	⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ⊆ 𝐴 )
49	48 1	sstrd	⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ⊆ ℝ )
50		ovolssnul	⊢ ( ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) = 0 )
51	48 1 2 50	syl3anc	⊢ ( 𝜑 → ( vol* ‘ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) = 0 )
52		nulmbl	⊢ ( ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) = 0 ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )
53	49 51 52	syl2anc	⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )