This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suppval

Description: The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019) (Revised by AV, 6-Apr-2019)

Ref Expression
Assertion suppval 
|- ( ( X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } )

Proof

Step Hyp Ref Expression
1 df-supp 
 |-  supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
2 1 a1i 
 |-  ( ( X e. V /\ Z e. W ) -> supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } ) )
3 dmeq 
 |-  ( x = X -> dom x = dom X )
4 3 adantr 
 |-  ( ( x = X /\ z = Z ) -> dom x = dom X )
5 imaeq1 
 |-  ( x = X -> ( x " { i } ) = ( X " { i } ) )
6 5 adantr 
 |-  ( ( x = X /\ z = Z ) -> ( x " { i } ) = ( X " { i } ) )
7 sneq 
 |-  ( z = Z -> { z } = { Z } )
8 7 adantl 
 |-  ( ( x = X /\ z = Z ) -> { z } = { Z } )
9 6 8 neeq12d 
 |-  ( ( x = X /\ z = Z ) -> ( ( x " { i } ) =/= { z } <-> ( X " { i } ) =/= { Z } ) )
10 4 9 rabeqbidv 
 |-  ( ( x = X /\ z = Z ) -> { i e. dom x | ( x " { i } ) =/= { z } } = { i e. dom X | ( X " { i } ) =/= { Z } } )
11 10 adantl 
 |-  ( ( ( X e. V /\ Z e. W ) /\ ( x = X /\ z = Z ) ) -> { i e. dom x | ( x " { i } ) =/= { z } } = { i e. dom X | ( X " { i } ) =/= { Z } } )
12 elex 
 |-  ( X e. V -> X e. _V )
13 12 adantr 
 |-  ( ( X e. V /\ Z e. W ) -> X e. _V )
14 elex 
 |-  ( Z e. W -> Z e. _V )
15 14 adantl 
 |-  ( ( X e. V /\ Z e. W ) -> Z e. _V )
16 dmexg 
 |-  ( X e. V -> dom X e. _V )
17 16 adantr 
 |-  ( ( X e. V /\ Z e. W ) -> dom X e. _V )
18 rabexg 
 |-  ( dom X e. _V -> { i e. dom X | ( X " { i } ) =/= { Z } } e. _V )
19 17 18 syl 
 |-  ( ( X e. V /\ Z e. W ) -> { i e. dom X | ( X " { i } ) =/= { Z } } e. _V )
20 2 11 13 15 19 ovmpod 
 |-  ( ( X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } )