Theorem pw2en 3348

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	|- A e. V

Assertion

Ref	Expression
pw2en	|- P~A ~~ (2o ^m A)

Proof of Theorem pw2en

Step	Hyp	Ref	Expression
1		pw2en.1	. . 3 |- A e. V
2	1	pwex 1806	. 2 |- P~A e. V
3		moeq 1431	. . . . 5 |- E*w w = {v | (v = (/) /\ z e. x)}
4	3	a1i 7	. . . 4 |- (z e. A -> E*w w = {v | (v = (/) /\ z e. x)})
5	1, 4	funopabex 2742	. . 3 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. V
6	5	a1i 7	. 2 |- (x e. P~A -> {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. V)
7		visset 1350	. . . . 5 |- y e. V
8	7	cnvex 2670	. . . 4 |- `'y e. V
9		imaexg 2612	. . . 4 |- (`'y e. V -> (`'y"{{(/)}}) e. V)
10	8, 9	ax-mp 6	. . 3 |- (`'y"{{(/)}}) e. V
11	10	a1i 7	. 2 |- (y e. (2o ^m A) -> (`'y"{{(/)}}) e. V)
12		sseqin2 1656	. . . . . . . . . 10 |- (x (_ A <-> (A i^i x) = x)
13	12	biimp 133	. . . . . . . . 9 |- (x (_ A -> (A i^i x) = x)
14	13	cleq1d 1109	. . . . . . . 8 |- (x (_ A -> ((A i^i x) = (`'y"{{(/)}}) <-> x = (`'y"{{(/)}})))
15		eleq2 1150	. . . . . . . . . . 11 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (<.u, {(/)}>. e. y <-> <.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}))
16		p0ex 1885	. . . . . . . . . . . . 13 |- {(/)} e. V
17		visset 1350	. . . . . . . . . . . . 13 |- u e. V
18	16, 17	elimasn 2617	. . . . . . . . . . . 12 |- (u e. (`'y"{{(/)}}) <-> <.{(/)}, u>. e. `'y)
19	16, 17	opelcnv 2518	. . . . . . . . . . . 12 |- (<.{(/)}, u>. e. `'y <-> <.u, {(/)}>. e. y)
20	18, 19	bitr 151	. . . . . . . . . . 11 |- (u e. (`'y"{{(/)}}) <-> <.u, {(/)}>. e. y)
21	15, 20	syl5bb 410	. . . . . . . . . 10 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (u e. (`'y"{{(/)}}) <-> <.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}))
22		cleq2ab 1179	. . . . . . . . . . . . 13 |- ({v | v = (/)} = {v | (v = (/) /\ u e. x)} <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
23		df-sn 1811	. . . . . . . . . . . . . 14 |- {(/)} = {v | v = (/)}
24	23	cleq1i 1108	. . . . . . . . . . . . 13 |- ({(/)} = {v | (v = (/) /\ u e. x)} <-> {v | v = (/)} = {v | (v = (/) /\ u e. x)})
25		iba 486	. . . . . . . . . . . . . . 15 |- (u e. x -> (v = (/) <-> (v = (/) /\ u e. x)))
26	25	19.21aiv 943	. . . . . . . . . . . . . 14 |- (u e. x -> A.v(v = (/) <-> (v = (/) /\ u e. x)))
27		0ex 1745	. . . . . . . . . . . . . . . 16 |- (/) e. V
28		cleq1 1107	. . . . . . . . . . . . . . . . 17 |- (v = (/) -> (v = (/) <-> (/) = (/)))
29	28	anbi1d 469	. . . . . . . . . . . . . . . . 17 |- (v = (/) -> ((v = (/) /\ u e. x) <-> ((/) = (/) /\ u e. x)))
30	28, 29	bibi12d 477	. . . . . . . . . . . . . . . 16 |- (v = (/) -> ((v = (/) <-> (v = (/) /\ u e. x)) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x))))
31	27, 30	cla4v 1400	. . . . . . . . . . . . . . 15 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
32		cleqid 1102	. . . . . . . . . . . . . . . . 17 |- (/) = (/)
33	32	a1bi 172	. . . . . . . . . . . . . . . 16 |- (u e. x <-> ((/) = (/) -> u e. x))
34		pm4.71 481	. . . . . . . . . . . . . . . 16 |- (((/) = (/) -> u e. x) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
35	33, 34	bitr 151	. . . . . . . . . . . . . . 15 |- (u e. x <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
36	31, 35	sylibr 175	. . . . . . . . . . . . . 14 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> u e. x)
37	26, 36	impbi 139	. . . . . . . . . . . . 13 |- (u e. x <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
38	22, 24, 37	3bitr4r 159	. . . . . . . . . . . 12 |- (u e. x <-> {(/)} = {v | (v = (/) /\ u e. x)})
39	38	anbi2i 367	. . . . . . . . . . 11 |- ((u e. A /\ u e. x) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
40		elin 1635	. . . . . . . . . . 11 |- (u e. (A i^i x) <-> (u e. A /\ u e. x))
41		eleq1 1149	. . . . . . . . . . . . 13 |- (z = u -> (z e. A <-> u e. A))
42		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (z = u -> (z e. x <-> u e. x))
43	42	anbi2d 468	. . . . . . . . . . . . . . 15 |- (z = u -> ((v = (/) /\ z e. x) <-> (v = (/) /\ u e. x)))
44	43	biabdv 1183	. . . . . . . . . . . . . 14 |- (z = u -> {v | (v = (/) /\ z e. x)} = {v | (v = (/) /\ u e. x)})
45	44	cleq2d 1112	. . . . . . . . . . . . 13 |- (z = u -> (w = {v | (v = (/) /\ z e. x)} <-> w = {v | (v = (/) /\ u e. x)}))
46	41, 45	anbi12d 476	. . . . . . . . . . . 12 |- (z = u -> ((z e. A /\ w = {v | (v = (/) /\ z e. x)}) <-> (u e. A /\ w = {v | (v = (/) /\ u e. x)})))
47		cleq1 1107	. . . . . . . . . . . . 13 |- (w = {(/)} -> (w = {v | (v = (/) /\ u e. x)} <-> {(/)} = {v | (v = (/) /\ u e. x)}))
48	47	anbi2d 468	. . . . . . . . . . . 12 |- (w = {(/)} -> ((u e. A /\ w = {v | (v = (/) /\ u e. x)}) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)})))
49	17, 16, 46, 48	opelopab 2117	. . . . . . . . . . 11 |- (<.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
50	39, 40, 49	3bitr4 158	. . . . . . . . . 10 |- (u e. (A i^i x) <-> <.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})})
51	21, 50	syl6rbbr 417	. . . . . . . . 9 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (u e. (A i^i x) <-> u e. (`'y"{{(/)}})))
52	51	cleqrd 1100	. . . . . . . 8 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (A i^i x) = (`'y"{{(/)}}))
53	14, 52	syl5bi 183	. . . . . . 7 |- (x (_ A -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> x = (`'y"{{(/)}})))
54	53	com12 13	. . . . . 6 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x (_ A -> x = (`'y"{{(/)}})))
55		sseq1 1521	. . . . . . . 8 |- (x = (`'y"{{(/)}}) -> (x (_ A <-> (`'y"{{(/)}}) (_ A))
56		imassrn 2611	. . . . . . . . 9 |- (`'y"{{(/)}}) (_ ran `'y
57	23, 16	eqeltrr 1160	. . . . . . . . . . . . . . 15 |- {v | v = (/)} e. V
58		pm3.26 256	. . . . . . . . . . . . . . . 16 |- ((v = (/) /\ z e. x) -> v = (/))
59	58	ss2abi 1552	. . . . . . . . . . . . . . 15 |- {v | (v = (/) /\ z e. x)} (_ {v | v = (/)}
60	57, 59	ssexi 1701	. . . . . . . . . . . . . 14 |- {v | (v = (/) /\ z e. x)} e. V
61		cleqid 1102	. . . . . . . . . . . . . 14 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}
62	60, 61	fnopab2 2747	. . . . . . . . . . . . 13 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} Fn A
63		fneq1 2718	. . . . . . . . . . . . 13 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (y Fn A <-> {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} Fn A))
64	62, 63	mpbiri 169	. . . . . . . . . . . 12 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> y Fn A)
65		fndm 2723	. . . . . . . . . . . 12 |- (y Fn A -> dom y = A)
66	64, 65	syl 12	. . . . . . . . . . 11 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> dom y = A)
67		dfdm4 2525	. . . . . . . . . . 11 |- dom y = ran `'y
68	66, 67	syl5eqr 1138	. . . . . . . . . 10 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})