Theorem indval

Description: Value of the indicator function generator for a set A and a domain O . (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Assertion	indval	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		indv	$$⊢O\in V\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$
2	1	adantr	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$
3		eleq2	$$⊢a=A\to \left(x\in a\leftrightarrow x\in A\right)$$
4	3	ifbid	$$⊢a=A\to if\left(x\in a,1,0\right)=if\left(x\in A,1,0\right)$$
5	4	mpteq2dv	$$⊢a=A\to \left(x\in O⟼if\left(x\in a,1,0\right)\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$
6	5	adantl	$$⊢\left(\left(O\in V\wedge A\subseteq O\right)\wedge a=A\right)\to \left(x\in O⟼if\left(x\in a,1,0\right)\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$
7		ssexg	$$⊢\left(A\subseteq O\wedge O\in V\right)\to A\in \mathrm{V}$$
8	7	ancoms	$$⊢\left(O\in V\wedge A\subseteq O\right)\to A\in \mathrm{V}$$
9		simpr	$$⊢\left(O\in V\wedge A\subseteq O\right)\to A\subseteq O$$
10	8 9	elpwd	$$⊢\left(O\in V\wedge A\subseteq O\right)\to A\in 𝒫O$$
11		mptexg	$$⊢O\in V\to \left(x\in O⟼if\left(x\in A,1,0\right)\right)\in \mathrm{V}$$
12	11	adantr	$$⊢\left(O\in V\wedge A\subseteq O\right)\to \left(x\in O⟼if\left(x\in A,1,0\right)\right)\in \mathrm{V}$$
13	2 6 10 12	fvmptd	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$