Theorem indf1o

Description: The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017)

	Ref	Expression
Assertion	indf1o	$$⊢O\in V\to {𝟙}_O:𝒫O\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^O$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢O\in V\to O\in V$$
2		0red	$$⊢O\in V\to 0\in ℝ$$
3		1red	$$⊢O\in V\to 1\in ℝ$$
4		0ne1	$$⊢0\ne 1$$
5	4	a1i	$$⊢O\in V\to 0\ne 1$$
6		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)$$
7	1 2 3 5 6	pw2f1o	$$⊢O\in V\to \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right):𝒫O\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^O$$
8		indv	$$⊢O\in V\to {𝟙}_O=\left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right)$$
9	8	f1oeq1d	$$⊢O\in V\to \left({𝟙}_O:𝒫O\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^O\leftrightarrow \left(a\in 𝒫O⟼\left(x\in O⟼if\left(x\in a,1,0\right)\right)\right):𝒫O\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^O\right)$$
10	7 9	mpbird	$$⊢O\in V\to {𝟙}_O:𝒫O\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^O$$