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	$$⊢\neg A\subseteq O\to {𝟙}_O\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		indv	$$⊢O\in \mathrm{V}\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$
2	1	fveq1d	$$⊢O\in \mathrm{V}\to {𝟙}_O\left(A\right)=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\left(A\right)$$
3	2	adantr	$$⊢\left(O\in \mathrm{V}\wedge \neg A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\left(A\right)$$
4		elpwi	$$⊢A\in 𝒫O\to A\subseteq O$$
5	4	con3i	$$⊢\neg A\subseteq O\to \neg A\in 𝒫O$$
6	5	adantl	$$⊢\left(O\in \mathrm{V}\wedge \neg A\subseteq O\right)\to \neg A\in 𝒫O$$
7		eqid	$$⊢\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$
8	7	fvmptndm	$$⊢\neg A\in 𝒫O\to \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\left(A\right)=\varnothing$$
9	6 8	syl	$$⊢\left(O\in \mathrm{V}\wedge \neg A\subseteq O\right)\to \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\left(A\right)=\varnothing$$
10	3 9	eqtrd	$$⊢\left(O\in \mathrm{V}\wedge \neg A\subseteq O\right)\to {𝟙}_O\left(A\right)=\varnothing$$
11	10	ex	$$⊢O\in \mathrm{V}\to \left(\neg A\subseteq O\to {𝟙}_O\left(A\right)=\varnothing \right)$$
12		fv2prc	$$⊢\neg O\in \mathrm{V}\to {𝟙}_O\left(A\right)=\varnothing$$
13	12	a1d	$$⊢\neg O\in \mathrm{V}\to \left(\neg A\subseteq O\to {𝟙}_O\left(A\right)=\varnothing \right)$$
14	11 13	pm2.61i	$$⊢\neg A\subseteq O\to {𝟙}_O\left(A\right)=\varnothing$$