Theorem indf

Description: An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017)

	Ref	Expression
Assertion	indf	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right):O⟶\left\{0,1\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		1re	$$⊢1\in ℝ$$
3		0re	$$⊢0\in ℝ$$
4		ifpr	$$⊢\left(1\in ℝ\wedge 0\in ℝ\right)\to if\left(x\in A,1,0\right)\in \left\{1,0\right\}$$
5	2 3 4	mp2an	$$⊢if\left(x\in A,1,0\right)\in \left\{1,0\right\}$$
6		prcom	$$⊢\left\{1,0\right\}=\left\{0,1\right\}$$
7	5 6	eleqtri	$$⊢if\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
8	7	a1i	$$⊢\left(\left(O\in V\wedge A\subseteq O\right)\wedge x\in O\right)\to if\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
9	1 8	fmpt3d	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right):O⟶\left\{0,1\right\}$$