This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
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 )