Theorem grothpw 10134

Description: Derive the Axiom of Power Sets ax-pow 3481 from the Tarksi-Grothendieck axiom ax-groth 10131. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3481 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.)

Assertion

Ref	Expression
grothpw	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

Distinct variable group:   x,y,z,w

Proof of Theorem grothpw

Step	Hyp	Ref	Expression
1		ax-groth 10131	. . . 4 |- E.y(x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y)))
2		biid 187	. . . . . 6 |- (x e. y <-> x e. y)
3		dfss2 2610	. . . . . . . . 9 |- (~Pz C_ y <-> A.w(w e. ~Pz -> w e. y))
4		df-pw 3035	. . . . . . . . . . . 12 |- ~Pz = {w | w C_ z}
5	4	abeq2i 2001	. . . . . . . . . . 11 |- (w e. ~Pz <-> w C_ z)
6	5	imbi1i 203	. . . . . . . . . 10 |- ((w e. ~Pz -> w e. y) <-> (w C_ z -> w e. y))
7	6	albii 1346	. . . . . . . . 9 |- (A.w(w e. ~Pz -> w e. y) <-> A.w(w C_ z -> w e. y))
8	3, 7	bitri 190	. . . . . . . 8 |- (~Pz C_ y <-> A.w(w C_ z -> w e. y))
9		dfss2 2610	. . . . . . . . . 10 |- (~Pz C_ w <-> A.v(v e. ~Pz -> v e. w))
10		df-pw 3035	. . . . . . . . . . . . 13 |- ~Pz = {v | v C_ z}
11	10	abeq2i 2001	. . . . . . . . . . . 12 |- (v e. ~Pz <-> v C_ z)
12	11	imbi1i 203	. . . . . . . . . . 11 |- ((v e. ~Pz -> v e. w) <-> (v C_ z -> v e. w))
13	12	albii 1346	. . . . . . . . . 10 |- (A.v(v e. ~Pz -> v e. w) <-> A.v(v C_ z -> v e. w))
14	9, 13	bitri 190	. . . . . . . . 9 |- (~Pz C_ w <-> A.v(v C_ z -> v e. w))
15	14	rexbii 2128	. . . . . . . 8 |- (E.w e. y ~Pz C_ w <-> E.w e. y A.v(v C_ z -> v e. w))
16	8, 15	anbi12i 540	. . . . . . 7 |- ((~Pz C_ y /\ E.w e. y ~Pz C_ w) <-> (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)))
17	16	ralbii 2127	. . . . . 6 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) <-> A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)))
18		df-ral 2109	. . . . . . 7 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z e. ~Py -> (z ~~ y \/ z e. y)))
19		visset 2295	. . . . . . . . . 10 |- z e. _V
20	19	elpw 3037	. . . . . . . . 9 |- (z e. ~Py <-> z C_ y)
21	20	imbi1i 203	. . . . . . . 8 |- ((z e. ~Py -> (z ~~ y \/ z e. y)) <-> (z C_ y -> (z ~~ y \/ z e. y)))
22	21	albii 1346	. . . . . . 7 |- (A.z(z e. ~Py -> (z ~~ y \/ z e. y)) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
23	18, 22	bitri 190	. . . . . 6 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
24	2, 17, 23	3anbi123i 1056	. . . . 5 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) <-> (x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y))))
25	24	exbii 1398	. . . 4 |- (E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) <-> E.y(x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y))))
26	1, 25	mpbir 207	. . 3 |- E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y))
27		simpl 346	. . . . . . . . 9 |- ((~Pz C_ y /\ E.w e. y ~Pz C_ w) -> ~Pz C_ y)
28	27	ralimi 2168	. . . . . . . 8 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> A.z e. y ~Pz C_ y)
29		pweq 3036	. . . . . . . . . 10 |- (z = x -> ~Pz = ~Px)
30	29	sseq1d 2644	. . . . . . . . 9 |- (z = x -> (~Pz C_ y <-> ~Px C_ y))
31	30	rcla4cv 2377	. . . . . . . 8 |- (A.z e. y ~Pz C_ y -> (x e. y -> ~Px C_ y))
32	28, 31	syl 12	. . . . . . 7 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> (x e. y -> ~Px C_ y))
33	32	anim2i 362	. . . . . 6 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w)) -> (x e. y /\ (x e. y -> ~Px C_ y)))
34	33	3adant3 896	. . . . 5 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> (x e. y /\ (x e. y -> ~Px C_ y)))
35		pm3.35 386	. . . . 5 |- ((x e. y /\ (x e. y -> ~Px C_ y)) -> ~Px C_ y)
36		visset 2295	. . . . . 6 |- y e. _V
37	36	ssex 3455	. . . . 5 |- (~Px C_ y -> ~Px e. _V)
38	34, 35, 37	3syl 24	. . . 4 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> ~Px e. _V)
39	38	19.23aiv 1674	. . 3 |- (E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> ~Px e. _V)
40	26, 39	ax-mp 7	. 2 |- ~Px e. _V
41		ssid 2634	. . . . . 6 |- ~Px C_ ~Px
42		elpwg 3038	. . . . . 6 |- (~Px e. _V -> (~Px e. ~P~Px <-> ~Px C_ ~Px))
43	41, 42	mpbiri 211	. . . . 5 |- (~Px e. _V -> ~Px e. ~P~Px)
44		pweq 3036	. . . . . . 7 |- (y = ~Px -> ~Py = ~P~Px)
45	44	eleq2d 1964	. . . . . 6 |- (y = ~Px -> (~Px e. ~Py <-> ~Px e. ~P~Px))
46	45	cla4egv 2365	. . . . 5 |- (~Px e. _V -> (~Px e. ~P~Px -> E.y~Px e. ~Py))
47	43, 46	mpd 29	. . . 4 |- (~Px e. _V -> E.y~Px e. ~Py)
48		elisset 2299	. . . . 5 |- (~Px e. ~Py -> ~Px e. _V)
49	48	19.23aiv 1674	. . . 4 |- (E.y~Px e. ~Py -> ~Px e. _V)
50	47, 49	impbii 174	. . 3 |- (~Px e. _V <-> E.y~Px e. ~Py)
51	36	elpw2 3464	. . . . 5 |- (~Px e. ~Py <-> ~Px C_ y)
52		dfss2 2610	. . . . . 6 |- (~Px C_ y <-> A.z(z e. ~Px -> z e. y))
53		df-pw 3035	. . . . . . . . 9 |- ~Px = {z | z C_ x}
54	53	abeq2i 2001	. . . . . . . 8 |- (z e. ~Px <-> z C_ x)
55	54	imbi1i 203	. . . . . . 7 |- ((z e. ~Px -> z e. y) <-> (z C_ x -> z e. y))
56	55	albii 1346	. . . . . 6 |- (A.z(z e. ~Px -> z e. y) <-> A.z(z C_ x -> z e. y))
57	52, 56	bitri 190	. . . . 5 |- (~Px C_ y <-> A.z(z C_ x -> z e. y))
58		dfss2 2610	. . . . . . 7 |- (z C_ x <-> A.w(w e. z -> w e. x))
59	58	imbi1i 203	. . . . . 6 |- ((z C_ x -> z e. y) <-> (A.w(w e. z -> w e. x) -> z e. y))
60	59	albii 1346	. . . . 5 |- (A.z(z C_ x -> z e. y) <-> A.z(A.w(w e. z -> w e. x) -> z e. y))
61	51, 57, 60	3bitri 194	. . . 4 |- (~Px e. ~Py <-> A.z(A.w(w e. z -> w e. x) -> z e. y))
62	61	exbii 1398	. . 3 |- (E.y~Px e. ~Py <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
63	50, 62	bitri 190	. 2 |- (~Px e. _V <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
64	40, 63	mpbi 206	1 |- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032   class class class wbr 3338   ~~ cen 5423

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-groth 10131

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-pw 3035

Copyright terms: Public domain