This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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