Metamath Proof Explorer

Theorem extmptsuppeq

Description: The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 30-Jun-2019)

Ref Expression
Hypotheses extmptsuppeq.b 
|- ( ph -> B e. W )
extmptsuppeq.a 
|- ( ph -> A C_ B )
extmptsuppeq.z 
|- ( ( ph /\ n e. ( B \ A ) ) -> X = Z )
Assertion extmptsuppeq 
|- ( ph -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) )

Proof

Step Hyp Ref Expression
1 extmptsuppeq.b 
 |-  ( ph -> B e. W )
2 extmptsuppeq.a 
 |-  ( ph -> A C_ B )
3 extmptsuppeq.z 
 |-  ( ( ph /\ n e. ( B \ A ) ) -> X = Z )
4 2 adantl 
 |-  ( ( Z e. _V /\ ph ) -> A C_ B )
5 4 sseld 
 |-  ( ( Z e. _V /\ ph ) -> ( n e. A -> n e. B ) )
6 5 anim1d 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. A /\ X e. ( _V \ { Z } ) ) -> ( n e. B /\ X e. ( _V \ { Z } ) ) ) )
7 eldif 
 |-  ( n e. ( B \ A ) <-> ( n e. B /\ -. n e. A ) )
8 3 adantll 
 |-  ( ( ( Z e. _V /\ ph ) /\ n e. ( B \ A ) ) -> X = Z )
9 7 8 sylan2br 
 |-  ( ( ( Z e. _V /\ ph ) /\ ( n e. B /\ -. n e. A ) ) -> X = Z )
10 9 expr 
 |-  ( ( ( Z e. _V /\ ph ) /\ n e. B ) -> ( -. n e. A -> X = Z ) )
11 elsn2g 
 |-  ( Z e. _V -> ( X e. { Z } <-> X = Z ) )
12 elndif 
 |-  ( X e. { Z } -> -. X e. ( _V \ { Z } ) )
13 11 12 syl6bir 
 |-  ( Z e. _V -> ( X = Z -> -. X e. ( _V \ { Z } ) ) )
14 13 ad2antrr 
 |-  ( ( ( Z e. _V /\ ph ) /\ n e. B ) -> ( X = Z -> -. X e. ( _V \ { Z } ) ) )
15 10 14 syld 
 |-  ( ( ( Z e. _V /\ ph ) /\ n e. B ) -> ( -. n e. A -> -. X e. ( _V \ { Z } ) ) )
16 15 con4d 
 |-  ( ( ( Z e. _V /\ ph ) /\ n e. B ) -> ( X e. ( _V \ { Z } ) -> n e. A ) )
17 16 impr 
 |-  ( ( ( Z e. _V /\ ph ) /\ ( n e. B /\ X e. ( _V \ { Z } ) ) ) -> n e. A )
18 simprr 
 |-  ( ( ( Z e. _V /\ ph ) /\ ( n e. B /\ X e. ( _V \ { Z } ) ) ) -> X e. ( _V \ { Z } ) )
19 17 18 jca 
 |-  ( ( ( Z e. _V /\ ph ) /\ ( n e. B /\ X e. ( _V \ { Z } ) ) ) -> ( n e. A /\ X e. ( _V \ { Z } ) ) )
20 19 ex 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. B /\ X e. ( _V \ { Z } ) ) -> ( n e. A /\ X e. ( _V \ { Z } ) ) ) )
21 6 20 impbid 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. A /\ X e. ( _V \ { Z } ) ) <-> ( n e. B /\ X e. ( _V \ { Z } ) ) ) )
22 21 rabbidva2 
 |-  ( ( Z e. _V /\ ph ) -> { n e. A | X e. ( _V \ { Z } ) } = { n e. B | X e. ( _V \ { Z } ) } )
23 eqid 
 |-  ( n e. A |-> X ) = ( n e. A |-> X )
24 1 2 ssexd 
 |-  ( ph -> A e. _V )
25 24 adantl 
 |-  ( ( Z e. _V /\ ph ) -> A e. _V )
26 simpl 
 |-  ( ( Z e. _V /\ ph ) -> Z e. _V )
27 23 25 26 mptsuppdifd 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. A |-> X ) supp Z ) = { n e. A | X e. ( _V \ { Z } ) } )
28 eqid 
 |-  ( n e. B |-> X ) = ( n e. B |-> X )
29 1 adantl 
 |-  ( ( Z e. _V /\ ph ) -> B e. W )
30 28 29 26 mptsuppdifd 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. B |-> X ) supp Z ) = { n e. B | X e. ( _V \ { Z } ) } )
31 22 27 30 3eqtr4d 
 |-  ( ( Z e. _V /\ ph ) -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) )
32 31 ex 
 |-  ( Z e. _V -> ( ph -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) ) )
33 simpr 
 |-  ( ( ( n e. A |-> X ) e. _V /\ Z e. _V ) -> Z e. _V )
34 supp0prc 
 |-  ( -. ( ( n e. A |-> X ) e. _V /\ Z e. _V ) -> ( ( n e. A |-> X ) supp Z ) = (/) )
35 33 34 nsyl5 
 |-  ( -. Z e. _V -> ( ( n e. A |-> X ) supp Z ) = (/) )
36 simpr 
 |-  ( ( ( n e. B |-> X ) e. _V /\ Z e. _V ) -> Z e. _V )
37 supp0prc 
 |-  ( -. ( ( n e. B |-> X ) e. _V /\ Z e. _V ) -> ( ( n e. B |-> X ) supp Z ) = (/) )
38 36 37 nsyl5 
 |-  ( -. Z e. _V -> ( ( n e. B |-> X ) supp Z ) = (/) )
39 35 38 eqtr4d 
 |-  ( -. Z e. _V -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) )
40 39 a1d 
 |-  ( -. Z e. _V -> ( ph -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) ) )
41 32 40 pm2.61i 
 |-  ( ph -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) )