Metamath Proof Explorer


Axiom ax-groth

Description: The Tarski-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 . An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007)

Ref Expression
Assertion ax-groth y x y z y w w z w y w y v v z v w z z y z y z y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvar y
1 vx setvar x
2 1 cv setvar x
3 0 cv setvar y
4 2 3 wcel wff x y
5 vz setvar z
6 vw setvar w
7 6 cv setvar w
8 5 cv setvar z
9 7 8 wss wff w z
10 7 3 wcel wff w y
11 9 10 wi wff w z w y
12 11 6 wal wff w w z w y
13 vv setvar v
14 13 cv setvar v
15 14 8 wss wff v z
16 14 7 wcel wff v w
17 15 16 wi wff v z v w
18 17 13 wal wff v v z v w
19 18 6 3 wrex wff w y v v z v w
20 12 19 wa wff w w z w y w y v v z v w
21 20 5 3 wral wff z y w w z w y w y v v z v w
22 8 3 wss wff z y
23 cen class
24 8 3 23 wbr wff z y
25 8 3 wcel wff z y
26 24 25 wo wff z y z y
27 22 26 wi wff z y z y z y
28 27 5 wal wff z z y z y z y
29 4 21 28 w3a wff x y z y w w z w y w y v v z v w z z y z y z y
30 29 0 wex wff y x y z y w w z w y w y v v z v w z z y z y z y