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 𝑦 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( ∀ 𝑤 ( 𝑤𝑧𝑤𝑦 ) ∧ ∃ 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧𝑦 → ( 𝑧𝑦𝑧𝑦 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy 𝑦
1 vx 𝑥
2 1 cv 𝑥
3 0 cv 𝑦
4 2 3 wcel 𝑥𝑦
5 vz 𝑧
6 vw 𝑤
7 6 cv 𝑤
8 5 cv 𝑧
9 7 8 wss 𝑤𝑧
10 7 3 wcel 𝑤𝑦
11 9 10 wi ( 𝑤𝑧𝑤𝑦 )
12 11 6 wal 𝑤 ( 𝑤𝑧𝑤𝑦 )
13 vv 𝑣
14 13 cv 𝑣
15 14 8 wss 𝑣𝑧
16 14 7 wcel 𝑣𝑤
17 15 16 wi ( 𝑣𝑧𝑣𝑤 )
18 17 13 wal 𝑣 ( 𝑣𝑧𝑣𝑤 )
19 18 6 3 wrex 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 )
20 12 19 wa ( ∀ 𝑤 ( 𝑤𝑧𝑤𝑦 ) ∧ ∃ 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 ) )
21 20 5 3 wral 𝑧𝑦 ( ∀ 𝑤 ( 𝑤𝑧𝑤𝑦 ) ∧ ∃ 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 ) )
22 8 3 wss 𝑧𝑦
23 cen
24 8 3 23 wbr 𝑧𝑦
25 8 3 wcel 𝑧𝑦
26 24 25 wo ( 𝑧𝑦𝑧𝑦 )
27 22 26 wi ( 𝑧𝑦 → ( 𝑧𝑦𝑧𝑦 ) )
28 27 5 wal 𝑧 ( 𝑧𝑦 → ( 𝑧𝑦𝑧𝑦 ) )
29 4 21 28 w3a ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( ∀ 𝑤 ( 𝑤𝑧𝑤𝑦 ) ∧ ∃ 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧𝑦 → ( 𝑧𝑦𝑧𝑦 ) ) )
30 29 0 wex 𝑦 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( ∀ 𝑤 ( 𝑤𝑧𝑤𝑦 ) ∧ ∃ 𝑤𝑦𝑣 ( 𝑣𝑧𝑣𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧𝑦 → ( 𝑧𝑦𝑧𝑦 ) ) )