Theorem pw2en 5671

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. (The 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	|- ~PA ~~ (2o ^m A)

Proof of Theorem pw2en

Step	Hyp	Ref	Expression
1		pw2en.1	. . 3 |- A e. _V
2	1	pwex 3654	. 2 |- ~PA e. _V
3	1	opabex2 4636	. . 3 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. _V
4	3	a1i 8	. 2 |- (x e. ~PA -> {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} e. _V)
5		visset 2541	. . . . 5 |- y e. _V
6	5	cnvex 4528	. . . 4 |- `'y e. _V
7		imaexg 4397	. . . 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		visset 2541	. . . . . 6 |- x e. _V
11	10	elpw 3231	. . . . 5 |- (x e. ~PA <-> x C_ A)
12		p0ex 3659	. . . . . . . . . . . 12 |- {(/)} e. _V
13		visset 2541	. . . . . . . . . . . 12 |- u e. _V
14	12, 13	elimasn 4408	. . . . . . . . . . 11 |- (u e. (`'y"{{(/)}}) <-> <.{(/)}, u>. e. `'y)
15	12, 13	opelcnv 4270	. . . . . . . . . . 11 |- (<.{(/)}, u>. e. `'y <-> <.u, {(/)}>. e. y)
16	14, 15	bitri 279	. . . . . . . . . 10 |- (u e. (`'y"{{(/)}}) <-> <.u, {(/)}>. e. y)
17		eleq2 2205	. . . . . . . . . 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)})}))
18	16, 17	syl5bb 721	. . . . . . . . 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)})}))
19		eq2ab 2253	. . . . . . . . . . . 12 |- ({v | v = (/)} = {v | (v = (/) /\ u e. x)} <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
20		df-sn 3242	. . . . . . . . . . . . 13 |- {(/)} = {v | v = (/)}
21	20	eqeq1i 2148	. . . . . . . . . . . 12 |- ({(/)} = {v | (v = (/) /\ u e. x)} <-> {v | v = (/)} = {v | (v = (/) /\ u e. x)})
22		iba 525	. . . . . . . . . . . . . 14 |- (u e. x -> (v = (/) <-> (v = (/) /\ u e. x)))
23	22	19.21aiv 1933	. . . . . . . . . . . . 13 |- (u e. x -> A.v(v = (/) <-> (v = (/) /\ u e. x)))
24		0ex 3614	. . . . . . . . . . . . . . 15 |- (/) e. _V
25		eqeq1 2147	. . . . . . . . . . . . . . . 16 |- (v = (/) -> (v = (/) <-> (/) = (/)))
26	25	anbi1d 752	. . . . . . . . . . . . . . . 16 |- (v = (/) -> ((v = (/) /\ u e. x) <-> ((/) = (/) /\ u e. x)))
27	25, 26	bibi12d 764	. . . . . . . . . . . . . . 15 |- (v = (/) -> ((v = (/) <-> (v = (/) /\ u e. x)) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x))))
28	24, 27	cla4v 2610	. . . . . . . . . . . . . 14 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
29		eqid 2141	. . . . . . . . . . . . . . . 16 |- (/) = (/)
30	29	a1bi 324	. . . . . . . . . . . . . . 15 |- (u e. x <-> ((/) = (/) -> u e. x))
31		pm4.71 957	. . . . . . . . . . . . . . 15 |- (((/) = (/) -> u e. x) <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
32	30, 31	bitri 279	. . . . . . . . . . . . . 14 |- (u e. x <-> ((/) = (/) <-> ((/) = (/) /\ u e. x)))
33	28, 32	sylibr 243	. . . . . . . . . . . . 13 |- (A.v(v = (/) <-> (v = (/) /\ u e. x)) -> u e. x)
34	23, 33	impbii 223	. . . . . . . . . . . 12 |- (u e. x <-> A.v(v = (/) <-> (v = (/) /\ u e. x)))
35	19, 21, 34	3bitr4ri 296	. . . . . . . . . . 11 |- (u e. x <-> {(/)} = {v | (v = (/) /\ u e. x)})
36	35	anbi2i 708	. . . . . . . . . 10 |- ((u e. A /\ u e. x) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
37		elin 2999	. . . . . . . . . 10 |- (u e. (A i^i x) <-> (u e. A /\ u e. x))
38		eleq1 2204	. . . . . . . . . . . 12 |- (z = u -> (z e. A <-> u e. A))
39		eleq1 2204	. . . . . . . . . . . . . . 15 |- (z = u -> (z e. x <-> u e. x))
40	39	anbi2d 751	. . . . . . . . . . . . . 14 |- (z = u -> ((v = (/) /\ z e. x) <-> (v = (/) /\ u e. x)))
41	40	abbidv 2257	. . . . . . . . . . . . 13 |- (z = u -> {v | (v = (/) /\ z e. x)} = {v | (v = (/) /\ u e. x)})
42	41	eqeq2d 2152	. . . . . . . . . . . 12 |- (z = u -> (w = {v | (v = (/) /\ z e. x)} <-> w = {v | (v = (/) /\ u e. x)}))
43	38, 42	anbi12d 763	. . . . . . . . . . 11 |- (z = u -> ((z e. A /\ w = {v | (v = (/) /\ z e. x)}) <-> (u e. A /\ w = {v | (v = (/) /\ u e. x)})))
44		eqeq1 2147	. . . . . . . . . . . 12 |- (w = {(/)} -> (w = {v | (v = (/) /\ u e. x)} <-> {(/)} = {v | (v = (/) /\ u e. x)}))
45	44	anbi2d 751	. . . . . . . . . . 11 |- (w = {(/)} -> ((u e. A /\ w = {v | (v = (/) /\ u e. x)}) <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)})))
46	13, 12, 43, 45	opelopab 3731	. . . . . . . . . 10 |- (<.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> (u e. A /\ {(/)} = {v | (v = (/) /\ u e. x)}))
47	36, 37, 46	3bitr4i 295	. . . . . . . . 9 |- (u e. (A i^i x) <-> <.u, {(/)}>. e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})})
48	18, 47	syl6rbbr 732	. . . . . . . 8 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (u e. (A i^i x) <-> u e. (`'y"{{(/)}})))
49	48	eqrdv 2139	. . . . . . 7 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (A i^i x) = (`'y"{{(/)}}))
50		sseqin2 3025	. . . . . . . . 9 |- (x C_ A <-> (A i^i x) = x)
51	50	biimpi 224	. . . . . . . 8 |- (x C_ A -> (A i^i x) = x)
52	51	eqeq1d 2149	. . . . . . 7 |- (x C_ A -> ((A i^i x) = (`'y"{{(/)}}) <-> x = (`'y"{{(/)}})))
53	49, 52	syl5ibcom 254	. . . . . 6 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x C_ A -> x = (`'y"{{(/)}})))
54		imassrn 4396	. . . . . . . 8 |- (`'y"{{(/)}}) C_ ran `' y
55		dfdm4 4277	. . . . . . . . . 10 |- dom y = ran `' y
56	20, 12	eqeltrri 2215	. . . . . . . . . . . . . 14 |- {v | v = (/)} e. _V
57		simpl 437	. . . . . . . . . . . . . . 15 |- ((v = (/) /\ z e. x) -> v = (/))
58	57	ss2abi 2905	. . . . . . . . . . . . . 14 |- {v | (v = (/) /\ z e. x)} C_ {v | v = (/)}
59	56, 58	ssexi 3623	. . . . . . . . . . . . 13 |- {v | (v = (/) /\ z e. x)} e. _V
60		eqid 2141	. . . . . . . . . . . . 13 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}
61	59, 60	fnopab2 4645	. . . . . . . . . . . 12 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} Fn A
62		fneq1 4602	. . . . . . . . . . . 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))
63	61, 62	mpbiri 321	. . . . . . . . . . 11 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> y Fn A)
64		fndm 4612	. . . . . . . . . . 11 |- (y Fn A -> dom y = A)
65	63, 64	syl 13	. . . . . . . . . 10 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> dom y = A)
66	55, 65	syl5eqr 2189	. . . . . . . . 9 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> ran `' y = A)
67	66	sseq2d 2872	. . . . . . . 8 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> ((`'y"{{(/)}}) C_ ran `' y <-> (`'y"{{(/)}}) C_ A))
68	54, 67	mpbii 319	. . . . . . 7 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (`'y"{{(/)}}) C_ A)
69		sseq1 2865	. . . . . . 7 |- (x = (`'y"{{(/)}}) -> (x C_ A <-> (`'y"{{(/)}}) C_ A))
70	68, 69	syl5ibrcom 258	. . . . . 6 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x = (`'y"{{(/)}}) -> x C_ A))
71	53, 70	impbid 235	. . . . 5 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x C_ A <-> x = (`'y"{{(/)}})))
72	11, 71	syl5bb 721	. . . 4 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (x e. ~PA <-> x = (`'y"{{(/)}})))
73	72	pm5.32ri 837	. . 3 |- ((x e. ~PA /\ y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}) <-> (x = (`'y"{{(/)}}) /\ y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}))
74		ancom 414	. . 3 |- ((x = (`'y"{{(/)}}) /\ y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}) <-> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} /\ x = (`'y"{{(/)}})))
75		elsn 3251	. . . . . . . . . . . . 13 |- (v e. {(/)} <-> v = (/))
76		iba 525	. . . . . . . . . . . . 13 |- (z e. x -> (v = (/) <-> (v = (/) /\ z e. x)))
77	75, 76	syl5bb 721	. . . . . . . . . . . 12 |- (z e. x -> (v e. {(/)} <-> (v = (/) /\ z e. x)))
78	77	abbi2dv 2258	. . . . . . . . . . 11 |- (z e. x -> {(/)} = {v | (v = (/) /\ z e. x)})
79	12	prid2 3304	. . . . . . . . . . . 12 |- {(/)} e. {(/), {(/)}}
80		df2o2 5352	. . . . . . . . . . . 12 |- 2o = {(/), {(/)}}
81	79, 80	eleqtrri 2217	. . . . . . . . . . 11 |- {(/)} e. 2o
82	78, 81	syl6eqelr 2231	. . . . . . . . . 10 |- (z e. x -> {v | (v = (/) /\ z e. x)} e. 2o)
83		abn0 3099	. . . . . . . . . . . . 13 |- ({v | (v = (/) /\ z e. x)} =/= (/) <-> E.v(v = (/) /\ z e. x))
84		simpr 442	. . . . . . . . . . . . . 14 |- ((v = (/) /\ z e. x) -> z e. x)
85	84	19.23aiv 1943	. . . . . . . . . . . . 13 |- (E.v(v = (/) /\ z e. x) -> z e. x)
86	83, 85	sylbi 225	. . . . . . . . . . . 12 |- ({v | (v = (/) /\ z e. x)} =/= (/) -> z e. x)
87	86	necon1bi 2308	. . . . . . . . . . 11 |- (-. z e. x -> {v | (v = (/) /\ z e. x)} = (/))
88	24	prid1 3303	. . . . . . . . . . . 12 |- (/) e. {(/), {(/)}}
89	88, 80	eleqtrri 2217	. . . . . . . . . . 11 |- (/) e. 2o
90	87, 89	syl6eqel 2230	. . . . . . . . . 10 |- (-. z e. x -> {v | (v = (/) /\ z e. x)} e. 2o)
91	82, 90	pm2.61i 192	. . . . . . . . 9 |- {v | (v = (/) /\ z e. x)} e. 2o
92	91	a1i 8	. . . . . . . 8 |- (z e. A -> {v | (v = (/) /\ z e. x)} e. 2o)
93	60, 92	fopab 4892	. . . . . . 7 |- {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}:A-->2o
94		feq1 4647	. . . . . . 7 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> (y:A-->2o <-> {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}:A-->2o))
95	93, 94	mpbiri 321	. . . . . 6 |- (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> y:A-->2o)
96		eleq2 2205	. . . . . . . . . . . . . . . 16 |- (x = (`'y"{{(/)}}) -> (z e. x <-> z e. (`'y"{{(/)}})))
97		visset 2541	. . . . . . . . . . . . . . . . . 18 |- z e. _V
98	12, 97	elimasn 4408	. . . . . . . . . . . . . . . . 17 |- (z e. (`'y"{{(/)}}) <-> <.{(/)}, z>. e. `'y)
99	12, 97	opelcnv 4270	. . . . . . . . . . . . . . . . 17 |- (<.{(/)}, z>. e. `'y <-> <.z, {(/)}>. e. y)
100	98, 99	bitri 279	. . . . . . . . . . . . . . . 16 |- (z e. (`'y"{{(/)}}) <-> <.z, {(/)}>. e. y)
101	96, 100	syl6bb 729	. . . . . . . . . . . . . . 15 |- (x = (`'y"{{(/)}}) -> (z e. x <-> <.z, {(/)}>. e. y))
102		ffn 4659	. . . . . . . . . . . . . . . . 17 |- (y:A-->2o -> y Fn A)
103	12	fnopfvb 4799	. . . . . . . . . . . . . . . . 17 |- ((y Fn A /\ z e. A) -> ((y` z) = {(/)} <-> <.z, {(/)}>. e. y))
104	102, 103	sylan 597	. . . . . . . . . . . . . . . 16 |- ((y:A-->2o /\ z e. A) -> ((y` z) = {(/)} <-> <.z, {(/)}>. e. y))
105	104	bicomd 271	. . . . . . . . . . . . . . 15 |- ((y:A-->2o /\ z e. A) -> (<.z, {(/)}>. e. y <-> (y` z) = {(/)}))
106	101, 105	sylan9bb 733	. . . . . . . . . . . . . 14 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (z e. x <-> (y` z) = {(/)}))
107	106	biimpa 615	. . . . . . . . . . . . 13 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ z e. x) -> (y` z) = {(/)})
108	78	adantl 448	. . . . . . . . . . . . 13 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ z e. x) -> {(/)} = {v | (v = (/) /\ z e. x)})
109	107, 108	eqtrd 2173	. . . . . . . . . . . 12 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ z e. x) -> (y` z) = {v | (v = (/) /\ z e. x)})
110		ffvelrn 4877	. . . . . . . . . . . . . . . . . . 19 |- ((y:A-->2o /\ z e. A) -> (y` z) e. 2o)
111	80	eleq2i 2208	. . . . . . . . . . . . . . . . . . . 20 |- ((y` z) e. 2o <-> (y` z) e. {(/), {(/)}})
112		fvex 4778	. . . . . . . . . . . . . . . . . . . . 21 |- (y` z) e. _V
113	112	elpr 3254	. . . . . . . . . . . . . . . . . . . 20 |- ((y` z) e. {(/), {(/)}} <-> ((y` z) = (/) \/ (y` z) = {(/)}))
114	111, 113	bitri 279	. . . . . . . . . . . . . . . . . . 19 |- ((y` z) e. 2o <-> ((y` z) = (/) \/ (y` z) = {(/)}))
115	110, 114	sylib 242	. . . . . . . . . . . . . . . . . 18 |- ((y:A-->2o /\ z e. A) -> ((y` z) = (/) \/ (y` z) = {(/)}))
116	115	ord 345	. . . . . . . . . . . . . . . . 17 |- ((y:A-->2o /\ z e. A) -> (-. (y` z) = (/) -> (y` z) = {(/)}))
117	116	adantl 448	. . . . . . . . . . . . . . . 16 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (-. (y` z) = (/) -> (y` z) = {(/)}))
118	117, 106	sylibrd 247	. . . . . . . . . . . . . . 15 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (-. (y` z) = (/) -> z e. x))
119	118	con1d 140	. . . . . . . . . . . . . 14 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (-. z e. x -> (y` z) = (/)))
120	119	imp 393	. . . . . . . . . . . . 13 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ -. z e. x) -> (y` z) = (/))
121	87	adantl 448	. . . . . . . . . . . . 13 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ -. z e. x) -> {v | (v = (/) /\ z e. x)} = (/))
122	120, 121	eqtr4d 2176	. . . . . . . . . . . 12 |- (((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) /\ -. z e. x) -> (y` z) = {v | (v = (/) /\ z e. x)})
123	109, 122	pm2.61dan 833	. . . . . . . . . . 11 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (y` z) = {v | (v = (/) /\ z e. x)})
124		fvopab2 4840	. . . . . . . . . . . . 13 |- ((z e. A /\ {v | (v = (/) /\ z e. x)} e. _V) -> ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z) = {v | (v = (/) /\ z e. x)})
125	59, 124	mpan2 679	. . . . . . . . . . . 12 |- (z e. A -> ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z) = {v | (v = (/) /\ z e. x)})
126	125	ad2antll 805	. . . . . . . . . . 11 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z) = {v | (v = (/) /\ z e. x)})
127	123, 126	eqtr4d 2176	. . . . . . . . . 10 |- ((x = (`'y"{{(/)}}) /\ (y:A-->2o /\ z e. A)) -> (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z))
128	127	expr 589	. . . . . . . . 9 |- ((x = (`'y"{{(/)}}) /\ y:A-->2o) -> (z e. A -> (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z)))
129	128	r19.21aiv 2425	. . . . . . . 8 |- ((x = (`'y"{{(/)}}) /\ y:A-->2o) -> A.z e. A (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z))
130		ax-17 1605	. . . . . . . . . . 11 |- (u e. y -> A.z u e. y)
131		hbopab1 3723	. . . . . . . . . . 11 |- (u e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} -> A.z u e. {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})})
132	130, 131	eqfnfv2f 4856	. . . . . . . . . 10 |- ((y Fn A /\ {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} Fn A) -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> A.z e. A (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z)))
133	102, 61, 132	sylancl 660	. . . . . . . . 9 |- (y:A-->2o -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> A.z e. A (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z)))
134	133	adantl 448	. . . . . . . 8 |- ((x = (`'y"{{(/)}}) /\ y:A-->2o) -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> A.z e. A (y` z) = ({<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}` z)))
135	129, 134	mpbird 318	. . . . . . 7 |- ((x = (`'y"{{(/)}}) /\ y:A-->2o) -> y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})})
136	135	ex 398	. . . . . 6 |- (x = (`'y"{{(/)}}) -> (y:A-->2o -> y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}))
137	95, 136	impbid2 237	. . . . 5 |- (x = (`'y"{{(/)}}) -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> y:A-->2o))
138		2on 5350	. . . . . . 7 |- 2o e. On
139	138	elisseti 2548	. . . . . 6 |- 2o e. _V
140	139, 1	elmap 5554	. . . . 5 |- (y e. (2o ^m A) <-> y:A-->2o)
141	137, 140	syl6bbr 731	. . . 4 |- (x = (`'y"{{(/)}}) -> (y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} <-> y e. (2o ^m A)))
142	141	pm5.32ri 837	. . 3 |- ((y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})} /\ x = (`'y"{{(/)}})) <-> (y e. (2o ^m A) /\ x = (`'y"{{(/)}})))
143	73, 74, 142	3bitri 289	. 2 |- ((x e. ~PA /\ y = {<.z, w>. | (z e. A /\ w = {v | (v = (/) /\ z e. x)})}) <-> (y e. (2o ^m A) /\ x = (`'y"{{(/)}})))
144	2, 4, 9, 143	en2 5622	1 |- ~PA ~~ (2o ^m A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615  {cab 2128   =/= wne 2266  A.wral 2355  _Vcvv 2538   i^i cin 2826   C_ wss 2827  (/)c0 3082  ~Pcpw 3227  {csn 3238  {cpr 3239  <.cop 3240   class class class wbr 3507  {copab 3565  Oncon0 3811  `'ccnv 4118  dom cdm 4119  ran crn 4120  "cima 4122   Fn wfn 4126  -->wf 4127  ` cfv 4131  (class class class)co 4981  2oc2o 5340   ^m cmap 5542   ~~ cen 5584

This theorem is referenced by:  pwen 5788  mappwen 6182  pwsdompw 6264  aleph1 6435  pwcfsdom 6450  cfpwsdom 6451  infmap1 9236  pw2eng 15131

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-suc 3817  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-1o 5344  df-2o 5345  df-map 5544  df-en 5588

Copyright terms: Public domain