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