# Metamath Proof Explorer

## Theorem pw2f1o

Description: The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of TakeutiZaring p. 96. (Contributed by Mario Carneiro, 6-Oct-2014)

Ref Expression
Hypotheses pw2f1o.1 $⊢ φ → A ∈ V$
pw2f1o.2 $⊢ φ → B ∈ W$
pw2f1o.3 $⊢ φ → C ∈ W$
pw2f1o.4 $⊢ φ → B ≠ C$
pw2f1o.5 $⊢ F = x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x C B$
Assertion pw2f1o $⊢ φ → F : 𝒫 A ⟶ 1-1 onto B C A$

### Proof

Step Hyp Ref Expression
1 pw2f1o.1 $⊢ φ → A ∈ V$
2 pw2f1o.2 $⊢ φ → B ∈ W$
3 pw2f1o.3 $⊢ φ → C ∈ W$
4 pw2f1o.4 $⊢ φ → B ≠ C$
5 pw2f1o.5 $⊢ F = x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x C B$
6 eqid $⊢ z ∈ A ⟼ if z ∈ x C B = z ∈ A ⟼ if z ∈ x C B$
7 1 2 3 4 pw2f1olem $⊢ φ → x ∈ 𝒫 A ∧ z ∈ A ⟼ if z ∈ x C B = z ∈ A ⟼ if z ∈ x C B ↔ z ∈ A ⟼ if z ∈ x C B ∈ B C A ∧ x = z ∈ A ⟼ if z ∈ x C B -1 C$
8 7 biimpa $⊢ φ ∧ x ∈ 𝒫 A ∧ z ∈ A ⟼ if z ∈ x C B = z ∈ A ⟼ if z ∈ x C B → z ∈ A ⟼ if z ∈ x C B ∈ B C A ∧ x = z ∈ A ⟼ if z ∈ x C B -1 C$
9 6 8 mpanr2 $⊢ φ ∧ x ∈ 𝒫 A → z ∈ A ⟼ if z ∈ x C B ∈ B C A ∧ x = z ∈ A ⟼ if z ∈ x C B -1 C$
10 9 simpld $⊢ φ ∧ x ∈ 𝒫 A → z ∈ A ⟼ if z ∈ x C B ∈ B C A$
11 vex $⊢ y ∈ V$
12 11 cnvex $⊢ y -1 ∈ V$
13 12 imaex $⊢ y -1 C ∈ V$
14 13 a1i $⊢ φ ∧ y ∈ B C A → y -1 C ∈ V$
15 1 2 3 4 pw2f1olem $⊢ φ → x ∈ 𝒫 A ∧ y = z ∈ A ⟼ if z ∈ x C B ↔ y ∈ B C A ∧ x = y -1 C$
16 5 10 14 15 f1od $⊢ φ → F : 𝒫 A ⟶ 1-1 onto B C A$