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

Metamath Proof Explorer

Theorem indsn

Description: The indicator function of a singleton. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Assertion indsn 
|- ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( O e. V /\ X e. O ) -> X e. O )
2 1 snssd 
 |-  ( ( O e. V /\ X e. O ) -> { X } C_ O )
3 indval 
 |-  ( ( O e. V /\ { X } C_ O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) )
4 2 3 syldan 
 |-  ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) )
5 velsn 
 |-  ( x e. { X } <-> x = X )
6 5 a1i 
 |-  ( ( O e. V /\ X e. O ) -> ( x e. { X } <-> x = X ) )
7 6 ifbid 
 |-  ( ( O e. V /\ X e. O ) -> if ( x e. { X } , 1 , 0 ) = if ( x = X , 1 , 0 ) )
8 7 mpteq2dv 
 |-  ( ( O e. V /\ X e. O ) -> ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )
9 4 8 eqtrd 
 |-  ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )