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

Proof

Step Hyp Ref Expression
1 fvn0elsupp ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B ∧ G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G
2 1 exp43 ⊢ B ∈ V → X ∈ B → G Fn B → G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G
3 2 3imp ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → G ⁡ X ≠ ∅ → X ∈ supp ∅⁡ G
4 simp3 ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → G Fn B
5 simp1 ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → B ∈ V
6 0ex ⊢ ∅ ∈ V
7 6 a1i ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → ∅ ∈ 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 → X ∈ supp ∅⁡ G ↔ X ∈ B ∧ G ⁡ X ≠ ∅
10 simpr ⊢ X ∈ B ∧ G ⁡ X ≠ ∅ → G ⁡ X ≠ ∅
11 9 10 biimtrdi ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → X ∈ supp ∅⁡ G → G ⁡ X ≠ ∅
12 3 11 impbid ⊢ B ∈ V ∧ X ∈ B ∧ G Fn B → G ⁡ X ≠ ∅ ↔ X ∈ supp ∅⁡ G