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