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 ) = (/) )