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