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 ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G

Proof

Step Hyp Ref Expression
1 simpr ⊢ B ∈ V ∧ X ∈ B → X ∈ B
2 simpr ⊢ G Fn B ∧ G ⁡ X ≠ ∅ → G ⁡ X ≠ ∅
3 1 2 anim12i ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → X ∈ B ∧ G ⁡ X ≠ ∅
4 simprl ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → G Fn B
5 simpll ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → B ∈ V
6 0ex ⊢ ∅ ∈ V
7 6 a1i ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → ∅ ∈ V
8 elsuppfn ⊢ G Fn B ∧ B ∈ V ∧ ∅ ∈ V → X ∈ supp ∅⁡ G ↔ X ∈ B ∧ G ⁡ X ≠ ∅
9 4 5 7 8 syl3anc ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G ↔ X ∈ B ∧ G ⁡ X ≠ ∅
10 3 9 mpbird ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G