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

Metamath Proof Explorer

Definition df-ind

Description: Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017)

Ref Expression
Assertion df-ind 
|- _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cind 
 |-  _Ind
1 vo 
 |-  o
2 cvv 
 |-  _V
3 va 
 |-  a
4 1 cv 
 |-  o
5 4 cpw 
 |-  ~P o
6 vx 
 |-  x
7 6 cv 
 |-  x
8 3 cv 
 |-  a
9 7 8 wcel 
 |-  x e. a
10 c1 
 |-  1
11 cc0 
 |-  0
12 9 10 11 cif 
 |-  if ( x e. a , 1 , 0 )
13 6 4 12 cmpt 
 |-  ( x e. o |-> if ( x e. a , 1 , 0 ) )
14 3 5 13 cmpt 
 |-  ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) )
15 1 2 14 cmpt 
 |-  ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
16 0 15 wceq 
 |-  _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )