# 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 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left({z}\approx {y}\vee {z}\in {y}\right)\right)\right)$

### 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}\in {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}\subseteq {z}$
10 7 3 wcel ${wff}{w}\in {y}$
11 9 10 wi ${wff}\left({w}\subseteq {z}\to {w}\in {y}\right)$
12 11 6 wal ${wff}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)$
13 vv ${setvar}{v}$
14 13 cv ${setvar}{v}$
15 14 8 wss ${wff}{v}\subseteq {z}$
16 14 7 wcel ${wff}{v}\in {w}$
17 15 16 wi ${wff}\left({v}\subseteq {z}\to {v}\in {w}\right)$
18 17 13 wal ${wff}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)$
19 18 6 3 wrex ${wff}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)$
20 12 19 wa ${wff}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)\right)$
21 20 5 3 wral ${wff}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)\right)$
22 8 3 wss ${wff}{z}\subseteq {y}$
23 cen ${class}\approx$
24 8 3 23 wbr ${wff}{z}\approx {y}$
25 8 3 wcel ${wff}{z}\in {y}$
26 24 25 wo ${wff}\left({z}\approx {y}\vee {z}\in {y}\right)$
27 22 26 wi ${wff}\left({z}\subseteq {y}\to \left({z}\approx {y}\vee {z}\in {y}\right)\right)$
28 27 5 wal ${wff}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left({z}\approx {y}\vee {z}\in {y}\right)\right)$
29 4 21 28 w3a ${wff}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left({z}\approx {y}\vee {z}\in {y}\right)\right)\right)$
30 29 0 wex ${wff}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {z}\to {v}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left({z}\approx {y}\vee {z}\in {y}\right)\right)\right)$