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 | |
|
pw2f1o.2 | |
||
pw2f1o.3 | |
||
pw2f1o.4 | |
||
pw2f1o.5 | |
||
Assertion | pw2f1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw2f1o.1 | |
|
2 | pw2f1o.2 | |
|
3 | pw2f1o.3 | |
|
4 | pw2f1o.4 | |
|
5 | pw2f1o.5 | |
|
6 | eqid | |
|
7 | 1 2 3 4 | pw2f1olem | |
8 | 7 | biimpa | |
9 | 6 8 | mpanr2 | |
10 | 9 | simpld | |
11 | vex | |
|
12 | 11 | cnvex | |
13 | 12 | imaex | |
14 | 13 | a1i | |
15 | 1 2 3 4 | pw2f1olem | |
16 | 5 10 14 15 | f1od | |