Obelisk Proof Assistant — Dependent Types, Families, Σ/Π & Universes

3. Set/Class-Theoretic Foundations (3.01–3.78)

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

Num Entity Database Record (Vertical Field Table)

3.21

Title	Domain (includes arguments with proper class values) `#DefBigDomain` `#label-domain-includes-arguments-with-proper-class-values`
Classification	Definition
Formula	0(∀(F:Class)(Dom(F)={x\|∃(b:Class)((x,b)∈F)})) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{x} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \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/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpDom`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(Dom([F@Class.Expression])={[x@Class.Expression]\|∃([b@Variable]:[Class@Type])(([x@Class.Expression],[b@Class.Expression])∈[F@Class.Expression])}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefBigDomain`) → · (3.21) · `#DefBigDomain`

3.22

Title	IF-THEN-ELSE-FI (Class conditional with NFV side condition and context turnstile) `#DefClassConditional` `#label-if-then-else-fi-class-conditional-with-nfv-side-condition-and-context-turnstile`
Classification	Definition
Formula	0(∀(Γ:Ctx)∀(v:Variable)∀(𝛙:Fm)∀(A:Class)∀(B:Class)((¬Fm .IFV(v,𝛙))→(𝘞,Γ⊢‹⟦IF ⟦𝛙⟧ THEN A ELSE B FI ⟧={⦃v⦄\|(⟦𝛙⟧∧(⦃v⦄∈A))∨((¬⟦𝛙⟧)∧(⦃v⦄∈B))}›))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/typing-colon.html}{:} \href{symbols/ctx-sort.html}{\mathsf{Ctx}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{v} \href{symbols/typing-colon.html}{:} \href{symbols/variable-sort.html}{\mathsf{Variable}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\psi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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/neg-conn.html}{\neg} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/dot-delim.html}{.} \href{symbols/ifv-pred.html}{\mathrm{IFV}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{v} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\boldsymbol{\psi}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-wau.html}{\mathcal{W}} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/antiquotation.html}{[\![ } \href{symbols/class-if-then-else.html}{\mathbf{IF}} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\psi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/class-if-then-else.html}{\mathbf{THEN}} \href{symbols/variables.html}{A} \href{symbols/class-if-then-else.html}{\mathbf{ELSE}} \href{symbols/variables.html}{B} \href{symbols/class-if-then-else.html}{\mathbf{FI}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/eq-pred.html}{=} \href{symbols/class-comprehension.html}{\{} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{v} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\psi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{v} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/or-conn.html}{\lor} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/neg-conn.html}{\neg} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\psi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{v} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpIf`
Scheme of Types	0(∀([Γ@Variable]:[Ctx@Type])∀([v@Variable]:[Variable@Type])∀([𝛙@Variable]:[Fm@Type])∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])((¬Fm.IFV([v@Variable.Expression],[𝛙@Fm.Expression]))→(𝘞,[Γ@Ctx.Expression]⊢‹⟦IF ⟦[𝛙@Fm.Expression]⟧ THEN [A@Class.Expression] ELSE [B@Class.Expression] FI⟧={[⦃[v@Variable.Expression]⦄@Class.Expression]\|(⟦[𝛙@Fm.Expression]⟧∧([⦃[v@Variable.Expression]⦄@Class.Expression]∈[A@Class.Expression]))∨((¬⟦[𝛙@Fm.Expression]⟧)∧([⦃[v@Variable.Expression]⦄@Class.Expression]∈[B@Class.Expression]))}›)))
Verification	Definitional (Kernel AST) · Standalone Entry (`DefClassConditional`) → · (3.22) · `#DefClassConditional`

3.23

