Theorem indv

Description: Value of the indicator function generator with domain O . (Contributed by Thierry Arnoux, 23-Aug-2017)

	Ref	Expression
Assertion	indv	$$⊢O\in V\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ind	$$⊢𝟙=\left(o\in \mathrm{V}⟼\left(a\in 𝒫o⟼\left(x\in o⟼if\left(x\in a,1,0\right)\right)\right)\right)$$
2		pweq	$$⊢o=O\to 𝒫o=𝒫O$$
3		mpteq1	$$⊢o=O\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)$$
4	2 3	mpteq12dv	$$⊢o=O\to \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)$$
5		elex	$$⊢O\in V\to O\in \mathrm{V}$$
6		pwexg	$$⊢O\in \mathrm{V}\to 𝒫O\in \mathrm{V}$$
7		mptexg	$$⊢𝒫O\in \mathrm{V}\to \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\in \mathrm{V}$$
8	5 6 7	3syl	$$⊢O\in V\to \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)\in \mathrm{V}$$
9	1 4 5 8	fvmptd3	$$⊢O\in V\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$