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

Proof

Step	Hyp	Ref	Expression
1		fvn0elsupp	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) → 𝑋 ∈ ( 𝐺 supp ∅ ) )
2	1	exp43	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑋 ∈ 𝐵 → ( 𝐺 Fn 𝐵 → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ ( 𝐺 supp ∅ ) ) ) ) )
3	2	3imp	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ ( 𝐺 supp ∅ ) ) )
4		simp3	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → 𝐺 Fn 𝐵 )
5		simp1	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → 𝐵 ∈ 𝑉 )
6		0ex	⊢ ∅ ∈ V
7	6	a1i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → ∅ ∈ V )
8		elsuppfn	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
9	4 5 7 8	syl3anc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
10		simpr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) → ( 𝐺 ‘ 𝑋 ) ≠ ∅ )
11	9 10	biimtrdi	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) → ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) )
12	3 11	impbid	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵 ) → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ ↔ 𝑋 ∈ ( 𝐺 supp ∅ ) ) )