Metamath Proof Explorer

Theorem mbfeqalem2

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

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

Proof

Step Hyp Ref Expression
1 mbfeqa.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 mbfeqa.2 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
3 mbfeqa.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
4 mbfeqalem.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
5 mbfeqalem.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℝ )
6 inundif ⊢ ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ) = ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 )
7 incom ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) )
8 dfin4 ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) )
9 7 8 eqtri ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) )
10 id ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol → ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol )
11 1 2 3 4 5 mbfeqalem1 ⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )
12 difmbl ⊢ ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ∧ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) ∈ dom vol )
13 10 11 12 syl2anr ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) ∈ dom vol )
14 9 13 eqeltrid ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol )
15 3 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐷 = 𝐶 )
16 1 2 15 5 4 mbfeqalem1 ⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol )
18 unmbl ⊢ ( ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol ∧ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol ) → ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ) ∈ dom vol )
19 14 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) → ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ) ∈ dom vol )
20 6 19 eqeltrrid ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) → ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol )
21 inundif ⊢ ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) = ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 )
22 incom ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) )
23 dfin4 ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) )
24 22 23 eqtri ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) = ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) )
25 id ⊢ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol → ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol )
26 difmbl ⊢ ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ∧ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ) ∈ dom vol )
27 25 16 26 syl2anr ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ) ) ∈ dom vol )
28 24 27 eqeltrid ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )
29 11 adantr ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol )
30 unmbl ⊢ ( ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol ∧ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∈ dom vol ) → ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) ∈ dom vol )
31 28 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) → ( ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∩ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ∪ ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∖ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ) ) ∈ dom vol )
32 21 31 eqeltrrid ⊢ ( ( 𝜑 ∧ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) → ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol )
33 20 32 impbida ⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ↔ ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) )
34 33 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) )
35 4 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℝ )
36 ismbf ⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℝ → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) )
37 35 36 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) “ 𝑦 ) ∈ dom vol ) )
38 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) : 𝐵 ⟶ ℝ )
39 ismbf ⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) : 𝐵 ⟶ ℝ → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) )
40 38 39 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) “ 𝑦 ) ∈ dom vol ) )
41 34 37 40 3bitr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ) )