Title	simple_if (polymorphic non-dependent conditional over Type) `#DefSimpleConditional` `#label-simple-if-polymorphic-non-dependent-conditional-over-type`
Classification	Definition
Formula	0∀(Tₑ:Type ), ((simple_if (⟦Tₑ⟧):Bool →(⟦Tₑ⟧→(⟦Tₑ⟧→⟦Tₑ⟧)))∧∀(t₁:⟦Tₑ⟧)∀(t₂:⟦Tₑ⟧)((simple_if (⟦Tₑ⟧,⊤,t₁,t₂)=t₁)∧(simple_if (⟦Tₑ⟧,⊥,t₁,t₂)=t₂))) 0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{T_e} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/simple-if.html}{\mathsf{simple\_if}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/typing-colon.html}{:} \href{symbols/bool-sort.html}{\mathsf{Bool}} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t_1} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t_2} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/simple-if.html}{\mathsf{simple\_if}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/comma-delim.html}{,} \href{symbols/top-const.html}{\top} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_1} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{t_1} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/simple-if.html}{\mathsf{simple\_if}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/comma-delim.html}{,} \href{symbols/bot-const.html}{\bot} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_1} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`EIf`
Scheme of Types	0`∀(Tₑ:Type), ((simple_if(⟦Tₑ⟧):Bool→(⟦Tₑ⟧→(⟦Tₑ⟧→⟦Tₑ⟧)))∧∀(t₁:⟦Tₑ⟧)∀(t₂:⟦Tₑ⟧)((simple_if(⟦Tₑ⟧,⊤,t₁,t₂)=t₁)∧(simple_if(⟦Tₑ⟧,⊥,t₁,t₂)=t₂)))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSimpleConditional`) → · (3.23) · `#DefSimpleConditional`

3.24

Title	ifᵈₑₚ (dependent conditional over (Bool → Type)) `#DefDependentConditional` `#label-if-dependent-conditional-over-bool-type`
Classification	Definition
Formula	0∀(Tₑ:Bool →Type ), ((ifᵈₑₚ :Π (b:Bool ),(⟦Tₑ(⊤)⟧→(⟦Tₑ(⊥)⟧→⟦Tₑ(b)⟧)))∧∀(b:Bool )∀(t₁:⟦Tₑ(⊤)⟧)∀(t₂:⟦Tₑ(⊥)⟧)((ifᵈₑₚ (b,t₁,t₂):⟦Tₑ(b)⟧)∧((ifᵈₑₚ (⊤,t₁,t₂)=t₁)∧(ifᵈₑₚ (⊥,t₁,t₂)=t₂)))) 0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{T_e} \href{symbols/typing-colon.html}{:} \href{symbols/bool-sort.html}{\mathsf{Bool}} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{symbols/typing-colon.html}{:} \href{symbols/pi-binder.html}{\Pi} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/typing-colon.html}{:} \href{symbols/bool-sort.html}{\mathsf{Bool}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/top-const.html}{\top} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/bot-const.html}{\bot} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/typing-colon.html}{:} \href{symbols/bool-sort.html}{\mathsf{Bool}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t_1} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/top-const.html}{\top} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t_2} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/bot-const.html}{\bot} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_1} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{T_e} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/top-const.html}{\top} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_1} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{t_1} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/bot-const.html}{\bot} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_1} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{t_2} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`EIfDep`
Scheme of Types	0`∀(Tₑ:Bool→Type), ((ifᵈₑₚ:Π(b:Bool),(⟦Tₑ(⊤)⟧→(⟦Tₑ(⊥)⟧→⟦Tₑ(b)⟧)))∧∀(b:Bool)∀(t₁:⟦Tₑ(⊤)⟧)∀(t₂:⟦Tₑ(⊥)⟧)((ifᵈₑₚ(b,t₁,t₂):⟦Tₑ(b)⟧)∧((ifᵈₑₚ(⊤,t₁,t₂)=t₁)∧(ifᵈₑₚ(⊥,t₁,t₂)=t₂))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefDependentConditional`) → · (3.24) · `#DefDependentConditional`

3.25

Title	Evaluation of a [function\|class-function\|family] `#DefValueAtArg` `#label-evaluation-of-a-function-class-function-family`
Classification	Definition
Formula	0(∀(F:Class)∀(a:Class)(F(a)=⟦IF (∃(s:Class)((a,s)∈F)) THEN ⋃{s\|(a,s)∈F} ELSE V FI ⟧)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/antiquotation.html}{[\![ } \href{symbols/class-if-then-else.html}{\mathbf{IF}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{s} \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}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-if-then-else.html}{\mathbf{THEN}} \href{symbols/bigunion-op.html}{\bigcup} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{s} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/class-comprehension.html}{\}} \href{symbols/class-if-then-else.html}{\mathbf{ELSE}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/class-if-then-else.html}{\mathbf{FI}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpValOf`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])∀([a@Variable]:[Class@Type])([F@Class.Expression]([a@Class.Expression])=⟦IF (∃([s@Variable]:[Class@Type])(([a@Class.Expression],[s@Class.Expression])∈[F@Class.Expression])) THEN ⋃{[s@Class.Expression]\|([a@Class.Expression],[s@Class.Expression])∈[F@Class.Expression]} ELSE V FI⟧))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefValueAtArg`) → · (3.25) · `#DefValueAtArg`

