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

Axiom ax-groth 7861
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 7872. An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)
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 1521 . . 3  wff  x  e.  y
4 vw . . . . . . . . 9  set  w
54cv 1517 . . . . . . . 8  class  w
6 vz . . . . . . . . 9  set  z
76cv 1517 . . . . . . . 8  class  z
85, 7wss 2791 . . . . . . 7  wff  w  C_  z
94, 2wel 1521 . . . . . . 7  wff  w  e.  y
108, 9wi 4 . . . . . 6  wff  ( w 
C_  z  ->  w  e.  y )
1110, 4wal 1439 . . . . 5  wff  A. w
( w  C_  z  ->  w  e.  y )
12 vv . . . . . . . . . 10  set  v
1312cv 1517 . . . . . . . . 9  class  v
1413, 7wss 2791 . . . . . . . 8  wff  v  C_  z
1512, 4wel 1521 . . . . . . . 8  wff  v  e.  w
1614, 15wi 4 . . . . . . 7  wff  ( v 
C_  z  ->  v  e.  w )
1716, 12wal 1439 . . . . . 6  wff  A. v
( v  C_  z  ->  v  e.  w )
182cv 1517 . . . . . 6  class  y
1917, 4, 18wrex 2273 . . . . 5  wff  E. w  e.  y  A. v
( v  C_  z  ->  v  e.  w )
2011, 19wa 356 . . . 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 2272 . . 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 2791 . . . . 5  wff  z  C_  y
23 cen 6294 . . . . . . 7  class  ~~
247, 18, 23wbr 3584 . . . . . 6  wff  z  ~~  y
256, 2wel 1521 . . . . . 6  wff  z  e.  y
2624, 25wo 355 . . . . 5  wff  ( z 
~~  y  \/  z  e.  y )
2722, 26wi 4 . . . 4  wff  ( z 
C_  y  ->  (
z  ~~  y  \/  z  e.  y )
)
2827, 6wal 1439 . . 3  wff  A. z
( z  C_  y  ->  ( z  ~~  y  \/  z  e.  y
) )
293, 21, 28w3a 894 . 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 1444 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  7862  axgroth2  7863
Copyright terms: Public domain