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