Theorem axgroth6 9250

Description: The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set x, there exists a set y containing x, the subsets of the members of y, the power sets of the members of y, and the subsets of y of cardinality less than that of y. (Contributed by NM, 21-Jun-2009.)

Assertion

Ref	Expression
axgroth6	|- E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) )

Distinct variable group:   x, y, z

Proof of Theorem axgroth6

Dummy variables w v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axgroth5 9246	. 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 ) )
2		biid 240	. . . 4 |- ( x e. y <-> x e. y )
3		pweq 3953	. . . . . . . . 9 |- ( z = v -> ~P z = ~P v )
4	3	sseq1d 3458	. . . . . . . 8 |- ( z = v -> ( ~P z C_ y <-> ~P v C_ y ) )
5	4	cbvralv 3018	. . . . . . 7 |- ( A. z e. y ~P z C_ y <-> A. v e. y ~P v C_ y )
6		ssid 3450	. . . . . . . . . 10 |- ~P z C_ ~P z
7		sseq2 3453	. . . . . . . . . . 11 |- ( w = ~P z -> ( ~P z C_ w <-> ~P z C_ ~P z ) )
8	7	rspcev 3149	. . . . . . . . . 10 |- ( ( ~P z e. y /\ ~P z C_ ~P z ) -> E. w e. y ~P z C_ w )
9	6, 8	mpan2 676	. . . . . . . . 9 |- ( ~P z e. y -> E. w e. y ~P z C_ w )
10		pweq 3953	. . . . . . . . . . . . 13 |- ( v = w -> ~P v = ~P w )
11	10	sseq1d 3458	. . . . . . . . . . . 12 |- ( v = w -> ( ~P v C_ y <-> ~P w C_ y ) )
12	11	rspccv 3146	. . . . . . . . . . 11 |- ( A. v e. y ~P v C_ y -> ( w e. y -> ~P w C_ y ) )
13		pwss 3965	. . . . . . . . . . . 12 |- ( ~P w C_ y <-> A. v ( v C_ w -> v e. y ) )
14		vex 3047	. . . . . . . . . . . . . 14 |- z e. _V
15	14	pwex 4585	. . . . . . . . . . . . 13 |- ~P z e. _V
16		sseq1 3452	. . . . . . . . . . . . . 14 |- ( v = ~P z -> ( v C_ w <-> ~P z C_ w ) )
17		eleq1 2516	. . . . . . . . . . . . . 14 |- ( v = ~P z -> ( v e. y <-> ~P z e. y ) )
18	16, 17	imbi12d 322	. . . . . . . . . . . . 13 |- ( v = ~P z -> ( ( v C_ w -> v e. y ) <-> ( ~P z C_ w -> ~P z e. y ) ) )
19	15, 18	spcv 3139	. . . . . . . . . . . 12 |- ( A. v ( v C_ w -> v e. y ) -> ( ~P z C_ w -> ~P z e. y ) )
20	13, 19	sylbi 199	. . . . . . . . . . 11 |- ( ~P w C_ y -> ( ~P z C_ w -> ~P z e. y ) )
21	12, 20	syl6 34	. . . . . . . . . 10 |- ( A. v e. y ~P v C_ y -> ( w e. y -> ( ~P z C_ w -> ~P z e. y ) ) )
22	21	rexlimdv 2876	. . . . . . . . 9 |- ( A. v e. y ~P v C_ y -> ( E. w e. y ~P z C_ w -> ~P z e. y ) )
23	9, 22	impbid2 208	. . . . . . . 8 |- ( A. v e. y ~P v C_ y -> ( ~P z e. y <-> E. w e. y ~P z C_ w ) )
24	23	ralbidv 2826	. . . . . . 7 |- ( A. v e. y ~P v C_ y -> ( A. z e. y ~P z e. y <-> A. z e. y E. w e. y ~P z C_ w ) )
25	5, 24	sylbi 199	. . . . . 6 |- ( A. z e. y ~P z C_ y -> ( A. z e. y ~P z e. y <-> A. z e. y E. w e. y ~P z C_ w ) )
26	25	pm5.32i 642	. . . . 5 |- ( ( A. z e. y ~P z C_ y /\ A. z e. y ~P z e. y ) <-> ( A. z e. y ~P z C_ y /\ A. z e. y E. w e. y ~P z C_ w ) )
27		r19.26 2916	. . . . 5 |- ( A. z e. y ( ~P z C_ y /\ ~P z e. y ) <-> ( A. z e. y ~P z C_ y /\ A. z e. y ~P z e. y ) )
28		r19.26 2916	. . . . 5 |- ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) <-> ( A. z e. y ~P z C_ y /\ A. z e. y E. w e. y ~P z C_ w ) )
29	26, 27, 28	3bitr4i 281	. . . 4 |- ( A. z e. y ( ~P z C_ y /\ ~P z e. y ) <-> A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) )
30		selpw 3957	. . . . . 6 |- ( z e. ~P y <-> z C_ y )
31		impexp 448	. . . . . . . . 9 |- ( ( ( z C_ y /\ z ~<_ y ) -> ( -. z ~~ y -> z e. y ) ) <-> ( z C_ y -> ( z ~<_ y -> ( -. z ~~ y -> z e. y ) ) ) )
32		vex 3047	. . . . . . . . . . . 12 |- y e. _V
33		ssdomg 7612	. . . . . . . . . . . 12 |- ( y e. _V -> ( z C_ y -> z ~<_ y ) )
34	32, 33	ax-mp 5	. . . . . . . . . . 11 |- ( z C_ y -> z ~<_ y )
35	34	pm4.71i 637	. . . . . . . . . 10 |- ( z C_ y <-> ( z C_ y /\ z ~<_ y ) )
36	35	imbi1i 327	. . . . . . . . 9 |- ( ( z C_ y -> ( -. z ~~ y -> z e. y ) ) <-> ( ( z C_ y /\ z ~<_ y ) -> ( -. z ~~ y -> z e. y ) ) )
37		brsdom 7589	. . . . . . . . . . . 12 |- ( z ~< y <-> ( z ~<_ y /\ -. z ~~ y ) )
38	37	imbi1i 327	. . . . . . . . . . 11 |- ( ( z ~< y -> z e. y ) <-> ( ( z ~<_ y /\ -. z ~~ y ) -> z e. y ) )
39		impexp 448	. . . . . . . . . . 11 |- ( ( ( z ~<_ y /\ -. z ~~ y ) -> z e. y ) <-> ( z ~<_ y -> ( -. z ~~ y -> z e. y ) ) )
40	38, 39	bitri 253	. . . . . . . . . 10 |- ( ( z ~< y -> z e. y ) <-> ( z ~<_ y -> ( -. z ~~ y -> z e. y ) ) )
41	40	imbi2i 314	. . . . . . . . 9 |- ( ( z C_ y -> ( z ~< y -> z e. y ) ) <-> ( z C_ y -> ( z ~<_ y -> ( -. z ~~ y -> z e. y ) ) ) )
42	31, 36, 41	3bitr4ri 282	. . . . . . . 8 |- ( ( z C_ y -> ( z ~< y -> z e. y ) ) <-> ( z C_ y -> ( -. z ~~ y -> z e. y ) ) )
43	42	pm5.74ri 250	. . . . . . 7 |- ( z C_ y -> ( ( z ~< y -> z e. y ) <-> ( -. z ~~ y -> z e. y ) ) )
44		pm4.64 374	. . . . . . 7 |- ( ( -. z ~~ y -> z e. y ) <-> ( z ~~ y \/ z e. y ) )
45	43, 44	syl6bb 265	. . . . . 6 |- ( z C_ y -> ( ( z ~< y -> z e. y ) <-> ( z ~~ y \/ z e. y ) ) )
46	30, 45	sylbi 199	. . . . 5 |- ( z e. ~P y -> ( ( z ~< y -> z e. y ) <-> ( z ~~ y \/ z e. y ) ) )
47	46	ralbiia 2817	. . . 4 |- ( A. z e. ~P y ( z ~< y -> z e. y ) <-> A. z e. ~P y ( z ~~ y \/ z e. y ) )
48	2, 29, 47	3anbi123i 1196	. . 3 |- ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z 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 ) ) )
49	48	exbii 1717	. 2 |- ( E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) ) <-> 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 ) ) )
50	1, 49	mpbir 213	1 |- E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 984   A.wal 1441   = wceq 1443   E.wex 1662   e. wcel 1886   A.wral 2736   E.wrex 2737   _Vcvv 3044   C_ wss 3403   ~Pcpw 3950   class class class wbr 4401   ~~ cen 7563   ~<_ cdom 7564   ~< csdm 7565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-groth 9245

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-dom 7568  df-sdom 7569

This theorem is referenced by:  grothomex  9251  grothac  9252