Theorem axgroth5 8655

Description: The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)

Assertion

Ref	Expression
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 ) )

Distinct variable group:   x, y, z, w

Proof of Theorem axgroth5

Dummy variable v is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-groth 8654	. 2 |- 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 228	. . . 4 |- ( x e. y <-> x e. y )
3		pwss 3773	. . . . . 6 |- ( ~P z C_ y <-> A. w ( w C_ z -> w e. y ) )
4		pwss 3773	. . . . . . 7 |- ( ~P z C_ w <-> A. v ( v C_ z -> v e. w ) )
5	4	rexbii 2691	. . . . . 6 |- ( E. w e. y ~P z C_ w <-> E. w e. y A. v ( v C_ z -> v e. w ) )
6	3, 5	anbi12i 679	. . . . 5 |- ( ( ~P z C_ y /\ E. w e. y ~P z C_ w ) <-> ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) )
7	6	ralbii 2690	. . . 4 |- ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z 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 ) ) )
8		df-ral 2671	. . . . 5 |- ( A. z e. ~P y ( z ~~ y \/ z e. y ) <-> A. z ( z e. ~P y -> ( z ~~ y \/ z e. y ) ) )
9		vex 2919	. . . . . . . 8 |- z e. _V
10	9	elpw 3765	. . . . . . 7 |- ( z e. ~P y <-> z C_ y )
11	10	imbi1i 316	. . . . . 6 |- ( ( z e. ~P y -> ( z ~~ y \/ z e. y ) ) <-> ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
12	11	albii 1572	. . . . 5 |- ( A. z ( z e. ~P y -> ( z ~~ y \/ z e. y ) ) <-> A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
13	8, 12	bitri 241	. . . 4 |- ( A. z e. ~P y ( z ~~ y \/ z e. y ) <-> A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
14	2, 7, 13	3anbi123i 1142	. . 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 ) ) <-> ( 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 ) ) ) )
15	14	exbii 1589	. 2 |- ( 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 ) ) <-> 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 ) ) ) )
16	1, 15	mpbir 201	1 |- 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 ) )

Syntax hints:   -> wi 4   \/ wo 358   /\ wa 359   /\ w3a 936   A.wal 1546   E.wex 1547   e. wcel 1721   A.wral 2666   E.wrex 2667   C_ wss 3280   ~Pcpw 3759   class class class wbr 4172   ~~ cen 7065

This theorem is referenced by:  grothpw  8657  grothpwex  8658  axgroth6  8659  grothtsk  8666

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-groth 8654

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761