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

Axiom ax-groth 6675
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 6686. 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 1460 . . 3 wff x e. y
4 vw . . . . . . . . 9 set w
54cv 1456 . . . . . . . 8 class w
6 vz . . . . . . . . 9 set z
76cv 1456 . . . . . . . 8 class z
85, 7wss 2662 . . . . . . 7 wff w C_ z
94, 2wel 1460 . . . . . . 7 wff w e. y
108, 9wi 4 . . . . . 6 wff (w C_ z -> w e. y)
1110, 4wal 1375 . . . . 5 wff A.w(w C_ z -> w e. y)
12 vv . . . . . . . . . 10 set v
1312cv 1456 . . . . . . . . 9 class v
1413, 7wss 2662 . . . . . . . 8 wff v C_ z
1512, 4wel 1460 . . . . . . . 8 wff v e. w
1614, 15wi 4 . . . . . . 7 wff (v C_ z -> v e. w)
1716, 12wal 1375 . . . . . 6 wff A.v(v C_ z -> v e. w)
182cv 1456 . . . . . 6 class y
1917, 4, 18wrex 2170 . . . . 5 wff E.w e. y A.v(v C_ z -> v e. w)
2011, 19wa 382 . . . 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 2169 . . 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 2662 . . . . 5 wff z C_ y
23 cen 5637 . . . . . . 7 class ~~
247, 18, 23wbr 3376 . . . . . 6 wff z ~~ y
256, 2wel 1460 . . . . . 6 wff z e. y
2624, 25wo 381 . . . . 5 wff (z ~~ y \/ z e. y)
2722, 26wi 4 . . . 4 wff (z C_ y -> (z ~~ y \/ z e. y))
2827, 6wal 1375 . . 3 wff A.z(z C_ y -> (z ~~ y \/ z e. y))
293, 21, 28w3a 946 . 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 1380 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 6676  axgroth2 6677  grothpw 6678
Copyright terms: Public domain