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 ) )