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

Metamath Proof Explorer

Theorem elsuppfnd

Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses elsuppfnd.1 ⊢ φ → F Fn A
elsuppfnd.2 ⊢ φ → A ∈ V
elsuppfnd.3 ⊢ φ → Z ∈ W
elsuppfnd.4 ⊢ φ → X ∈ A
elsuppfnd.5 ⊢ φ → F ⁡ X ≠ Z
Assertion elsuppfnd ⊢ φ → X ∈ supp Z⁡ F

Proof

Step Hyp Ref Expression
1 elsuppfnd.1 ⊢ φ → F Fn A
2 elsuppfnd.2 ⊢ φ → A ∈ V
3 elsuppfnd.3 ⊢ φ → Z ∈ W
4 elsuppfnd.4 ⊢ φ → X ∈ A
5 elsuppfnd.5 ⊢ φ → F ⁡ X ≠ Z
6 elsuppfn ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ W → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ≠ Z
7 6 biimpar ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ W ∧ X ∈ A ∧ F ⁡ X ≠ Z → X ∈ supp Z⁡ F
8 1 2 3 4 5 7 syl32anc ⊢ φ → X ∈ supp Z⁡ F