Theorem indsupp

Description: The support of the indicator function. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Assertion	indsupp	|- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( O e. V /\ A C_ O ) -> O e. V )
2		c0ex	|- 0 e. _V
3	2	a1i	|- ( ( O e. V /\ A C_ O ) -> 0 e. _V )
4		indf	|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
5		fsuppeq	|- ( ( O e. V /\ 0 e. _V ) -> ( ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = ( `' ( ( _Ind ` O ) ` A ) " ( { 0 , 1 } \ { 0 } ) ) ) )
6	5	imp	|- ( ( ( O e. V /\ 0 e. _V ) /\ ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = ( `' ( ( _Ind ` O ) ` A ) " ( { 0 , 1 } \ { 0 } ) ) )
7	1 3 4 6	syl21anc	|- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = ( `' ( ( _Ind ` O ) ` A ) " ( { 0 , 1 } \ { 0 } ) ) )
8		prcom	|- { 0 , 1 } = { 1 , 0 }
9	8	difeq1i	|- ( { 0 , 1 } \ { 0 } ) = ( { 1 , 0 } \ { 0 } )
10		ax-1ne0	|- 1 =/= 0
11		difprsn2	|- ( 1 =/= 0 -> ( { 1 , 0 } \ { 0 } ) = { 1 } )
12	10 11	ax-mp	|- ( { 1 , 0 } \ { 0 } ) = { 1 }
13	9 12	eqtri	|- ( { 0 , 1 } \ { 0 } ) = { 1 }
14	13	a1i	|- ( ( O e. V /\ A C_ O ) -> ( { 0 , 1 } \ { 0 } ) = { 1 } )
15	14	imaeq2d	|- ( ( O e. V /\ A C_ O ) -> ( `' ( ( _Ind ` O ) ` A ) " ( { 0 , 1 } \ { 0 } ) ) = ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) )
16		indpi1	|- ( ( O e. V /\ A C_ O ) -> ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) = A )
17	7 15 16	3eqtrd	|- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )