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	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → 𝑋 ∈ ( 𝐺 supp ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
2		simpr	⊢ ( ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) → ( 𝐺 ‘ 𝑋 ) ≠ ∅ )
3	1 2	anim12i	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) )
4		simprl	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → 𝐺 Fn 𝐵 )
5		simpll	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → 𝐵 ∈ 𝑉 )
6		0ex	⊢ ∅ ∈ V
7	6	a1i	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → ∅ ∈ V )
8		elsuppfn	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
9	4 5 7 8	syl3anc	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
10	3 9	mpbird	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → 𝑋 ∈ ( 𝐺 supp ∅ ) )