Axiom ax-groth 10131

Description: The Tarksi-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 10141. An open problem is finding a shorter equivalent.

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	. . . . 5 set x
2	1	cv 1297	. . . 4 class x
3		vy	. . . . 5 set y
4	3	cv 1297	. . . 4 class y
5	2, 4	wcel 1300	. . 3 wff x e. y
6		vw	. . . . . . . . 9 set w
7	6	cv 1297	. . . . . . . 8 class w
8		vz	. . . . . . . . 9 set z
9	8	cv 1297	. . . . . . . 8 class z
10	7, 9	wss 2593	. . . . . . 7 wff w C_ z
11	7, 4	wcel 1300	. . . . . . 7 wff w e. y
12	10, 11	wi 3	. . . . . 6 wff (w C_ z -> w e. y)
13	12, 6	wal 1296	. . . . 5 wff A.w(w C_ z -> w e. y)
14		vv	. . . . . . . . . 10 set v
15	14	cv 1297	. . . . . . . . 9 class v
16	15, 9	wss 2593	. . . . . . . 8 wff v C_ z
17	15, 7	wcel 1300	. . . . . . . 8 wff v e. w
18	16, 17	wi 3	. . . . . . 7 wff (v C_ z -> v e. w)
19	18, 14	wal 1296	. . . . . 6 wff A.v(v C_ z -> v e. w)
20	19, 6, 4	wrex 2106	. . . . 5 wff E.w e. y A.v(v C_ z -> v e. w)
21	13, 20	wa 240	. . . 4 wff (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w))
22	21, 8, 4	wral 2105	. . 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))
23	9, 4	wss 2593	. . . . 5 wff z C_ y
24		cen 5423	. . . . . . 7 class ~~
25	9, 4, 24	wbr 3338	. . . . . 6 wff z ~~ y
26	9, 4	wcel 1300	. . . . . 6 wff z e. y
27	25, 26	wo 239	. . . . 5 wff (z ~~ y \/ z e. y)
28	23, 27	wi 3	. . . 4 wff (z C_ y -> (z ~~ y \/ z e. y))
29	28, 8	wal 1296	. . 3 wff A.z(z C_ y -> (z ~~ y \/ z e. y))
30	5, 22, 29	w3a 858	. 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)))
31	30, 3	wex 1326	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 10132  axgroth2 10133  grothpw 10134  grothomex 10136

Copyright terms: Public domain