# 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 ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to {X}\in {supp}_{\varnothing }\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({B}\in {V}\wedge {X}\in {B}\right)\to {X}\in {B}$
2 simpr ${⊢}\left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\to {G}\left({X}\right)\ne \varnothing$
3 1 2 anim12i ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to \left({X}\in {B}\wedge {G}\left({X}\right)\ne \varnothing \right)$
4 simprl ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to {G}Fn{B}$
5 simpll ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to {B}\in {V}$
6 0ex ${⊢}\varnothing \in \mathrm{V}$
7 6 a1i ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to \varnothing \in \mathrm{V}$
8 elsuppfn ${⊢}\left({G}Fn{B}\wedge {B}\in {V}\wedge \varnothing \in \mathrm{V}\right)\to \left({X}\in {supp}_{\varnothing }\left({G}\right)↔\left({X}\in {B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)$
9 4 5 7 8 syl3anc ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to \left({X}\in {supp}_{\varnothing }\left({G}\right)↔\left({X}\in {B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)$
10 3 9 mpbird ${⊢}\left(\left({B}\in {V}\wedge {X}\in {B}\right)\wedge \left({G}Fn{B}\wedge {G}\left({X}\right)\ne \varnothing \right)\right)\to {X}\in {supp}_{\varnothing }\left({G}\right)$