This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∅ ) ) )