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

Metamath Proof Explorer

Theorem indval0

Description: The indicator function generator does not generate a (meaningful) indicator function for a class which is not a subset of the domain. (Contributed by AV, 11-Apr-2026)

Ref Expression
Assertion indval0 
|- ( -. A C_ O -> ( ( _Ind ` O ) ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 indv 
 |-  ( O e. _V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
2 1 fveq1d 
 |-  ( O e. _V -> ( ( _Ind ` O ) ` A ) = ( ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) ` A ) )
3 2 adantr 
 |-  ( ( O e. _V /\ -. A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) ` A ) )
4 elpwi 
 |-  ( A e. ~P O -> A C_ O )
5 4 con3i 
 |-  ( -. A C_ O -> -. A e. ~P O )
6 5 adantl 
 |-  ( ( O e. _V /\ -. A C_ O ) -> -. A e. ~P O )
7 eqid 
 |-  ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) )
8 7 fvmptndm 
 |-  ( -. A e. ~P O -> ( ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) ` A ) = (/) )
9 6 8 syl 
 |-  ( ( O e. _V /\ -. A C_ O ) -> ( ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) ` A ) = (/) )
10 3 9 eqtrd 
 |-  ( ( O e. _V /\ -. A C_ O ) -> ( ( _Ind ` O ) ` A ) = (/) )
11 10 ex 
 |-  ( O e. _V -> ( -. A C_ O -> ( ( _Ind ` O ) ` A ) = (/) ) )
12 fv2prc 
 |-  ( -. O e. _V -> ( ( _Ind ` O ) ` A ) = (/) )
13 12 a1d 
 |-  ( -. O e. _V -> ( -. A C_ O -> ( ( _Ind ` O ) ` A ) = (/) ) )
14 11 13 pm2.61i 
 |-  ( -. A C_ O -> ( ( _Ind ` O ) ` A ) = (/) )