3.26

Title	Image class `#DefRelationalImage` `#label-image-class`
Classification	Definition
Formula	0(∀(f:Class)∀(A:Class)(f[A]={b\|∃(a:Class)((a∈A)∧(f(a)=b))})) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/image-op.html}{[} \href{symbols/variables.html}{A} \href{symbols/image-op.html}{]} \href{symbols/eq-pred.html}{=} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{b} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \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}{a} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpImage`
Scheme of Types	0`(∀([f@Variable]:[Class@Type])∀([A@Variable]:[Class@Type])([f@Class.Expression][[A@Class.Expression]]={[b@Class.Expression]\|∃([a@Variable]:[Class@Type])(([a@Class.Expression]∈[A@Class.Expression])∧([f@Class.Expression]([a@Class.Expression])=[b@Class.Expression]))}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefRelationalImage`) → · (3.26) · `#DefRelationalImage`

3.27

Title	“Has exactly one element” predicate `#DefIsSingleton` `#label-has-exactly-one-element-predicate`
Classification	Definition
Formula	0(∀(s:Class)((s singleton )⟷(∃!(x:Class)(x∈s)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{s} \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}{s} \href{symbols/singleton-pred.html}{\mathsf{singleton}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-uniq-binder.html}{\exists!} \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/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpSingleton`
Scheme of Types	0`(∀([s@Variable]:[Class@Type])(([s@Class.Expression] singleton)⟷(∃!([x@Variable]:[Class@Type])([x@Class.Expression]∈[s@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefIsSingleton`) → · (3.27) · `#DefIsSingleton`

3.28

Title	“Is set-valued” predicate `#DefIsSetValued` `#label-is-set-valued-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F set-valued )⟷(∀(x:Class)((x∈Dom(F))→(F(x) set ))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/set-valued-pred.html}{\mathsf{set\text{-}valued}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \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/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpSetValued`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] set-valued)⟷(∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([F@Class.Expression]))→([F@Class.Expression]([x@Class.Expression]) set)))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefIsSetValued`) → · (3.28) · `#DefIsSetValued`

3.29

Title	“Has concentrated set values” predicate `#DefHasConcentratedValues` `#label-has-concentrated-set-values-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F concentrated set values )⟷(∀(x:Class)((x∈Dom(F))→((F(x) set )→∃!(y:Class)((x,y)∈F)))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/concentrated-pred.html}{\mathsf{concentrated}} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/values-pred.html}{\mathsf{values}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \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/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/exists-uniq-binder.html}{\exists!} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \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/comma-delim.html}{,} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpConcentrated`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] concentrated set values)⟷(∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([F@Class.Expression]))→(([F@Class.Expression]([x@Class.Expression]) set)→∃!([y@Variable]:[Class@Type])(([x@Class.Expression],[y@Class.Expression])∈[F@Class.Expression]))))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefHasConcentratedValues`) → · (3.29) · `#DefHasConcentratedValues`

3.30

Title	“Has flat proper values” predicate `#DefFlatValues` `#label-has-flat-proper-values-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F flat proper values )⟷(∀(x:Class)((x∈Dom(F))→((F(x) proper )→∀(b:Class)(((x,b)∈F)→(b singleton ))))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/flat-pred.html}{\mathsf{flat}} \href{symbols/proper-pred.html}{\mathsf{proper}} \href{symbols/values-pred.html}{\mathsf{values}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \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/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/proper-pred.html}{\mathsf{proper}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/singleton-pred.html}{\mathsf{singleton}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpFlat`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] flat proper values)⟷(∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([F@Class.Expression]))→(([F@Class.Expression]([x@Class.Expression]) proper)→∀([b@Variable]:[Class@Type])((([x@Class.Expression],[b@Class.Expression])∈[F@Class.Expression])→([b@Class.Expression] singleton)))))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefFlatValues`) → · (3.30) · `#DefFlatValues`

