Axiom ax-groth 10908

Description: The Tarski-Grothendieck Axiom. For every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. 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 10919). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
ax-groth	⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣

Detailed syntax breakdown of Axiom ax-groth

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2		vy	. . . 4 setvar 𝑦
3	1, 2	wel 2146	. . 3 wff 𝑥 ∈ 𝑦
4		vw	. . . . . . . . 9 setvar 𝑤
5	4	cv 1569	. . . . . . . 8 class 𝑤
6		vz	. . . . . . . . 9 setvar 𝑧
7	6	cv 1569	. . . . . . . 8 class 𝑧
8	5, 7	wss 3899	. . . . . . 7 wff 𝑤 ⊆ 𝑧
9	4, 2	wel 2146	. . . . . . 7 wff 𝑤 ∈ 𝑦
10	8, 9	wi 4	. . . . . 6 wff (𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦)
11	10, 4	wal 1568	. . . . 5 wff ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦)
12		vv	. . . . . . . . . 10 setvar 𝑣
13	12	cv 1569	. . . . . . . . 9 class 𝑣
14	13, 7	wss 3899	. . . . . . . 8 wff 𝑣 ⊆ 𝑧
15	12, 4	wel 2146	. . . . . . . 8 wff 𝑣 ∈ 𝑤
16	14, 15	wi 4	. . . . . . 7 wff (𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)
17	16, 12	wal 1568	. . . . . 6 wff ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)
18	2	cv 1569	. . . . . 6 class 𝑦
19	17, 4, 18	wrex 3087	. . . . 5 wff ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)
20	11, 19	wa 401	. . . 4 wff (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤))
21	20, 6, 18	wral 3077	. . 3 wff ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤))
22	7, 18	wss 3899	. . . . 5 wff 𝑧 ⊆ 𝑦
23		cen 8970	. . . . . . 7 class ≈
24	7, 18, 23	wbr 5103	. . . . . 6 wff 𝑧 ≈ 𝑦
25	6, 2	wel 2146	. . . . . 6 wff 𝑧 ∈ 𝑦
26	24, 25	wo 861	. . . . 5 wff (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)
27	22, 26	wi 4	. . . 4 wff (𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
28	27, 6	wal 1568	. . 3 wff ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
29	3, 21, 28	w3a 1103	. 2 wff (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))
30	29, 2	wex 1812	1 wff ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))

This axiom is used by:  axgroth5  10909  axgroth2  10910