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