3.31

Title	“Is a family” predicate `#DefFamily` `#label-is-a-family-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F family )⟷((F concentrated set values )∧(F flat proper values )))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/concentrated-pred.html}{\mathsf{concentrated}} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/values-pred.html}{\mathsf{values}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/flat-pred.html}{\mathsf{flat}} \href{symbols/proper-pred.html}{\mathsf{proper}} \href{symbols/values-pred.html}{\mathsf{values}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpFamily`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] family)⟷(([F@Class.Expression] concentrated set values)∧([F@Class.Expression] flat proper values))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefFamily`) → · (3.31) · `#DefFamily`

3.32

Title	“Is a class-function” predicate `#DefClassFunction` `#label-is-a-class-function-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F class-function )⟷((F family )∧(F set-valued )))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/class-func-pred.html}{\mathsf{class\text{-}function}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/set-valued-pred.html}{\mathsf{set\text{-}valued}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpClassFunc`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] class-function)⟷(([F@Class.Expression] family)∧([F@Class.Expression] set-valued))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefClassFunction`) → · (3.32) · `#DefClassFunction`

3.33

Title	“Is injective” predicate `#DefInjectiveFunction` `#label-is-injective-predicate`
Classification	Definition
Formula	0(∀(F:Class)((F injective )⟷(((F family )∧(F set-valued ))∧∀(x:Class)∀(y:Class)((((x∈Dom(F))∧(y∈Dom(F)))∧(F(x)=F(y)))→(x=y))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \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}{F} \href{symbols/injective-pred.html}{\mathsf{injective}} \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/variables.html}{F} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/set-valued-pred.html}{\mathsf{set\text{-}valued}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \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/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInjective`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])(([F@Class.Expression] injective)⟷((([F@Class.Expression] family)∧([F@Class.Expression] set-valued))∧∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])(((([x@Class.Expression]∈Dom([F@Class.Expression]))∧([y@Class.Expression]∈Dom([F@Class.Expression])))∧([F@Class.Expression]([x@Class.Expression])=[F@Class.Expression]([y@Class.Expression])))→([x@Class.Expression]=[y@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefInjectiveFunction`) → · (3.33) · `#DefInjectiveFunction`

3.34

