Metamath Proof Explorer


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 = x 2 𝑜 A x -1 1 𝑜
Assertion pw2f1o2 A V F : 2 𝑜 A 1-1 onto 𝒫 A

Proof

Step Hyp Ref Expression
1 pw2f1o2.f F = x 2 𝑜 A x -1 1 𝑜
2 1 pw2f1ocnv A V F : 2 𝑜 A 1-1 onto 𝒫 A F -1 = y 𝒫 A z A if z y 1 𝑜
3 2 simpld A V F : 2 𝑜 A 1-1 onto 𝒫 A