Theorem grothpw

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ~P z C_ y /\ E. w e. y ~P z C_ w ) -> ~P z C_ y )
2	1	ralimi	|- ( 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	|- ( z = x -> ~P z = ~P x )
4	3	sseq1d	|- ( z = x -> ( ~P z C_ y <-> ~P x C_ y ) )
5	4	rspccv	|- ( A. z e. y ~P z C_ y -> ( x e. y -> ~P x C_ y ) )
6	2 5	syl	|- ( 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	|- ( ( 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	|- ( ( 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	|- ( ( x e. y /\ ( x e. y -> ~P x C_ y ) ) -> ~P x C_ y )
10		vex	|- y e. _V
11	10	ssex	|- ( ~P x C_ y -> ~P x e. _V )
12	8 9 11	3syl	|- ( ( 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	|- 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	|- ~P x e. _V
15		axpweq	|- ( ~P x e. _V <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
16	14 15	mpbi	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )