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

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 ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐺 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 ∅ ) )