Metamath Proof Explorer

Theorem suppval1

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

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

Proof

Step Hyp Ref Expression
1 suppval 
 |-  ( ( X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } )
2 1 3adant1 
 |-  ( ( Fun X /\ X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } )
3 funfn 
 |-  ( Fun X <-> X Fn dom X )
4 3 biimpi 
 |-  ( Fun X -> X Fn dom X )
5 4 3ad2ant1 
 |-  ( ( Fun X /\ X e. V /\ Z e. W ) -> X Fn dom X )
6 fnsnfv 
 |-  ( ( X Fn dom X /\ i e. dom X ) -> { ( X ` i ) } = ( X " { i } ) )
7 5 6 sylan 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> { ( X ` i ) } = ( X " { i } ) )
8 7 eqcomd 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( X " { i } ) = { ( X ` i ) } )
9 8 neeq1d 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( ( X " { i } ) =/= { Z } <-> { ( X ` i ) } =/= { Z } ) )
10 fvex 
 |-  ( X ` i ) e. _V
11 sneqbg 
 |-  ( ( X ` i ) e. _V -> ( { ( X ` i ) } = { Z } <-> ( X ` i ) = Z ) )
12 10 11 mp1i 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( { ( X ` i ) } = { Z } <-> ( X ` i ) = Z ) )
13 12 necon3bid 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( { ( X ` i ) } =/= { Z } <-> ( X ` i ) =/= Z ) )
14 9 13 bitrd 
 |-  ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( ( X " { i } ) =/= { Z } <-> ( X ` i ) =/= Z ) )
15 14 rabbidva 
 |-  ( ( Fun X /\ X e. V /\ Z e. W ) -> { i e. dom X | ( X " { i } ) =/= { Z } } = { i e. dom X | ( X ` i ) =/= Z } )
16 2 15 eqtrd 
 |-  ( ( Fun X /\ X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X ` i ) =/= Z } )