Theorem grothpwex

Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth . Note that ax-pow is not used by the proof. Use axpweq to obtain ax-pow . Use pwex or pwexg instead. (Contributed by Gérard Lang, 22-Jun-2009) (New usage is discouraged.)

	Ref	Expression
Assertion	grothpwex	|- ~P x e. _V

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