Theorem pw2f1o2

Description: Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en , which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypothesis	pw2f1o2.f	$$⊢F=\left(x\in \left({2_{𝑜}}^A\right)⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)$$
Assertion	pw2f1o2	$$⊢A\in V\to F:{2_{𝑜}}^A\underset{1-1\; onto}{⟶}𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		pw2f1o2.f	$$⊢F=\left(x\in \left({2_{𝑜}}^A\right)⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)$$
2	1	pw2f1ocnv	$$⊢A\in V\to \left(F:{2_{𝑜}}^A\underset{1-1\; onto}{⟶}𝒫A\wedge F^{-1}=\left(y\in 𝒫A⟼\left(z\in A⟼if\left(z\in y,1_{𝑜},\varnothing \right)\right)\right)\right)$$
3	2	simpld	$$⊢A\in V\to F:{2_{𝑜}}^A\underset{1-1\; onto}{⟶}𝒫A$$