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

Metamath Proof Explorer

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 )