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 ( 𝜑𝐹 Fn 𝐴 )
elsuppfnd.2 ( 𝜑𝐴𝑉 )
elsuppfnd.3 ( 𝜑𝑍𝑊 )
elsuppfnd.4 ( 𝜑𝑋𝐴 )
elsuppfnd.5 ( 𝜑 → ( 𝐹𝑋 ) ≠ 𝑍 )
Assertion elsuppfnd ( 𝜑𝑋 ∈ ( 𝐹 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 elsuppfnd.1 ( 𝜑𝐹 Fn 𝐴 )
2 elsuppfnd.2 ( 𝜑𝐴𝑉 )
3 elsuppfnd.3 ( 𝜑𝑍𝑊 )
4 elsuppfnd.4 ( 𝜑𝑋𝐴 )
5 elsuppfnd.5 ( 𝜑 → ( 𝐹𝑋 ) ≠ 𝑍 )
6 elsuppfn ( ( 𝐹 Fn 𝐴𝐴𝑉𝑍𝑊 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋𝐴 ∧ ( 𝐹𝑋 ) ≠ 𝑍 ) ) )
7 6 biimpar ( ( ( 𝐹 Fn 𝐴𝐴𝑉𝑍𝑊 ) ∧ ( 𝑋𝐴 ∧ ( 𝐹𝑋 ) ≠ 𝑍 ) ) → 𝑋 ∈ ( 𝐹 supp 𝑍 ) )
8 1 2 3 4 5 7 syl32anc ( 𝜑𝑋 ∈ ( 𝐹 supp 𝑍 ) )