pw2en - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pw2en 4587

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 2823	. 2
3	1	opabex2 3716	. . 3 $/\$ $/\$
4	3	a1i 8	. 2 $/\$ $/\$
5		visset 1859	. . . . 5
6	5	cnvex 3625	. . . 4
7		imaexg 3508	. . . 4
8	6, 7	ax-mp 7	. . 3
9	8	a1i 8	. 2
10		sseqin2 2281	. . . . . . . . 9
11	10	biimpi 149	. . . . . . . 8
12	11	eqeq1d 1526	. . . . . . 7
13		eleq2 1578	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
14		p0ex 2828	. . . . . . . . . . . 12
15		visset 1859	. . . . . . . . . . . 12
16	14, 15	elimasn 3518	. . . . . . . . . . 11
17	14, 15	opelcnv 3389	. . . . . . . . . . 11
18	16, 17	bitri 171	. . . . . . . . . 10
19	13, 18	syl5bb 535	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
20		eq2ab 1616	. . . . . . . . . . . 12 $/\$ $/\$
21		df-sn 2470	. . . . . . . . . . . . 13
22	21	eqeq1i 1525	. . . . . . . . . . . 12 $/\$ $/\$
23		iba 645	. . . . . . . . . . . . . 14 $/\$
24	23	19.21aiv 1324	. . . . . . . . . . . . 13 $/\$
25		0ex 2785	. . . . . . . . . . . . . . 15
26		eqeq1 1524	. . . . . . . . . . . . . . . 16
27	26	anbi1d 620	. . . . . . . . . . . . . . . 16 $/\$ $/\$
28	26, 27	bibi12d 632	. . . . . . . . . . . . . . 15 $/\$ $/\$
29	25, 28	cla4v 1914	. . . . . . . . . . . . . 14 $/\$ $/\$
30		eqid 1518	. . . . . . . . . . . . . . . 16
31	30	a1bi 195	. . . . . . . . . . . . . . 15
32		pm4.71 638	. . . . . . . . . . . . . . 15 $/\$
33	31, 32	bitri 171	. . . . . . . . . . . . . 14 $/\$
34	29, 33	sylibr 198	. . . . . . . . . . . . 13 $/\$
35	24, 34	impbii 155	. . . . . . . . . . . 12 $/\$
36	20, 22, 35	3bitr4ri 182	. . . . . . . . . . 11 $/\$
37	36	anbi2i 483	. . . . . . . . . 10 $/\$ $/\$ $/\$
38		elin 2259	. . . . . . . . . 10 $/\$
39		eleq1 1577	. . . . . . . . . . . 12
40		eleq1 1577	. . . . . . . . . . . . . . 15
41	40	anbi2d 619	. . . . . . . . . . . . . 14 $/\$ $/\$
42	41	abbidv 1620	. . . . . . . . . . . . 13 $/\$ $/\$
43	42	eqeq2d 1529	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 43	anbi12d 631	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
45		eqeq1 1524	. . . . . . . . . . . 12 $/\$ $/\$
46	45	anbi2d 619	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
47	15, 14, 44, 46	opelopab 2897	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
48	37, 38, 47	3bitr4i 181	. . . . . . . . 9 $/\$ $/\$
49	19, 48	syl6rbbr 542	. . . . . . . 8 $/\$ $/\$
50	49	eqrdv 1516	. . . . . . 7 $/\$ $/\$
51	12, 50	syl5cbi 207	. . . . . 6 $/\$ $/\$
52		sseq1 2134	. . . . . . 7
53		imassrn 3507	. . . . . . . 8
54	21, 14	eqeltrri 1588	. . . . . . . . . . . . . 14
55		pm3.26 317	. . . . . . . . . . . . . . 15 $/\$
56	55	ss2abi 2172	. . . . . . . . . . . . . 14 $/\$
57	54, 56	ssexi 2794	. . . . . . . . . . . . 13 $/\$
58		eqid 1518	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
59	57, 58	fnopab2 3725	. . . . . . . . . . . 12 $/\$ $/\$
60		fneq1 3688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
61	59, 60	mpbiri 192	. . . . . . . . . . 11 $/\$ $/\$
62		fndm 3693	. . . . . . . . . . 11
63	61, 62	syl 10	. . . . . . . . . 10 $/\$ $/\$
64		dfdm4 3396	. . . . . . . . . 10
65	63, 64	syl5eqr 1564	. . . . . . . . 9 $/\$ $/\$
66	65	sseq2d 2141	. . . . . . . 8 $/\$ $/\$
67	53, 66	mpbii 191	. . . . . . 7 $/\$ $/\$
68	52, 67	syl5cbir 209	. . . . . 6 $/\$ $/\$
69	51, 68	impbid 519	. . . . 5 $/\$ $/\$
70		visset 1859	. . . . . 6
71	70	elpw 2461	. . . . 5
72	69, 71	syl5bb 535	. . . 4 $/\$ $/\$
73	72	pm5.32ri 649	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		ancom 437	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		iba 645	. . . . . . . . . . . . 13 $/\$
76		elsn 2479	. . . . . . . . . . . . 13
77	75, 76	syl5bb 535	. . . . . . . . . . . 12 $/\$
78	77	abbi2dv 1621	. . . . . . . . . . 11 $/\$
79	14	prid2 2514	. . . . . . . . . . . 12
80		df2o2 4277	. . . . . . . . . . . 12
81	79, 80	eleqtrri 1590	. . . . . . . . . . 11
82	78, 81	syl6eqelr 1600	. . . . . . . . . 10 $/\$
83		abn0 2343	. . . . . . . . . . . . 13 $/\$ $/\$
84		pm3.27 321	. . . . . . . . . . . . . 14 $/\$
85	84	19.23aiv 1333	. . . . . . . . . . . . 13 $/\$
86	83, 85	sylbi 197	. . . . . . . . . . . 12 $/\$
87	86	necon1bi 1652	. . . . . . . . . . 11 $/\$
88	25	prid1 2513	. . . . . . . . . . . 12
89	88, 80	eleqtrri 1590	. . . . . . . . . . 11
90	87, 89	syl6eqel 1599	. . . . . . . . . 10 $/\$
91	82, 90	pm2.61i 124	. . . . . . . . 9 $/\$
92	91	a1i 8	. . . . . . . 8 $/\$
93	58, 92	fopab 3941	. . . . . . 7 $/\$ $/\$
94		feq1 3727	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
95	93, 94	mpbiri 192	. . . . . 6 $/\$ $/\$
96		eleq2 1578	. . . . . . . . . . . . . . . . 17
97		visset 1859	. . . . . . . . . . . . . . . . . . 19
98	14, 97	elimasn 3518	. . . . . . . . . . . . . . . . . 18
99	14, 97	opelcnv 3389	. . . . . . . . . . . . . . . . . 18
100	98, 99	bitri 171	. . . . . . . . . . . . . . . . 17
101	96, 100	syl6bb 539	. . . . . . . . . . . . . . . 16
102	14	fnopfvb 3865	. . . . . . . . . . . . . . . . . 18 $/\$
103		ffn 3734	. . . . . . . . . . . . . . . . . 18
104	102, 103	sylan 450	. . . . . . . . . . . . . . . . 17 $/\$
105	104	bicomd 524	. . . . . . . . . . . . . . . 16 $/\$
106	101, 105	sylan9bb 543	. . . . . . . . . . . . . . 15 $/\$ $/\$
107	106	biimpa 416	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	78	adantl 388	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109	107, 108	eqtrd 1550	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
110		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	80	eleq2i 1581	. . . . . . . . . . . . . . . . . . . . 21
112		fvex 3843	. . . . . . . . . . . . . . . . . . . . . 22
113	112	elpr 2482	. . . . . . . . . . . . . . . . . . . . 21 $\/$
114	111, 113	bitri 171	. . . . . . . . . . . . . . . . . . . 20 $\/$
115	110, 114	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
116	115	ord 230	. . . . . . . . . . . . . . . . . 18 $/\$
117	116	adantl 388	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
118	117, 106	sylibrd 202	. . . . . . . . . . . . . . . 16 $/\$ $/\$
119	118	con1d 93	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	imp 348	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	87	adantl 388	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
122	120, 121	eqtr4d 1553	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
123	109, 122	pm2.61dan 480	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		fvopab2 3902	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125	57, 124	mpan2 700	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126	125	ad2antll 407	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
127	123, 126	eqtr4d 1553	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	127	exp32 377	. . . . . . . . . 10 $/\$ $/\$
129	128	imp 348	. . . . . . . . 9 $/\$ $/\$ $/\$
130	129	r19.21aiv 1759	. . . . . . . 8 $/\$ $/\$ $/\$
131		ax-17 1007	. . . . . . . . . . . 12
132		hbopab1 2890	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
133	131, 132	eqfnfvf2 3912	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	59, 133	mpan2 700	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	103, 134	syl 10	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	adantl 388	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
137	130, 136	mpbird 194	. . . . . . 7 $/\$ $/\$ $/\$
138	137	ex 371	. . . . . 6 $/\$ $/\$
139	95, 138	impbid2 521	. . . . 5 $/\$ $/\$
140		2on 4275	. . . . . . 7
141	140	elisseti 1864	. . . . . 6
142	141, 1	elmap 4475	. . . . 5
143	139, 142	syl6bbr 541	. . . 4 $/\$ $/\$
144	143	pm5.32ri 649	. . 3 $/\$ $/\$ $/\$ $/\$
145	73, 74, 144	3bitri 175	. 2 $/\$ $/\$ $/\$ $/\$
146	2, 4, 9, 145	en2 4543	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 144 $\/$ wo 220 $/\$ wa 221

wal 990

wceq 992

wcel 994

wex 1016

cab 1505

wne 1628

wral 1691

cvv 1857

cin 2098

wss 2099

c0 2332

cpw 2458

csn 2467

cpr 2468

cop 2469 class class class wbr 2692

copab 2740

con0 2975

ccnv 3250

cdm 3251

crn 3252

cima 3254

wfn 3258

wf 3259

cfv 3263 (class class class)co 4021

c2o 4265

cm 4463

cen 4505

This theorem is referenced by: pwen 4650 aleph1 5021 infmap1 7785

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-nul 2333 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-suc 2981 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-1o 4269 df-2o 4270 df-map 4465 df-en 4509