Title	“Is a function” predicate `#DefSetFunction` `#label-is-a-function-predicate`
Classification	Definition
Formula	0(∀(f:Class)((f function )⟷((f class-function )∧(f set )))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \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}{f} \href{symbols/func-pred.html}{\mathsf{function}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/class-func-pred.html}{\mathsf{class\text{-}function}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpFunc`
Scheme of Types	0`(∀([f@Variable]:[Class@Type])(([f@Class.Expression] function)⟷(([f@Class.Expression] class-function)∧([f@Class.Expression] set))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSetFunction`) → · (3.34) · `#DefSetFunction`

3.35

Title	“Semi-singleton” predicate `#DefSemiSingleton` `#label-semi-singleton-predicate`
Classification	Definition
Formula	0(∀(s:Class)∀(x:Class)∀(y:Class)(((x∈s)∧(y∈s))→(x=y))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{s} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpSemiSingleton`
Scheme of Types	0`(∀([s@Variable]:[Class@Type])∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])((([x@Class.Expression]∈[s@Class.Expression])∧([y@Class.Expression]∈[s@Class.Expression]))→([x@Class.Expression]=[y@Class.Expression])))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSemiSingleton`) → · (3.35) · `#DefSemiSingleton`

3.36

Title	“Semi-singleton subset” relation (s sss A) `#DefSemiSingletonSubclass` `#label-semi-singleton-subset-relation-s-sss-a`
Classification	Definition
Formula	0(∀(s:Class)∀(A:Class)((s⊆A)∧∀(x:Class)∀(y:Class)(((x∈s)∧(y∈s))→(x=y)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{s} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \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}{s} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpSss`
Scheme of Types	0`(∀([s@Variable]:[Class@Type])∀([A@Variable]:[Class@Type])(([s@Class.Expression]⊆[A@Class.Expression])∧∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])((([x@Class.Expression]∈[s@Class.Expression])∧([y@Class.Expression]∈[s@Class.Expression]))→([x@Class.Expression]=[y@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSemiSingletonSubclass`) → · (3.36) · `#DefSemiSingletonSubclass`

3.37

Title	Evaluation of “Family Value” via semi-singleton subsets `#ThmFamilyEvaluation` `#label-evaluation-of-family-value-via-semi-singleton-subsets`
Classification	Theorem
Formula	0(∀(F:Class)∀(x:Class)((F family )→(F(x)=⋃{s\|(x,s)∈F}))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \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}{F} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/bigunion-op.html}{\bigcup} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{s} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpValOf`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])∀([x@Variable]:[Class@Type])(([F@Class.Expression] family)→([F@Class.Expression]([x@Class.Expression])=⋃{[s@Class.Expression]\|([x@Class.Expression],[s@Class.Expression])∈[F@Class.Expression]})))`
Verification	Verified (Kernel) · Standalone Entry (`ThmFamilyEvaluation`) → · (3.37) · `#ThmFamilyEvaluation`

3.38

Title	“Dependent Sum (Sigma-Type)” model over a family `#DefSigmaModel` `#label-dependent-sum-sigma-type-model-over-a-family`
Classification	Definition
Formula	0(∀(B:Class)∀(x:Class)∀(y:Class)((B family )→(((x∈Dom(B))∧(y∈B(x)))⟷((x,y)∈{s\|∃(a:Class)∃(b:Class)((s=(a,b))∧((a∈Dom(B))∧(b∈B(a))))})))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \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}{B} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \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/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{s} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \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}{s} \href{symbols/eq-pred.html}{=} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/in-pred.html}{\in} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpSigma`
Scheme of Types	0(∀([B@Variable]:[Class@Type])∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])(([B@Class.Expression] family)→((([x@Class.Expression]∈Dom([B@Class.Expression]))∧([y@Class.Expression]∈[B@Class.Expression]([x@Class.Expression])))⟷(([x@Class.Expression],[y@Class.Expression])∈{[s@Class.Expression]\|∃([a@Variable]:[Class@Type])∃([b@Variable]:[Class@Type])(([s@Class.Expression]=([a@Class.Expression],[b@Class.Expression]))∧(([a@Class.Expression]∈Dom([B@Class.Expression]))∧([b@Class.Expression]∈[B@Class.Expression]([a@Class.Expression]))))}))))
Kernel Note	Explicit typed term interpretation / valuation (μ_A : A.Expression → Class.Expression) of the dependent sum Σ(x:Dom(F)) over a family F in the fixed background model.
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSigmaModel`) → · (3.38) · `#DefSigmaModel`

3.39

Title	“Dependent Product (Pi-Type)” predicate and section model `#DefPiPredicateModel` `#label-dependent-product-pi-type-predicate-and-section-model`
Classification	Theorem
Formula	0(∀(B:Class)∀(f:Class)(((B family )∧((f family )∧(Dom(f)=Dom(B))))→∀(x:Class)((x∈Dom(B))→(f(x)∈B(x))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \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/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPi`
Scheme of Types	0`(∀([B@Variable]:[Class@Type])∀([f@Variable]:[Class@Type])((([B@Class.Expression] family)∧(([f@Class.Expression] family)∧(Dom([f@Class.Expression])=Dom([B@Class.Expression]))))→∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([B@Class.Expression]))→([f@Class.Expression]([x@Class.Expression])∈[B@Class.Expression]([x@Class.Expression])))))`
Kernel Note	Explicit typed term interpretation / valuation (μ_A : A.Expression → Class.Expression) of dependent product sections Π(x:Dom(F)) over a family F in the fixed background model.
Verification	Verified (Kernel) · Standalone Entry (`DefPiPredicateModel`) → · (3.39) · `#DefPiPredicateModel`

3.40

Title	“Is not strictly larger than” binary relation `#DefCardLessEq` `#label-is-not-strictly-larger-than-binary-relation`
Classification	Definition
Formula	0(∀(A:Class)∀(B:Class)((A≼B)⟷(∃(f:Class)((((f class-function )∧(A⊆Dom(f)))∧(f[A]⊆B))∧(f injective ))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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}{A} ≼\href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \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/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/class-func-pred.html}{\mathsf{class\text{-}function}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/image-op.html}{[} \href{symbols/variables.html}{A} \href{symbols/image-op.html}{]} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/injective-pred.html}{\mathsf{injective}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpLessEq`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression]≼[B@Class.Expression])⟷(∃([f@Variable]:[Class@Type])(((([f@Class.Expression] class-function)∧([A@Class.Expression]⊆Dom([f@Class.Expression])))∧([f@Class.Expression][[A@Class.Expression]]⊆[B@Class.Expression]))∧([f@Class.Expression] injective)))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefCardLessEq`) → · (3.40) · `#DefCardLessEq`

3.41

Title	Class cardinality `#DefCardinality` `#label-class-cardinality`
Classification	Definition
Formula	0(∀(K:Class)(\|K\|=(On∩⋂{a\|(a∈On)∧(K≼a)}))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-op.html}{ \mid } \href{symbols/variables.html}{K} \href{symbols/card-op.html}{ \mid } \href{symbols/eq-pred.html}{=} \href{symbols/delimiters-brackets.html}{(} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/bininter-op.html}{\cap} \href{symbols/biginter-op.html}{\bigcap} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{a} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} ≼\href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpCard`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])(\|[K@Class.Expression]\|=(On∩⋂{[a@Class.Expression]\|([a@Class.Expression]∈On)∧([K@Class.Expression]≼[a@Class.Expression])})))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefCardinality`) → · (3.41) · `#DefCardinality`

3.42

Title	“Is strictly smaller than” binary relation `#DefCardLess` `#label-is-strictly-smaller-than-binary-relation`
Classification	Definition
Formula	0(∀(A:Class)∀(B:Class)((A≺B)⟷(¬(B≼A)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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}{A} \href{symbols/card-lt-pred.html}{\prec} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} ≼\href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpLess`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression]≺[B@Class.Expression])⟷(¬([B@Class.Expression]≼[A@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefCardLess`) → · (3.42) · `#DefCardLess`

3.43

Title	Size limitation axiom related statement `#AxmSizeLimitation` `#label-size-limitation-axiom-related-statement`
Classification	Axiom
Formula	0(∀(X:Class)((X∈V)⟷(\|X\|≺\|V\|))) 0\(\href{symbols/delimiters-brackets.html}{(} \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/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-op.html}{ \mid } \href{symbols/variables.html}{X} \href{symbols/card-op.html}{ \mid } \href{symbols/card-lt-pred.html}{\prec} \href{symbols/card-op.html}{ \mid } \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/card-op.html}{ \mid } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PSizeLimAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(([X@Class.Expression]∈V)⟷(\|[X@Class.Expression]\|≺\|V\|)))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmSizeLimitation`) → · (3.43) · `#AxmSizeLimitation`

3.44

Title	“Is hereditary” predicate `#DefHereditaryClass` `#label-is-hereditary-predicate`
Classification	Definition
Formula	0(∀(A:Class)(Hereditary(A)⟷(∀(B:Class)((B∈A)→∀(X:Class)((X⊆B)→(X∈A)))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \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/sub-pred.html}{\subseteq} \href{symbols/variables.html}{B} \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/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])(Hereditary([A@Class.Expression])⟷(∀([B@Variable]:[Class@Type])(([B@Class.Expression]∈[A@Class.Expression])→∀([X@Variable]:[Class@Type])(([X@Class.Expression]⊆[B@Class.Expression])→([X@Class.Expression]∈[A@Class.Expression]))))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefHereditaryClass`) → · (3.44) · `#DefHereditaryClass`

3.45

Title	“Is powerful” predicate `#DefPowerfulClass` `#label-is-powerful-predicate`
Classification	Definition
Formula	0(∀(U:Class)(Powerful(U)⟷(∀(B:Class)((B∈U)→(𝒫(B)∈U))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/powerful-pred.html}{\mathsf{Powerful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/power-op.html}{\mathcal{P}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([U@Variable]:[Class@Type])(Powerful([U@Class.Expression])⟷(∀([B@Variable]:[Class@Type])(([B@Class.Expression]∈[U@Class.Expression])→(𝒫([B@Class.Expression])∈[U@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefPowerfulClass`) → · (3.45) · `#DefPowerfulClass`

3.46

Title	“Is pairful” predicate `#DefPairfulClass` `#label-is-pairful-predicate`
Classification	Definition
Formula	0(∀(U:Class)(Pairful(U)⟷(∀(A:Class)∀(B:Class)(((A∈U)∧(B∈U))→({A,B}∈U))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/pairful-pred.html}{\mathsf{Pairful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/upair-op.html}{\{} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/upair-op.html}{\}} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([U@Variable]:[Class@Type])(Pairful([U@Class.Expression])⟷(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])((([A@Class.Expression]∈[U@Class.Expression])∧([B@Class.Expression]∈[U@Class.Expression]))→({[A@Class.Expression],[B@Class.Expression]}∈[U@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefPairfulClass`) → · (3.46) · `#DefPairfulClass`

3.47

Title	“Is tight” predicate `#DefTightClass` `#label-is-tight-predicate`
Classification	Definition
Formula	0(∀(U:Class)(Tight(U)⟷(∀(B:Class)((B⊆U)→((B≺U)⟷(B∈U)))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/tight-pred.html}{\mathsf{Tight}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \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}{B} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/card-lt-pred.html}{\prec} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([U@Variable]:[Class@Type])(Tight([U@Class.Expression])⟷(∀([B@Variable]:[Class@Type])(([B@Class.Expression]⊆[U@Class.Expression])→(([B@Class.Expression]≺[U@Class.Expression])⟷([B@Class.Expression]∈[U@Class.Expression]))))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefTightClass`) → · (3.47) · `#DefTightClass`

3.68

Title	“Is a universe” predicate `#DefGrothendieckUniverse` `#label-is-a-universe-predicate`
Classification	Definition
Formula	0(∀(U:Class)((U universe )⟷(((ω∈U)∧((Tr(U)∧Hereditary(U))∧(Powerful(U)∧Tight(U))))∧Pairful(U)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \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}{U} \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/variables.html}{U} \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/variables.html}{U} \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/variables.html}{U} \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/variables.html}{U} \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/variables.html}{U} \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/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([U@Variable]:[Class@Type])(([U@Class.Expression] universe)⟷(((ω∈[U@Class.Expression])∧((Tr([U@Class.Expression])∧Hereditary([U@Class.Expression]))∧(Powerful([U@Class.Expression])∧Tight([U@Class.Expression]))))∧Pairful([U@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefGrothendieckUniverse`) → · (3.68) · `#DefGrothendieckUniverse`

3.69

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`

3.70

Title	“Tarski's axiom” `#AxmTarskiUniverses` `#label-tarski-s-axiom`
Classification	Axiom
Formula	0(∀(x:Class)((x set )→∃(u:Class)(((u universe )∧(x∈u))∧(u set )))) 0\(\href{symbols/delimiters-brackets.html}{(} \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/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{u} \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/delimiters-brackets.html}{(} \href{symbols/variables.html}{u} \href{symbols/universe-pred.html}{\mathsf{universe}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{u} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{u} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpUniverse`
Scheme of Types	0`(∀([x@Variable]:[Class@Type])(([x@Class.Expression] set)→∃([u@Variable]:[Class@Type])((([u@Class.Expression] universe)∧([x@Class.Expression]∈[u@Class.Expression]))∧([u@Class.Expression] set))))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmTarskiUniverses`) → · (3.70) · `#AxmTarskiUniverses`

3.71

Title	General form of the transfinite ∈-induction principle on a transitive class `#ThmTransitiveClassInduction` `#label-general-form-of-the-transfinite-induction-principle-on-a-transitive-class`
Classification	Theorem
Formula	0(∀(K:Class)∀(A:Class)((Tr(K)∧((K∩𝒫(A))⊆A))→(K⊆A))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \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/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/bininter-op.html}{\cap} \href{symbols/power-op.html}{\mathcal{P}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PEpsIndAx_prf`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])∀([A@Variable]:[Class@Type])((Tr([K@Class.Expression])∧(([K@Class.Expression]∩𝒫([A@Class.Expression]))⊆[A@Class.Expression]))→([K@Class.Expression]⊆[A@Class.Expression])))`
Kernel Note	Transfinite membership (∈) induction on a well-founded transitive class, contrasted with successor-induction (Peano 0-successor-induction Ind(X) in 3.55).
Verification	Verified (Kernel) · Standalone Entry (`ThmTransitiveClassInduction`) → · (3.71) · `#ThmTransitiveClassInduction`