Axiom ax-groth 9645

Description: The Tarski-Grothendieck Axiom. For every set x there is an inaccessible cardinal y such that y is not in x. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics." This version of the axiom is used by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html). Unlike the ZFC axioms, this axiom is very long when expressed in terms of primitive symbols - see grothprim 9656. An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)

Assertion

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

Distinct variable group:   x, y, z, w, v

Detailed syntax breakdown of Axiom ax-groth

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar x
2		vy	. . . 4 setvar y
3	1, 2	wel 1991	. . 3 wff x e. y
4		vw	. . . . . . . . 9 setvar w
5	4	cv 1482	. . . . . . . 8 class w
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1482	. . . . . . . 8 class z
8	5, 7	wss 3574	. . . . . . 7 wff w C_ z
9	4, 2	wel 1991	. . . . . . 7 wff w e. y
10	8, 9	wi 4	. . . . . 6 wff ( w C_ z -> w e. y )
11	10, 4	wal 1481	. . . . 5 wff A. w ( w C_ z -> w e. y )
12		vv	. . . . . . . . . 10 setvar v
13	12	cv 1482	. . . . . . . . 9 class v
14	13, 7	wss 3574	. . . . . . . 8 wff v C_ z
15	12, 4	wel 1991	. . . . . . . 8 wff v e. w
16	14, 15	wi 4	. . . . . . 7 wff ( v C_ z -> v e. w )
17	16, 12	wal 1481	. . . . . 6 wff A. v ( v C_ z -> v e. w )
18	2	cv 1482	. . . . . 6 class y
19	17, 4, 18	wrex 2913	. . . . 5 wff E. w e. y A. v ( v C_ z -> v e. w )
20	11, 19	wa 384	. . . 4 wff ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) )
21	20, 6, 18	wral 2912	. . 3 wff A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) )
22	7, 18	wss 3574	. . . . 5 wff z C_ y
23		cen 7952	. . . . . . 7 class ~~
24	7, 18, 23	wbr 4653	. . . . . 6 wff z ~~ y
25	6, 2	wel 1991	. . . . . 6 wff z e. y
26	24, 25	wo 383	. . . . 5 wff ( z ~~ y \/ z e. y )
27	22, 26	wi 4	. . . 4 wff ( z C_ y -> ( z ~~ y \/ z e. y ) )
28	27, 6	wal 1481	. . 3 wff A. z ( z C_ y -> ( z ~~ y \/ z e. y ) )
29	3, 21, 28	w3a 1037	. 2 wff ( 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 ) ) )
30	29, 2	wex 1704	1 wff 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 ) ) )

This axiom is referenced by:  axgroth5  9646  axgroth2  9647