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 
|- ( 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 mbfeqalem1 
|- ( ph -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol )

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 dfsymdif4 
 |-  ( ( `' ( x e. B |-> C ) " y ) /_\ ( `' ( x e. B |-> D ) " y ) ) = { z | -. ( z e. ( `' ( x e. B |-> C ) " y ) <-> z e. ( `' ( x e. B |-> D ) " y ) ) }
7 eldif 
 |-  ( z e. ( B \ A ) <-> ( z e. B /\ -. z e. A ) )
8 eldifi 
 |-  ( x e. ( B \ A ) -> x e. B )
9 8 4 sylan2 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C e. RR )
10 eqid 
 |-  ( x e. B |-> C ) = ( x e. B |-> C )
11 10 fvmpt2 
 |-  ( ( x e. B /\ C e. RR ) -> ( ( x e. B |-> C ) ` x ) = C )
12 8 9 11 syl2an2 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( ( x e. B |-> C ) ` x ) = C )
13 8 5 sylan2 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> D e. RR )
14 eqid 
 |-  ( x e. B |-> D ) = ( x e. B |-> D )
15 14 fvmpt2 
 |-  ( ( x e. B /\ D e. RR ) -> ( ( x e. B |-> D ) ` x ) = D )
16 8 13 15 syl2an2 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( ( x e. B |-> D ) ` x ) = D )
17 3 12 16 3eqtr4d 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> D ) ` x ) )
18 17 ralrimiva 
 |-  ( ph -> A. x e. ( B \ A ) ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> D ) ` x ) )
19 nfv 
 |-  F/ z ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> D ) ` x )
20 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> C ) ` z )
21 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> D ) ` z )
22 20 21 nfeq 
 |-  F/ x ( ( x e. B |-> C ) ` z ) = ( ( x e. B |-> D ) ` z )
23 fveq2 
 |-  ( x = z -> ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> C ) ` z ) )
24 fveq2 
 |-  ( x = z -> ( ( x e. B |-> D ) ` x ) = ( ( x e. B |-> D ) ` z ) )
25 23 24 eqeq12d 
 |-  ( x = z -> ( ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> D ) ` x ) <-> ( ( x e. B |-> C ) ` z ) = ( ( x e. B |-> D ) ` z ) ) )
26 19 22 25 cbvralw 
 |-  ( A. x e. ( B \ A ) ( ( x e. B |-> C ) ` x ) = ( ( x e. B |-> D ) ` x ) <-> A. z e. ( B \ A ) ( ( x e. B |-> C ) ` z ) = ( ( x e. B |-> D ) ` z ) )
27 18 26 sylib 
 |-  ( ph -> A. z e. ( B \ A ) ( ( x e. B |-> C ) ` z ) = ( ( x e. B |-> D ) ` z ) )
28 27 r19.21bi 
 |-  ( ( ph /\ z e. ( B \ A ) ) -> ( ( x e. B |-> C ) ` z ) = ( ( x e. B |-> D ) ` z ) )
29 28 eleq1d 
 |-  ( ( ph /\ z e. ( B \ A ) ) -> ( ( ( x e. B |-> C ) ` z ) e. y <-> ( ( x e. B |-> D ) ` z ) e. y ) )
30 7 29 sylan2br 
 |-  ( ( ph /\ ( z e. B /\ -. z e. A ) ) -> ( ( ( x e. B |-> C ) ` z ) e. y <-> ( ( x e. B |-> D ) ` z ) e. y ) )
31 30 anass1rs 
 |-  ( ( ( ph /\ -. z e. A ) /\ z e. B ) -> ( ( ( x e. B |-> C ) ` z ) e. y <-> ( ( x e. B |-> D ) ` z ) e. y ) )
32 31 pm5.32da 
 |-  ( ( ph /\ -. z e. A ) -> ( ( z e. B /\ ( ( x e. B |-> C ) ` z ) e. y ) <-> ( z e. B /\ ( ( x e. B |-> D ) ` z ) e. y ) ) )
33 4 fmpttd 
 |-  ( ph -> ( x e. B |-> C ) : B --> RR )
34 33 ffnd 
 |-  ( ph -> ( x e. B |-> C ) Fn B )
35 34 adantr 
 |-  ( ( ph /\ -. z e. A ) -> ( x e. B |-> C ) Fn B )
36 elpreima 
 |-  ( ( x e. B |-> C ) Fn B -> ( z e. ( `' ( x e. B |-> C ) " y ) <-> ( z e. B /\ ( ( x e. B |-> C ) ` z ) e. y ) ) )
37 35 36 syl 
 |-  ( ( ph /\ -. z e. A ) -> ( z e. ( `' ( x e. B |-> C ) " y ) <-> ( z e. B /\ ( ( x e. B |-> C ) ` z ) e. y ) ) )
38 5 fmpttd 
 |-  ( ph -> ( x e. B |-> D ) : B --> RR )
39 38 ffnd 
 |-  ( ph -> ( x e. B |-> D ) Fn B )
40 39 adantr 
 |-  ( ( ph /\ -. z e. A ) -> ( x e. B |-> D ) Fn B )
41 elpreima 
 |-  ( ( x e. B |-> D ) Fn B -> ( z e. ( `' ( x e. B |-> D ) " y ) <-> ( z e. B /\ ( ( x e. B |-> D ) ` z ) e. y ) ) )
42 40 41 syl 
 |-  ( ( ph /\ -. z e. A ) -> ( z e. ( `' ( x e. B |-> D ) " y ) <-> ( z e. B /\ ( ( x e. B |-> D ) ` z ) e. y ) ) )
43 32 37 42 3bitr4d 
 |-  ( ( ph /\ -. z e. A ) -> ( z e. ( `' ( x e. B |-> C ) " y ) <-> z e. ( `' ( x e. B |-> D ) " y ) ) )
44 43 ex 
 |-  ( ph -> ( -. z e. A -> ( z e. ( `' ( x e. B |-> C ) " y ) <-> z e. ( `' ( x e. B |-> D ) " y ) ) ) )
45 44 con1d 
 |-  ( ph -> ( -. ( z e. ( `' ( x e. B |-> C ) " y ) <-> z e. ( `' ( x e. B |-> D ) " y ) ) -> z e. A ) )
46 45 abssdv 
 |-  ( ph -> { z | -. ( z e. ( `' ( x e. B |-> C ) " y ) <-> z e. ( `' ( x e. B |-> D ) " y ) ) } C_ A )
47 6 46 eqsstrid 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) /_\ ( `' ( x e. B |-> D ) " y ) ) C_ A )
48 47 difsymssdifssd 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) C_ A )
49 48 1 sstrd 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) C_ RR )
50 ovolssnul 
 |-  ( ( ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) = 0 )
51 48 1 2 50 syl3anc 
 |-  ( ph -> ( vol* ` ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) = 0 )
52 nulmbl 
 |-  ( ( ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) C_ RR /\ ( vol* ` ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) ) = 0 ) -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol )
53 49 51 52 syl2anc 
 |-  ( ph -> ( ( `' ( x e. B |-> C ) " y ) \ ( `' ( x e. B |-> D ) " y ) ) e. dom vol )