This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy 
 |-  y
1 vx 
 |-  x
2 1 cv 
 |-  x
3 0 cv 
 |-  y
4 2 3 wcel 
 |-  x e. y
5 vz 
 |-  z
6 vw 
 |-  w
7 6 cv 
 |-  w
8 5 cv 
 |-  z
9 7 8 wss 
 |-  w C_ z
10 7 3 wcel 
 |-  w e. y
11 9 10 wi 
 |-  ( w C_ z -> w e. y )
12 11 6 wal 
 |-  A. w ( w C_ z -> w e. y )
13 vv 
 |-  v
14 13 cv 
 |-  v
15 14 8 wss 
 |-  v C_ z
16 14 7 wcel 
 |-  v e. w
17 15 16 wi 
 |-  ( v C_ z -> v e. w )
18 17 13 wal 
 |-  A. v ( v C_ z -> v e. w )
19 18 6 3 wrex 
 |-  E. w e. y A. v ( v C_ z -> v e. w )
20 12 19 wa 
 |-  ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) )
21 20 5 3 wral 
 |-  A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) )
22 8 3 wss 
 |-  z C_ y
23 cen 
 |-  ~~
24 8 3 23 wbr 
 |-  z ~~ y
25 8 3 wcel 
 |-  z e. y
26 24 25 wo 
 |-  ( z ~~ y \/ z e. y )
27 22 26 wi 
 |-  ( z C_ y -> ( z ~~ y \/ z e. y ) )
28 27 5 wal 
 |-  A. z ( z C_ y -> ( z ~~ y \/ z e. y ) )
29 4 21 28 w3a 
 |-  ( 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 ) ) )
30 29 0 wex 
 |-  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 ) ) )