Axiom ax-groth 8777

Description: Grothendieck's 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 8783. 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 (_ z -> w e. y) /\ E.w e. y A.v(v (_ z -> v e. w)) /\ A.z(z (_ 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 955	. . . 4 class x
3		vy	. . . . 5 set y
4	3	cv 955	. . . 4 class y
5	2, 4	wcel 958	. . 3 wff x e. y
6		vw	. . . . . . . . 9 set w
7	6	cv 955	. . . . . . . 8 class w
8		vz	. . . . . . . . 9 set z
9	8	cv 955	. . . . . . . 8 class z
10	7, 9	wss 2047	. . . . . . 7 wff w (_ z
11	7, 4	wcel 958	. . . . . . 7 wff w e. y
12	10, 11	wi 3	. . . . . 6 wff (w (_ z -> w e. y)
13	12, 6	wal 954	. . . . 5 wff A.w(w (_ z -> w e. y)
14		vv	. . . . . . . . . 10 set v
15	14	cv 955	. . . . . . . . 9 class v
16	15, 9	wss 2047	. . . . . . . 8 wff v (_ z
17	15, 7	wcel 958	. . . . . . . 8 wff v e. w
18	16, 17	wi 3	. . . . . . 7 wff (v (_ z -> v e. w)
19	18, 14	wal 954	. . . . . 6 wff A.v(v (_ z -> v e. w)
20	19, 6, 4	wrex 1646	. . . . 5 wff E.w e. y A.v(v (_ z -> v e. w)
21	13, 20	wa 223	. . . 4 wff (A.w(w (_ z -> w e. y) /\ E.w e. y A.v(v (_ z -> v e. w))
22	21, 8, 4	wral 1645	. . 3 wff A.z e. y (A.w(w (_ z -> w e. y) /\ E.w e. y A.v(v (_ z -> v e. w))
23	9, 4	wss 2047	. . . . 5 wff z (_ y
24		cen 4364	. . . . . . 7 class ~~
25	9, 4, 24	wbr 2619	. . . . . 6 wff z ~~ y
26	9, 4	wcel 958	. . . . . 6 wff z e. y
27	25, 26	wo 222	. . . . 5 wff (z ~~ y \/ z e. y)
28	23, 27	wi 3	. . . 4 wff (z (_ y -> (z ~~ y \/ z e. y))
29	28, 8	wal 954	. . 3 wff A.z(z (_ y -> (z ~~ y \/ z e. y))
30	5, 22, 29	w3a 775	. 2 wff (x e. y /\ A.z e. y (A.w(w (_ z -> w e. y) /\ E.w e. y A.v(v (_ z -> v e. w)) /\ A.z(z (_ y -> (z ~~ y \/ z e. y)))
31	30, 3	wex 980	1 wff E.y(x e. y /\ A.z e. y (A.w(w (_ z -> w e. y) /\ E.w e. y A.v(v (_ z -> v e. w)) /\ A.z(z (_ y -> (z ~~ y \/ z e. y)))

This axiom is referenced by:  axgroth2 8778  grothinf 8781

Copyright terms: Public domain