ThmUniversalClassIsUniverse (3.69, Theorem): The class of all sets is a universe

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#ThmUniversalClassIsUniverse) →

Formula Display:

Proof Trees:

ThmUniversalClassIsUniverse (3.69) — The class of all sets is a universe

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

Title	The class of all sets is a universe `#ThmUniversalClassIsUniverse` `#label-the-class-of-all-sets-is-a-universe`
Classification	Theorem
Formula	0(V universe ) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/universe-pred.html}{\mathsf{universe}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PVUniverseAx_prf`
Scheme of Types	0`(V universe)`
Formal Kernel Proof	Step 0a (V → set, from #DefUniversalClass + #AxmLeftInSound + #RulClassComprehension): 1(𝘍,[]⊢‹∀(x:Class)((x∈V)→(x set ))›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 0b (set → V, from #DefUniversalClass + #AxmLeftInSound + #RulClassComprehension + #AxmPropVerum): 1(𝘍,[]⊢‹∀(x:Class)((x set )→(x∈V))›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 1 (ω ∈ V, from #AxmOmegaIsSet + Step 0b): 1(𝘍,[]⊢‹ω∈V›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/omega-const.html}{\omega} \href{../symbols/in-pred.html}{\in} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 2 (V transitive, from #DefTransitiveClass + #DefSubclass + #DefIsSet + Step 0b): 1(𝘍,[]⊢‹Tr(V)›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 3 (V Hereditary, from #DefHereditaryClass + #AxmHeredity + Steps 0a, 0b): 1(𝘍,[]⊢‹Hereditary(V)›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 4 (V Powerful, from #DefPowerfulClass + #AxmExponent + Steps 0a, 0b): 1(𝘍,[]⊢‹Powerful(V)›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/powerful-pred.html}{\mathsf{Powerful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 5 (V Tight, from #DefTightClass + #AxmSizeLimitation + #DefCardinality/#DefCardLess): 1(𝘍,[]⊢‹Tight(V)›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/tight-pred.html}{\mathsf{Tight}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 6 (V Pairful, from #DefPairfulClass + #DefUnorderedPair sethood + Steps 0a, 0b): 1(𝘍,[]⊢‹Pairful(V)›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/pairful-pred.html}{\mathsf{Pairful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 7 (Instantiated #DefGrothendieckUniverse at U := V): 1(𝘍,[]⊢‹(V universe )⟷(((ω∈V)∧((Tr(V)∧Hereditary(V))∧(Powerful(V)∧Tight(V))))∧Pairful(V))›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/universe-pred.html}{\mathsf{universe}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/in-pred.html}{\in} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/powerful-pred.html}{\mathsf{Powerful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/tight-pred.html}{\mathsf{Tight}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/pairful-pred.html}{\mathsf{Pairful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \) Step 8 (Conclusion via PAndR_prf + def_to_intro, verified by Thm.checkPipeline & Thm.slow_check): 1(𝘍,[]⊢‹V universe ›) 1\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/universe-pred.html}{\mathsf{universe}} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \)
Kernel Note	Formal kernel proof (v_universe_thm_proof : unit -> Thm, verified by Thm.checkPipeline and Thm.slow_check) deriving (𝘍, [] ⊢ (V universe)) from 3.68 #DefGrothendieckUniverse (PKernelDef_prf) and the 6 component lemmas: (1) (ω ∈ V) via 3.57 #AxmOmegaIsSet (POmegaSetAx_prf), 3.05 #DefUniversalClass (PKernelDef_prf), 3.08 #AxmLeftInSound (PLeftInSoundAx_prf), and 3.01 #RulClassComprehension (PComprAx_prf); (2) (V transitive) via 3.15 #DefTransitiveClass (PKernelDef_prf), 3.06 #DefSubclass (PKernelDef_prf), and 3.02 #DefIsSet (PSetDef_prf); (3) (V Hereditary) via 3.44 #DefHereditaryClass (PKernelDef_prf) and 3.12 #AxmHeredity (PHeredityAx_prf); (4) (V Powerful) via 3.45 #DefPowerfulClass (PKernelDef_prf) and 3.13 #AxmExponent (PPowSetAx_prf); (5) (V Tight) via 3.47 #DefTightClass (PKernelDef_prf), 3.43 #AxmSizeLimitation (PSizeLimAx_prf), and 3.41/3.42 #DefCardinality/#DefCardLess (PCardLessOrderAx_prf); (6) (V Pairful) via 3.46 #DefPairfulClass (PKernelDef_prf) and 3.49 #DefUnorderedPair sethood (PPairSetAx_prf). Backup axiom constructor PVUniverseAx_prf (v_universe_axm_backup_entry) is also retained in the kernel just in case.
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassIsUniverse`) → · (3.69) · `#ThmUniversalClassIsUniverse`