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	8	f1oeq1d	⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ↔ ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ) )
10	7 9	mpbird	⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) )