Theorem pw2f1o2

Description: Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en , which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypothesis	pw2f1o2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
Assertion	pw2f1o2	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pw2f1o2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
2	1	pw2f1ocnv	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑦 , 1o , ∅ ) ) ) ) )
3	2	simpld	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 )