Theorem indfval

Description: Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	3adant3	$$⊢\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\to {𝟙}_O\left(A\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$
3		simpr	$$⊢\left(\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\wedge x=X\right)\to x=X$$
4	3	eleq1d	$$⊢\left(\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\wedge x=X\right)\to \left(x\in A\leftrightarrow X\in A\right)$$
5	4	ifbid	$$⊢\left(\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\wedge x=X\right)\to if\left(x\in A,1,0\right)=if\left(X\in A,1,0\right)$$
6		simp3	$$⊢\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\to X\in O$$
7		1re	$$⊢1\in ℝ$$
8		0re	$$⊢0\in ℝ$$
9	7 8	ifcli	$$⊢if\left(X\in A,1,0\right)\in ℝ$$
10	9	a1i	$$⊢\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\to if\left(X\in A,1,0\right)\in ℝ$$
11	2 5 6 10	fvmptd	$$⊢\left(O\in V\wedge A\subseteq O\wedge X\in O\right)\to {𝟙}_O\left(A\right)\left(X\right)=if\left(X\in A,1,0\right)$$