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

Metamath Proof Explorer

Theorem suppvalfn

Description: The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 22-Apr-2019)

Ref Expression
Assertion suppvalfn 
|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn X -> Fun F )
2 1 3ad2ant1 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> Fun F )
3 fnex 
 |-  ( ( F Fn X /\ X e. V ) -> F e. _V )
4 3 3adant3 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> F e. _V )
5 simp3 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> Z e. W )
6 suppval1 
 |-  ( ( Fun F /\ F e. _V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
7 2 4 5 6 syl3anc 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
8 fndm 
 |-  ( F Fn X -> dom F = X )
9 8 3ad2ant1 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> dom F = X )
10 9 rabeqdv 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> { i e. dom F | ( F ` i ) =/= Z } = { i e. X | ( F ` i ) =/= Z } )
11 7 10 eqtrd 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )