Theorem grothpw 9648

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

Assertion

Ref	Expression
grothpw	|- E. y A. 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		simpl 473	. . . . . . . 8 |- ( ( ~P z C_ y /\ E. w e. y ~P z C_ w ) -> ~P z C_ y )
2	1	ralimi 2952	. . . . . . 7 |- ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) -> A. z e. y ~P z C_ y )
3		pweq 4161	. . . . . . . . 9 |- ( z = x -> ~P z = ~P x )
4	3	sseq1d 3632	. . . . . . . 8 |- ( z = x -> ( ~P z C_ y <-> ~P x C_ y ) )
5	4	rspccv 3306	. . . . . . 7 |- ( A. z e. y ~P z C_ y -> ( x e. y -> ~P x C_ y ) )
6	2, 5	syl 17	. . . . . 6 |- ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) -> ( x e. y -> ~P x C_ y ) )
7	6	anim2i 593	. . . . 5 |- ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) ) -> ( x e. y /\ ( x e. y -> ~P x C_ y ) ) )
8	7	3adant3 1081	. . . 4 |- ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) -> ( x e. y /\ ( x e. y -> ~P x C_ y ) ) )
9		pm3.35 611	. . . 4 |- ( ( x e. y /\ ( x e. y -> ~P x C_ y ) ) -> ~P x C_ y )
10		vex 3203	. . . . 5 |- y e. _V
11	10	ssex 4802	. . . 4 |- ( ~P x C_ y -> ~P x e. _V )
12	8, 9, 11	3syl 18	. . 3 |- ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) -> ~P x e. _V )
13		axgroth5 9646	. . 3 |- E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) )
14	12, 13	exlimiiv 1859	. 2 |- ~P x e. _V
15		pwidg 4173	. . . . 5 |- ( ~P x e. _V -> ~P x e. ~P ~P x )
16		pweq 4161	. . . . . . 7 |- ( y = ~P x -> ~P y = ~P ~P x )
17	16	eleq2d 2687	. . . . . 6 |- ( y = ~P x -> ( ~P x e. ~P y <-> ~P x e. ~P ~P x ) )
18	17	spcegv 3294	. . . . 5 |- ( ~P x e. _V -> ( ~P x e. ~P ~P x -> E. y ~P x e. ~P y ) )
19	15, 18	mpd 15	. . . 4 |- ( ~P x e. _V -> E. y ~P x e. ~P y )
20		elex 3212	. . . . 5 |- ( ~P x e. ~P y -> ~P x e. _V )
21	20	exlimiv 1858	. . . 4 |- ( E. y ~P x e. ~P y -> ~P x e. _V )
22	19, 21	impbii 199	. . 3 |- ( ~P x e. _V <-> E. y ~P x e. ~P y )
23	10	elpw2 4828	. . . . 5 |- ( ~P x e. ~P y <-> ~P x C_ y )
24		pwss 4175	. . . . . 6 |- ( ~P x C_ y <-> A. z ( z C_ x -> z e. y ) )
25		dfss2 3591	. . . . . . . 8 |- ( z C_ x <-> A. w ( w e. z -> w e. x ) )
26	25	imbi1i 339	. . . . . . 7 |- ( ( z C_ x -> z e. y ) <-> ( A. w ( w e. z -> w e. x ) -> z e. y ) )
27	26	albii 1747	. . . . . 6 |- ( A. z ( z C_ x -> z e. y ) <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
28	24, 27	bitri 264	. . . . 5 |- ( ~P x C_ y <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
29	23, 28	bitri 264	. . . 4 |- ( ~P x e. ~P y <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
30	29	exbii 1774	. . 3 |- ( E. y ~P x e. ~P y <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
31	22, 30	bitri 264	. 2 |- ( ~P x e. _V <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
32	14, 31	mpbi 220	1 |- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   ~Pcpw 4158   class class class wbr 4653   ~~ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-groth 9645

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by: (None)