HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-groth 6711
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 6722. 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
StepHypRef Expression
1 vx . . . 4 set x
2 vy . . . 4 set y
31, 2wel 1452 . . 3 wff x e. y
4 vw . . . . . . . . 9 set w
54cv 1448 . . . . . . . 8 class w
6 vz . . . . . . . . 9 set z
76cv 1448 . . . . . . . 8 class z
85, 7wss 2657 . . . . . . 7 wff w C_ z
94, 2wel 1452 . . . . . . 7 wff w e. y
108, 9wi 4 . . . . . 6 wff (w C_ z -> w e. y)
1110, 4wal 1366 . . . . 5 wff A.w(w C_ z -> w e. y)
12 vv . . . . . . . . . 10 set v
1312cv 1448 . . . . . . . . 9 class v
1413, 7wss 2657 . . . . . . . 8 wff v C_ z
1512, 4wel 1452 . . . . . . . 8 wff v e. w
1614, 15wi 4 . . . . . . 7 wff (v C_ z -> v e. w)
1716, 12wal 1366 . . . . . 6 wff A.v(v C_ z -> v e. w)
182cv 1448 . . . . . 6 class y
1917, 4, 18wrex 2163 . . . . 5 wff E.w e. y A.v(v C_ z -> v e. w)
2011, 19wa 377 . . . 4 wff (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w))
2120, 6, 18wral 2162 . . 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))
227, 18wss 2657 . . . . 5 wff z C_ y
23 cen 5671 . . . . . . 7 class ~~
247, 18, 23wbr 3373 . . . . . 6 wff z ~~ y
256, 2wel 1452 . . . . . 6 wff z e. y
2624, 25wo 376 . . . . 5 wff (z ~~ y \/ z e. y)
2722, 26wi 4 . . . 4 wff (z C_ y -> (z ~~ y \/ z e. y))
2827, 6wal 1366 . . 3 wff A.z(z C_ y -> (z ~~ y \/ z e. y))
293, 21, 28w3a 937 . 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)))
3029, 2wex 1371 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)))
Colors of variables: wff set class
This axiom is referenced by:  axgroth5 6712  axgroth2 6713  grothpw 6714
Copyright terms: Public domain