Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem pw2en 4426

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. (This proof seems excessively long. An attempt to find a shorter one is on my to-do list.)

Hypothesis

Ref	Expression
pw2en.1

Assertion

Ref	Expression
pw2en

---

Proof of Theorem pw2en

Step	Hyp	Ref	Expression
1		pw2en.1	. . 3
2	1	pwex 2735	. 2
3	1	opabex2 3596	. . 3
4	3	a1i 8	. 2
5		visset 1804	. . . . 5
6	5	cnvex 3506	. . . 4
7		imaexg 3400	. . . 4
8	6, 7	ax-mp 7	. . 3
9	8	a1i 8	. 2
10		sseqin2 2219	. . . . . . . . 9
11	10	biimp 151	. . . . . . . 8
12	11	eqeq1d 1475	. . . . . . 7
13		eleq2 1527	. . . . . . . . . 10
14		p0ex 2760	. . . . . . . . . . . 12
15		visset 1804	. . . . . . . . . . . 12
16	14, 15	elimasn 3410	. . . . . . . . . . 11
17	14, 15	opelcnv 3287	. . . . . . . . . . 11
18	16, 17	bitr 173	. . . . . . . . . 10
19	13, 18	syl5bb 530	. . . . . . . . 9
20		eq2ab 1565	. . . . . . . . . . . 12
21		df-sn 2402	. . . . . . . . . . . . 13
22	21	eqeq1i 1474	. . . . . . . . . . . 12
23		iba 640	. . . . . . . . . . . . . 14
24	23	19.21aiv 1281	. . . . . . . . . . . . 13
25		0ex 2701	. . . . . . . . . . . . . . 15
26		eqeq1 1473	. . . . . . . . . . . . . . . 16
27	26	anbi1d 615	. . . . . . . . . . . . . . . 16
28	26, 27	bibi12d 627	. . . . . . . . . . . . . . 15
29	25, 28	cla4v 1859	. . . . . . . . . . . . . 14
30		eqid 1468	. . . . . . . . . . . . . . . 16
31	30	a1bi 197	. . . . . . . . . . . . . . 15
32		pm4.71 633	. . . . . . . . . . . . . . 15
33	31, 32	bitr 173	. . . . . . . . . . . . . 14
34	29, 33	sylibr 200	. . . . . . . . . . . . 13
35	24, 34	impbi 157	. . . . . . . . . . . 12
36	20, 22, 35	3bitr4r 184	. . . . . . . . . . 11
37	36	anbi2i 479	. . . . . . . . . 10
38		elin 2197	. . . . . . . . . 10
39		eleq1 1526	. . . . . . . . . . . 12
40		eleq1 1526	. . . . . . . . . . . . . . 15
41	40	anbi2d 614	. . . . . . . . . . . . . 14
42	41	abbidv 1569	. . . . . . . . . . . . 13
43	42	eqeq2d 1478	. . . . . . . . . . . 12
44	39, 43	anbi12d 626	. . . . . . . . . . 11
45		eqeq1 1473	. . . . . . . . . . . 12
46	45	anbi2d 614	. . . . . . . . . . 11
47	15, 14, 44, 46	opelopab 2809	. . . . . . . . . 10
48	37, 38, 47	3bitr4 183	. . . . . . . . 9
49	19, 48	syl6rbbr 537	. . . . . . . 8
50	49	eqrdv 1466	. . . . . . 7
51	12, 50	syl5cbi 209	. . . . . 6
52		sseq1 2072	. . . . . . 7
53		imassrn 3399	. . . . . . . 8
54	21, 14	eqeltrr 1537	. . . . . . . . . . . . . 14
55		pm3.26 319	. . . . . . . . . . . . . . 15
56	55	ss2abi 2110	. . . . . . . . . . . . . 14
57	54, 56	ssexi 2710	. . . . . . . . . . . . 13
58		eqid 1468	. . . . . . . . . . . . 13
59	57, 58	fnopab2 3604	. . . . . . . . . . . 12
60		fneq1 3568	. . . . . . . . . . . 12
61	59, 60	mpbiri 194	. . . . . . . . . . 11
62		fndm 3573	. . . . . . . . . . 11
63	61, 62	syl 10	. . . . . . . . . 10
64		dfdm4 3294	. . . . . . . . . 10
65	63, 64	syl5eqr 1513	. . . . . . . . 9
66	65	sseq2d 2079	. . . . . . . 8