Theorem pw2en 4446

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 2745	. 2 |- P~A e. V
3	1	opabex2 3610	. . 3 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. V
4	3	a1i 8	. 2 |- (x e. P~A -> {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. V)
5		visset 1813	. . . . 5 |- y e. V
6	5	cnvex 3520	. . . 4 |- `'y e. V
7		imaexg 3416	. . . 4 |- (`'y e. V -> (`'y"{{(/)}}) e. V)
8	6, 7	ax-mp 7	. . 3 |- (`'y"{{(/)}}) e. V
9	8	a1i 8	. 2 |- (y e. (2o ^m A) -> (`'y"{{(/)}}) e. V)
10		sseqin2 2229	. . . . . . . . 9 |- (x (_ A <-> (A i^i x) = x)
11	10	biimp 151	. . . . . . . 8 |- (x (_ A -> (A i^i x) = x)
12	11	eqeq1d 1483	. . . . . . 7 |- (x (_ A -> ((A i^i x) = (`'y"{{(/)}}) <-> x = (`'y"{{(/)}})))
13		eleq2 1535	. . . . . . . . . 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)})}))
14		p0ex 2770	. . . . . . . . . . . 12 |- {(/)} e. V
15		visset 1813	. . . . . . . . . . . 12 |- u e. V
16	14, 15	elimasn 3426	. . . . . . . . . . 11 |- (u e. (`'y"{{(/)}}) <-> <.{(/)}, u>. e. `'y)
17	14, 15	opelcnv 3298	. . . . . . . . . . 11 |- (<.{(/)}, u>. e. `'y <-> <.u, {(/)}>. e. y)
18	16, 17	bitr 173	. . . . . . . . . 10 |- (u e. (`'y"{{(/)}}) <-> <.u, {(/)}>. e. y)
19	13, 18	syl5bb 532	. . . . . . . . 9 |- (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)})}))
20		eq2ab 1573	. . . . . . . . . . . 12 |- ({v | v = (/)} = {v | (v = (/) /\ u e. x)} <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
21		df-sn 2412	. . . . . . . . . . . . 13 |- {(/)} = {v | v = (/)}
22	21	eqeq1i 1482	. . . . . . . . . . . 12 |- ({(/)} = {v | (v = (/) /\ u e. x)} <-> {v | v = (/)} = {v | (v = (/) /\ u e. x)})
23		iba 642	. . . . . . . . . . . . . 14 |- (u e. x -> (v = (/) <-> (v = (/) /\ u e. x)))
24	23	19.21aiv 1286	. . . . . . . . . . . . 13 |- (u e. x -> A.v(v = (/) <-> (v = (/) /\ u e. x)))
25		0ex 2711	. . . . . . . . . . . . . . 15 |- (/) e. V
26		eqeq1 1481	. . . . . . . . . . . . . . . 16 |- (v = (/) -> (v = (/) <-> (/) = (/)))
27	26	anbi1d 617	. . . . . . . . . . . . . . . 16 |- (v = (/) -> ((v = (/) /\ u e. x) <-> ((/) = (/) /\ u e. x)))
28	26, 27	bibi12d 629	. . . . . . . . . . . . . . 15 |- (v = (/) -> ((v = (/) <-> (v = (/) /\ u e. x)) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x))))
29	25, 28	cla4v 1868	. . . . . . . . . . . . . 14 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
30		eqid 1475	. . . . . . . . . . . . . . . 16 |- (/) = (/)
31	30	a1bi 197	. . . . . . . . . . . . . . 15 |- (u e. x <-> ((/) = (/) -> u e. x))
32		pm4.71 635	. . . . . . . . . . . . . . 15 |- (((/) = (/) -> u e. x) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
33	31, 32	bitr 173	. . . . . . . . . . . . . 14 |- (u e. x <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
34	29, 33	sylibr 200	. . . . . . . . . . . . 13 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> u e. x)
35	24, 34	impbi 157	. . . . . . . . . . . 12 |- (u e. x <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
36	20, 22, 35	3bitr4r 184	. . . . . . . . . . 11 |- (u e. x <-> {(/)} = {v | (v = (/) /\ u e. x)})
37	36	anbi2i 480	. . . . . . . . . 10 |- ((u e. A /\ u e. x) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
38		elin 2207	. . . . . . . . . 10 |- (u e. (A i^i x) <-> (u e. A /\ u e. x))
39		eleq1 1534	. . . . . . . . . . . 12 |- (z = u -> (z e. A <-> u e. A))
40		eleq1 1534	. . . . . . . . . . . . . . 15 |- (z = u -> (z e. x <-> u e. x))
41	40	anbi2d 616	. . . . . . . . . . . . . 14 |- (z = u -> ((v = (/) /\ z e. x) <-> (v = (/) /\ u e. x)))
42	41	abbidv 1577	. . . . . . . . . . . . 13 |- (z = u -> {v | (v = (/) /\ z e. x)} = {v | (v = (/) /\ u e. x)})
43	42	eqeq2d 1486	. . . . . . . . . . . 12 |- (z = u -> (w = {v | (v = (/) /\ z e. x)} <-> w = {v | (v = (/) /\ u e. x)}))
44	39, 43	anbi12d 628	. . . . . . . . . . 11 |- (z = u -> ((z e. A /\ w = {v | (v = (/) /\ z e. x)}) <-> (u e. A /\ w = {v | (v = (/) /\ u e. x)})))
45		eqeq1 1481	. . . . . . . . . . . 12 |- (w = {(/)} -> (w = {v | (v = (/) /\ u e. x)} <-> {(/)} = {v | (v = (/) /\ u e. x)}))
46	45	anbi2d 616	. . . . . . . . . . 11 |- (w = {(/)} -> ((u e. A /\ w = {v | (v = (/) /\ u e. x)}) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)})))
47	15, 14, 44, 46	opelopab 2820	. . . . . . . . . 10 |- (<.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
48	37, 38, 47	3bitr4 183	. . . . . . . . 9 |- (u e. (A i^i x) <-> <.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})})
49	19, 48	syl6rbbr 539	. . . . . . . 8 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (u e. (A i^i x) <-> u e. (`'y"{{(/)}})))
50	49	eqrdv 1473	. . . . . . 7 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (A i^i x) = (`'y"{{(/)}}))
51	12, 50	syl5cbi 209	. . . . . 6 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x (_ A -> x = (`'y"{{(/)}})))
52		sseq1 2082	. . . . . . 7 |- (x = (`'y"{{(/)}}) -> (x (_ A <-> (`'y"{{(/)}}) (_ A))
53		imassrn 3415	. . . . . . . 8 |- (`'y"{{(/)}}) (_ ran `' y
54	21, 14	eqeltrr 1545	. . . . . . . . . . . . . 14 |- {v | v = (/)} e. V
55		pm3.26 319	. . . . . . . . . . . . . . 15 |- ((v = (/) /\ z e. x) -> v = (/))
56	55	ss2abi 2120	. . . . . . . . . . . . . 14 |- {v | (v = (/) /\ z e. x)} (_ {v | v = (/)}
57	54, 56	ssexi 2720	. . . . . . . . . . . . 13 |- {v | (v = (/) /\ z e. x)} e. V
58		eqid 1475	. . . . . . . . . . . . 13 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}
59	57, 58	fnopab2 3618	. . . . . . . . . . . 12 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} Fn A
60		fneq1 3582	. . . . . . . . . . . 12 |- (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))
61	59, 60	mpbiri 194	. . . . . . . . . . 11 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> y Fn A)
62		fndm 3587	. . . . . . . . . . 11 |- (y Fn A -> dom y = A)
63	61, 62	syl 10	. . . . . . . . . 10 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> dom y = A)
64		dfdm4 3305	. . . . . . . . . 10 |- dom y = ran `' y
65	63, 64	syl5eqr 1521	. . . . . . . . 9 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> ran `' y = A)
66	65	sseq2d 2089	. . . . . . . 8 |- (y = {<.z, w>. | (z e. A