Metamath Proof Explorer

Theorem fvn0elsupp

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

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( B e. V /\ X e. B ) -> X e. B )
2 simpr 
 |-  ( ( G Fn B /\ ( G ` X ) =/= (/) ) -> ( G ` X ) =/= (/) )
3 1 2 anim12i 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> ( X e. B /\ ( G ` X ) =/= (/) ) )
4 simprl 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> G Fn B )
5 simpll 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> B e. V )
6 0ex 
 |-  (/) e. _V
7 6 a1i 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> (/) 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 /\ ( G ` X ) =/= (/) ) ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
10 3 9 mpbird 
 |-  ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> X e. ( G supp (/) ) )