Metamath Proof Explorer

Theorem fvn0elsuppb

Description: The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020)

Ref Expression
Assertion fvn0elsuppb 
|- ( ( B e. V /\ X e. B /\ G Fn B ) -> ( ( G ` X ) =/= (/) <-> X e. ( G supp (/) ) ) )

Proof

Step Hyp Ref Expression
1 fvn0elsupp 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> X e. ( G supp (/) ) )
2 1 exp43 
 |-  ( B e. V -> ( X e. B -> ( G Fn B -> ( ( G ` X ) =/= (/) -> X e. ( G supp (/) ) ) ) ) )
3 2 3imp 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> ( ( G ` X ) =/= (/) -> X e. ( G supp (/) ) ) )
4 simp3 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> G Fn B )
5 simp1 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> B e. V )
6 0ex 
 |-  (/) e. _V
7 6 a1i 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> (/) e. _V )
8 elsuppfn 
 |-  ( ( G Fn B /\ B e. V /\ (/) e. _V ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
9 4 5 7 8 syl3anc 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
10 simpr 
 |-  ( ( X e. B /\ ( G ` X ) =/= (/) ) -> ( G ` X ) =/= (/) )
11 9 10 biimtrdi 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> ( X e. ( G supp (/) ) -> ( G ` X ) =/= (/) ) )
12 3 11 impbid 
 |-  ( ( B e. V /\ X e. B /\ G Fn B ) -> ( ( G ` X ) =/= (/) <-> X e. ( G supp (/) ) ) )