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

Metamath Proof Explorer

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	$⊢ F = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])$
	Assertion	pw2f1o2	$⊢ A \in V \to F : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		pw2f1o2.f	$⊢ F = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])$
2	1	pw2f1ocnv	$⊢ A \in V \to (F : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A \land F^{-1} = (y \in 𝒫 A ⟼ (z \in A ⟼ if (z \in y, 1_{𝑜}, \emptyset))))$
3	2	simpld	$⊢ A \in V \to F : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A$