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