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

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 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )