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 ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvary
1 vx setvarx
2 1 cv setvarx
3 0 cv setvary
4 2 3 wcel wffx∈y
5 vz setvarz
6 vw setvarw
7 6 cv setvarw
8 5 cv setvarz
9 7 8 wss wffw⊆z
10 7 3 wcel wffw∈y
11 9 10 wi wffw⊆z→w∈y
12 11 6 wal wff∀ww⊆z→w∈y
13 vv setvarv
14 13 cv setvarv
15 14 8 wss wffv⊆z
16 14 7 wcel wffv∈w
17 15 16 wi wffv⊆z→v∈w
18 17 13 wal wff∀vv⊆z→v∈w
19 18 6 3 wrex wff∃w∈y∀vv⊆z→v∈w
20 12 19 wa wff∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w
21 20 5 3 wral wff∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w
22 8 3 wss wffz⊆y
23 cen class≈
24 8 3 23 wbr wffz≈y
25 8 3 wcel wffz∈y
26 24 25 wo wffz≈y∨z∈y
27 22 26 wi wffz⊆y→z≈y∨z∈y
28 27 5 wal wff∀zz⊆y→z≈y∨z∈y
29 4 21 28 w3a wffx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
30 29 0 wex wff∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y