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 
|- ( ph -> A C_ RR )
mbfeqa.2 
|- ( ph -> ( vol* ` A ) = 0 )
mbfeqa.3 
|- ( ( ph /\ x e. ( B \ A ) ) -> C = D )
mbfeqalem.4 
|- ( ( ph /\ x e. B ) -> C e. RR )
mbfeqalem.5 
|- ( ( ph /\ x e. B ) -> D e. RR )
Assertion mbfeqalem2 
|- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )

Proof

Step Hyp Ref Expression
1 mbfeqa.1 
 |-  ( ph -> A C_ RR )
2 mbfeqa.2 
 |-  ( ph -> ( vol* ` A ) = 0 )
3 mbfeqa.3 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = D )
4 mbfeqalem.4 
 |-  ( ( ph /\ x e. B ) -> C e. RR )
5 mbfeqalem.5 
 |-  ( ( ph /\ x e. B ) -> D e. RR )
6 inundif 
 |-  ( ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) u. ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) ) = ( `' ( x e. B |-> D ) " y )
7 incom 
 |-  ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) = ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) )
8 dfin4 
 |-  ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) = ( ( `' ( x e. B |-> C ) " y ) \ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) )
9 7 8 eqtri 
 |-  ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) = ( ( `' ( x e. B |-> C ) " y ) \ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) )
10 id 
 |-  ( ( `' ( x e. B |-> C ) " y ) e. dom vol -> ( `' ( x e. B |-> C ) " y ) e. dom vol )
11 1 2 3 4 5 mbfeqalem1 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol )
12 difmbl 
 |-  ( ( ( `' ( x e. B |-> C ) " y ) e. dom vol /\ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol ) -> ( ( `' ( x e. B |-> C ) " y ) \ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) e. dom vol )
13 10 11 12 syl2anr 
 |-  ( ( ph /\ ( `' ( x e. B |-> C ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> C ) " y ) \ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) e. dom vol )
14 9 13 eqeltrid 
 |-  ( ( ph /\ ( `' ( x e. B |-> C ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) e. dom vol )
15 3 eqcomd 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> D = C )
16 1 2 15 5 4 mbfeqalem1 
 |-  ( ph -> ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) e. dom vol )
17 16 adantr 
 |-  ( ( ph /\ ( `' ( x e. B |-> C ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) e. dom vol )
18 unmbl 
 |-  ( ( ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) e. dom vol /\ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) e. dom vol ) -> ( ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) u. ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) ) e. dom vol )
19 14 17 18 syl2anc 
 |-  ( ( ph /\ ( `' ( x e. B |-> C ) " y ) e. dom vol ) -> ( ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) u. ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) ) e. dom vol )
20 6 19 eqeltrrid 
 |-  ( ( ph /\ ( `' ( x e. B |-> C ) " y ) e. dom vol ) -> ( `' ( x e. B |-> D ) " y ) e. dom vol )
21 inundif 
 |-  ( ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) u. ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) = ( `' ( x e. B |-> C ) " y )
22 incom 
 |-  ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) = ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) )
23 dfin4 
 |-  ( ( `' ( x e. B |-> D ) " y ) i^i ( `' ( x e. B |-> C ) " y ) ) = ( ( `' ( x e. B |-> D ) " y ) \ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) )
24 22 23 eqtri 
 |-  ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) = ( ( `' ( x e. B |-> D ) " y ) \ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) )
25 id 
 |-  ( ( `' ( x e. B |-> D ) " y ) e. dom vol -> ( `' ( x e. B |-> D ) " y ) e. dom vol )
26 difmbl 
 |-  ( ( ( `' ( x e. B |-> D ) " y ) e. dom vol /\ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) e. dom vol ) -> ( ( `' ( x e. B |-> D ) " y ) \ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) ) e. dom vol )
27 25 16 26 syl2anr 
 |-  ( ( ph /\ ( `' ( x e. B |-> D ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> D ) " y ) \ ( ( `' ( x e. B |-> D ) " y ) \ ( `' ( x e. B |-> C ) " y ) ) ) e. dom vol )
28 24 27 eqeltrid 
 |-  ( ( ph /\ ( `' ( x e. B |-> D ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) e. dom vol )
29 11 adantr 
 |-  ( ( ph /\ ( `' ( x e. B |-> D ) " y ) e. dom vol ) -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol )
30 unmbl 
 |-  ( ( ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) e. dom vol /\ ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol ) -> ( ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) u. ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) e. dom vol )
31 28 29 30 syl2anc 
 |-  ( ( ph /\ ( `' ( x e. B |-> D ) " y ) e. dom vol ) -> ( ( ( `' ( x e. B |-> C ) " y ) i^i ( `' ( x e. B |-> D ) " y ) ) u. ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) e. dom vol )
32 21 31 eqeltrrid 
 |-  ( ( ph /\ ( `' ( x e. B |-> D ) " y ) e. dom vol ) -> ( `' ( x e. B |-> C ) " y ) e. dom vol )
33 20 32 impbida 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) e. dom vol <-> ( `' ( x e. B |-> D ) " y ) e. dom vol ) )
34 33 ralbidv 
 |-  ( ph -> ( A. y e. ran (,) ( `' ( x e. B |-> C ) " y ) e. dom vol <-> A. y e. ran (,) ( `' ( x e. B |-> D ) " y ) e. dom vol ) )
35 4 fmpttd 
 |-  ( ph -> ( x e. B |-> C ) : B --> RR )
36 ismbf 
 |-  ( ( x e. B |-> C ) : B --> RR -> ( ( x e. B |-> C ) e. MblFn <-> A. y e. ran (,) ( `' ( x e. B |-> C ) " y ) e. dom vol ) )
37 35 36 syl 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> A. y e. ran (,) ( `' ( x e. B |-> C ) " y ) e. dom vol ) )
38 5 fmpttd 
 |-  ( ph -> ( x e. B |-> D ) : B --> RR )
39 ismbf 
 |-  ( ( x e. B |-> D ) : B --> RR -> ( ( x e. B |-> D ) e. MblFn <-> A. y e. ran (,) ( `' ( x e. B |-> D ) " y ) e. dom vol ) )
40 38 39 syl 
 |-  ( ph -> ( ( x e. B |-> D ) e. MblFn <-> A. y e. ran (,) ( `' ( x e. B |-> D ) " y ) e. dom vol ) )
41 34 37 40 3bitr4d 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )