Theorem elsuppfnd

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

	Ref	Expression
Hypotheses	elsuppfnd.1	|- ( ph -> F Fn A )
	elsuppfnd.2	|- ( ph -> A e. V )
	elsuppfnd.3	|- ( ph -> Z e. W )
	elsuppfnd.4	|- ( ph -> X e. A )
	elsuppfnd.5	|- ( ph -> ( F ` X ) =/= Z )
Assertion	elsuppfnd	|- ( ph -> X e. ( F supp Z ) )

Proof

Step	Hyp	Ref	Expression
1		elsuppfnd.1	|- ( ph -> F Fn A )
2		elsuppfnd.2	|- ( ph -> A e. V )
3		elsuppfnd.3	|- ( ph -> Z e. W )
4		elsuppfnd.4	|- ( ph -> X e. A )
5		elsuppfnd.5	|- ( ph -> ( F ` X ) =/= Z )
6		elsuppfn	|- ( ( F Fn A /\ A e. V /\ Z e. W ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
7	6	biimpar	|- ( ( ( F Fn A /\ A e. V /\ Z e. W ) /\ ( X e. A /\ ( F ` X ) =/= Z ) ) -> X e. ( F supp Z ) )
8	1 2 3 4 5 7	syl32anc	|- ( ph -> X e. ( F supp Z ) )