Theorem indfsid

Description: Conditions for a function to be an indicator function. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	indfsid.1	|- ( ph -> O e. V )
	indfsid.2	|- ( ph -> F : O --> { 0 , 1 } )
Assertion	indfsid	|- ( ph -> F = ( ( _Ind ` O ) ` ( F supp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		indfsid.1	|- ( ph -> O e. V )
2		indfsid.2	|- ( ph -> F : O --> { 0 , 1 } )
3		indpreima	|- ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F = ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) )
4	1 2 3	syl2anc	|- ( ph -> F = ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) )
5		c0ex	|- 0 e. _V
6	5	a1i	|- ( ph -> 0 e. _V )
7		fsuppeq	|- ( ( O e. V /\ 0 e. _V ) -> ( F : O --> { 0 , 1 } -> ( F supp 0 ) = ( `' F " ( { 0 , 1 } \ { 0 } ) ) ) )
8	7	imp	|- ( ( ( O e. V /\ 0 e. _V ) /\ F : O --> { 0 , 1 } ) -> ( F supp 0 ) = ( `' F " ( { 0 , 1 } \ { 0 } ) ) )
9	1 6 2 8	syl21anc	|- ( ph -> ( F supp 0 ) = ( `' F " ( { 0 , 1 } \ { 0 } ) ) )
10		0ne1	|- 0 =/= 1
11		difprsn1	|- ( 0 =/= 1 -> ( { 0 , 1 } \ { 0 } ) = { 1 } )
12	10 11	mp1i	|- ( ph -> ( { 0 , 1 } \ { 0 } ) = { 1 } )
13	12	imaeq2d	|- ( ph -> ( `' F " ( { 0 , 1 } \ { 0 } ) ) = ( `' F " { 1 } ) )
14	9 13	eqtrd	|- ( ph -> ( F supp 0 ) = ( `' F " { 1 } ) )
15	14	fveq2d	|- ( ph -> ( ( _Ind ` O ) ` ( F supp 0 ) ) = ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) )
16	4 15	eqtr4d	|- ( ph -> F = ( ( _Ind ` O ) ` ( F supp 0 ) ) )