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 ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝑉 )
2 0red ⊢ ( 𝑂 ∈ 𝑉 → 0 ∈ ℝ )
3 1red ⊢ ( 𝑂 ∈ 𝑉 → 1 ∈ ℝ )
4 0ne1 ⊢ 0 ≠ 1
5 4 a1i ⊢ ( 𝑂 ∈ 𝑉 → 0 ≠ 1 )
6 eqid ⊢ ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) )
7 1 2 3 5 6 pw2f1o ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) )
8 indv ⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
9 f1oeq1 ⊢ ( ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) → ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ↔ ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ) )
10 8 9 syl ⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ↔ ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ) )
11 7 10 mpbird ⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) )