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 f1oeq1 ⊢ 𝟙 O = a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 → 𝟙 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 8 9 syl ⊢ 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
11 7 10 mpbird ⊢ O ∈ V → 𝟙 O : 𝒫 O ⟶ 1-1 onto 0 1 O