Metamath Proof Explorer


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 V 𝟙 O : 𝒫 O 1-1 onto 0 1 O

Proof

Step Hyp Ref Expression
1 id O V O V
2 0red O V 0
3 1red O V 1
4 0ne1 0 1
5 4 a1i O V 0 1
6 eqid a 𝒫 O x O if x a 1 0 = a 𝒫 O x O if x a 1 0
7 1 2 3 5 6 pw2f1o O V a 𝒫 O x O if x a 1 0 : 𝒫 O 1-1 onto 0 1 O
8 indv O V 𝟙 O = a 𝒫 O x O if x a 1 0
9 8 f1oeq1d O V 𝟙 O : 𝒫 O 1-1 onto 0 1 O a 𝒫 O x O if x a 1 0 : 𝒫 O 1-1 onto 0 1 O
10 7 9 mpbird O V 𝟙 O : 𝒫 O 1-1 onto 0 1 O