Axiom ax-groth

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 ). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	|- y
1		vx	|- x
2	1	cv	|- x
3	0	cv	|- y
4	2 3	wcel	|- x e. y
5		vz	|- z
6		vw	|- w
7	6	cv	|- w
8	5	cv	|- z
9	7 8	wss	|- w C_ z
10	7 3	wcel	|- w e. y
11	9 10	wi	|- ( w C_ z -> w e. y )
12	11 6	wal	|- A. w ( w C_ z -> w e. y )
13		vv	|- v
14	13	cv	|- v
15	14 8	wss	|- v C_ z
16	14 7	wcel	|- v e. w
17	15 16	wi	|- ( v C_ z -> v e. w )
18	17 13	wal	|- A. v ( v C_ z -> v e. w )
19	18 6 3	wrex	|- E. w e. y A. v ( v C_ z -> v e. w )
20	12 19	wa	|- ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) )
21	20 5 3	wral	|- 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	8 3	wss	|- z C_ y
23		cen	|- ~~
24	8 3 23	wbr	|- z ~~ y
25	8 3	wcel	|- z e. y
26	24 25	wo	|- ( z ~~ y \/ z e. y )
27	22 26	wi	|- ( z C_ y -> ( z ~~ y \/ z e. y ) )
28	27 5	wal	|- A. z ( z C_ y -> ( z ~~ y \/ z e. y ) )
29	4 21 28	w3a	|- ( 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 0	wex	|- 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 ) ) )