Obelisk Entity Database — 3. Set/Class-Theoretic Foundations (3.01

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.01

Title	Class comprehension `#RulClassComprehension` `#label-class-comprehension`
Classification	Inference Rule
Formula	0((⦃x⦄∈{⦃x⦄\|⟦𝛗⟧})⟷((⦃x⦄ set )∧⟦𝛗⟧)) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/in-pred.html}{\in} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PComprAx_prf`
Scheme of Types	0`(([⦃[x@Variable.Expression]⦄@Class.Expression]∈{[⦃[x@Variable.Expression]⦄@Class.Expression]\|⟦[𝛗@Fm.Expression]⟧})⟷(([⦃[x@Variable.Expression]⦄@Class.Expression] set)∧⟦[𝛗@Fm.Expression]⟧))`
Judgements	1[(x:Name), (𝛗:Fm)] 1\(\href{../symbols/image-op.html}{[} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/typing-colon.html}{:} \href{../symbols/name-sort.html}{\mathsf{Name}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/image-op.html}{]} \)
Side Condition	1⊤ 1\(\href{../symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulClassComprehension`) → · (3.01) · `#RulClassComprehension`

3.02

Title	“Is a set” predicate `#DefIsSet` `#label-is-a-set-predicate`
Classification	Definition
Formula	0(∀(X:Class)((X set )⟷(∃(Y:Class)(X∈Y)))) 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/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/exists-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/variables.html}{X} \href{../symbols/in-pred.html}{\in} \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	`PSetDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(([X@Class.Expression] set)⟷(∃([Y@Variable]:[Class@Type])([X@Class.Expression]∈[Y@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefIsSet`) → · (3.02) · `#DefIsSet`

3.03

Title	“Is a proper class” predicate `#DefIsProperClass` `#label-is-a-proper-class-predicate`
Classification	Definition
Formula	0(∀(K:Class)((K proper )⟷(¬(K set )))) 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/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/proper-pred.html}{\mathsf{proper}} \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}{K} \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	`TpProper`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])(([K@Class.Expression] proper)⟷(¬([K@Class.Expression] set))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefIsProperClass`) → · (3.03) · `#DefIsProperClass`

3.04

Title	Empty set `#DefEmptySet` `#label-empty-set`
Classification	Definition
Formula	0(∅={x\|⊥}) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/bot-const.html}{\bot} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpEmptySet`
Scheme of Types	0`(∅={[x@Class.Expression]\|⊥})`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefEmptySet`) → · (3.04) · `#DefEmptySet`

3.05

Title	Universal class `#DefUniversalClass` `#label-universal-class`
Classification	Definition
Formula	0(V={x\|⊤}) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/top-const.html}{\top} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(V={[x@Class.Expression]\|⊤})`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefUniversalClass`) → · (3.05) · `#DefUniversalClass`

3.06

Title	Subclass relation `#DefSubclass` `#label-subclass-relation`
Classification	Definition
Formula	0(∀(X:Class)∀(Y:Class)((X⊆Y)⟷(∀(a:Class)((a∈X)→(a∈Y))))) 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/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}{X} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{Y} \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/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/in-pred.html}{\in} \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	`PSubDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])(([X@Class.Expression]⊆[Y@Class.Expression])⟷(∀([a@Variable]:[Class@Type])(([a@Class.Expression]∈[X@Class.Expression])→([a@Class.Expression]∈[Y@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSubclass`) → · (3.06) · `#DefSubclass`

3.07

Title	Example: “The empty class is a subclass of any class” statement `#ThmEmptySetIsSubclass` `#label-example-the-empty-class-is-a-subclass-of-any-class-statement`
Classification	Theorem
Formula	0(∀(X:Class)(∅⊆X)) 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/emptyset-const.html}{\emptyset} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PSubDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(∅⊆[X@Class.Expression]))`
Verification	Verified (Kernel) · Standalone Entry (`ThmEmptySetIsSubclass`) → · (3.07) · `#ThmEmptySetIsSubclass`

3.08

Title	“Membership respects equality from the left” `#AxmLeftInSound` `#label-membership-respects-equality-from-the-left`
Classification	Axiom
Formula	0(∀(X:Class)∀(Y:Class)((X=Y)→∀(z:Class)((z∈X)⟷(z∈Y)))) 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/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}{X} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{Y} \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}{z} \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}{z} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{z} \href{../symbols/in-pred.html}{\in} \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	`PLeftInSoundAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])(([X@Class.Expression]=[Y@Class.Expression])→∀([z@Variable]:[Class@Type])(([z@Class.Expression]∈[X@Class.Expression])⟷([z@Class.Expression]∈[Y@Class.Expression]))))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmLeftInSound`) → · (3.08) · `#AxmLeftInSound`

3.09

Title	“Membership respects equality from the right” `#AxmRightInSound` `#label-membership-respects-equality-from-the-right`
Classification	Axiom
Formula	0(∀(X:Class)∀(Y:Class)((X=Y)→∀(W:Class)((X∈W)⟷(Y∈W)))) 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/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}{X} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{Y} \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}{W} \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/variables.html}{W} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{Y} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{W} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PRightInSoundAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])(([X@Class.Expression]=[Y@Class.Expression])→∀([W@Variable]:[Class@Type])(([X@Class.Expression]∈[W@Class.Expression])⟷([Y@Class.Expression]∈[W@Class.Expression]))))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmRightInSound`) → · (3.09) · `#AxmRightInSound`

3.10

Title	“Extensionality” `#AxmExtensionality` `#label-extensionality`
Classification	Axiom
Formula	0(∀(X:Class)∀(Y:Class)((∀(z:Class)((z∈X)⟷(z∈Y)))→(X=Y))) 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/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/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{z} \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}{z} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{z} \href{../symbols/in-pred.html}{\in} \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}{)} \)
SML Kernel AST	`PEqDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])((∀([z@Variable]:[Class@Type])(([z@Class.Expression]∈[X@Class.Expression])⟷([z@Class.Expression]∈[Y@Class.Expression])))→([X@Class.Expression]=[Y@Class.Expression])))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmExtensionality`) → · (3.10) · `#AxmExtensionality`

3.11

Title	“Intensionality”(admissible) `#AxmIntensionality` `#label-intensionality-admissible`
Classification	Theorem
Formula	0(∀(X:Class)∀(Y:Class)(((X set )∧(Y set ))→((∀(W:Class)((X∈W)⟷(Y∈W)))→(X=Y)))) 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/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/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{Y} \href{../symbols/set-pred.html}{\mathsf{set}} \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/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{W} \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/variables.html}{W} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{Y} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{W} \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}{)} \)
SML Kernel AST	`PEqDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])((([X@Class.Expression] set)∧([Y@Class.Expression] set))→((∀([W@Variable]:[Class@Type])(([X@Class.Expression]∈[W@Class.Expression])⟷([Y@Class.Expression]∈[W@Class.Expression])))→([X@Class.Expression]=[Y@Class.Expression]))))`
Verification	Verified (Kernel) · Standalone Entry (`AxmIntensionality`) → · (3.11) · `#AxmIntensionality`

3.12

Title	“Heredity”(a subclass of a set is also a set) `#AxmHeredity` `#label-heredity-a-subclass-of-a-set-is-also-a-set`
Classification	Axiom
Formula	0(∀(A:Class)∀(B:Class)(((A⊆B)∧(B set ))→(A set ))) 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/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{B} \href{../symbols/set-pred.html}{\mathsf{set}} \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}{A} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PHeredityAx_prf`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])((([A@Class.Expression]⊆[B@Class.Expression])∧([B@Class.Expression] set))→([A@Class.Expression] set)))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmHeredity`) → · (3.12) · `#AxmHeredity`

3.13

Title	“Exponent”(powerclass of a set is also a set) `#AxmExponent` `#label-exponent-powerclass-of-a-set-is-also-a-set`
Classification	Axiom
Formula	0(∀(X:Class)((X set )→(𝒫(X) 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/delimiters-brackets.html}{(} \href{../symbols/power-op.html}{\mathcal{P}} \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}{)} \)
SML Kernel AST	`PPowSetAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(([X@Class.Expression] set)→(𝒫([X@Class.Expression]) set)))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmExponent`) → · (3.13) · `#AxmExponent`

3.14

Title	“Regularity”(only universal class is equal to its powerclass) `#AxmRegularity` `#label-regularity-only-universal-class-is-equal-to-its-powerclass`
Classification	Axiom
Formula	0(∀(X:Class)((𝒫(X)⊆X)→(V⊆X))) 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/power-op.html}{\mathcal{P}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PEpsIndAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])((𝒫([X@Class.Expression])⊆[X@Class.Expression])→(V⊆[X@Class.Expression])))`
Kernel Note	Kernel Form (Cumulative 𝒫-Induction): ∀(X:Class)((𝒫(X) ⊆ X) → (V ⊆ X)). Classically equivalent (via X = V \ A) to the textbook ∈-minimal-element Regularity / Foundation formulation ∀(A:Class)((A ≠ ∅) → ∃(x:Class)((x ∈ A) ∧ ((x ∩ A) = ∅))).
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmRegularity`) → · (3.14) · `#AxmRegularity`

3.15

Title	Transitivity predicate `#DefTransitiveClass` `#label-transitivity-predicate`
Classification	Definition
Formula	0(∀(A:Class)(Tr(A)⟷(∀(B:Class)((B∈A)→(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/delimiters-brackets.html}{(} \href{../symbols/trans-pred.html}{\mathrm{Tr}} \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/delimiters-brackets.html}{(} \href{../symbols/variables.html}{B} \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}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])(Tr([A@Class.Expression])⟷(∀([B@Variable]:[Class@Type])(([B@Class.Expression]∈[A@Class.Expression])→([B@Class.Expression]⊆[A@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefTransitiveClass`) → · (3.15) · `#DefTransitiveClass`

3.16

Title	Ordinality predicate `#DefOrdinalClass` `#label-ordinality-predicate`
Classification	Definition
Formula	0(∀(A:Class)(Ord(A)⟷(Tr(A)∧∀(B:Class)((B∈A)→Tr(B))))) 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/ord-pred.html}{\mathrm{Ord}} \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/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \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}{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/trans-pred.html}{\mathrm{Tr}} \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/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpOrd`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])(Ord([A@Class.Expression])⟷(Tr([A@Class.Expression])∧∀([B@Variable]:[Class@Type])(([B@Class.Expression]∈[A@Class.Expression])→Tr([B@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefOrdinalClass`) → · (3.16) · `#DefOrdinalClass`

3.17

Title	Class of all ordinal sets(ordinal numbers) `#DefClassOfOrdinals` `#label-class-of-all-ordinal-sets-ordinal-numbers`
Classification	Definition
Formula	0(On={w\|Ord(w)}) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{w} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/ord-pred.html}{\mathrm{Ord}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{w} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpOn`
Scheme of Types	0`(On={[w@Class.Expression]\|Ord([w@Class.Expression])})`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefClassOfOrdinals`) → · (3.17) · `#DefClassOfOrdinals`

3.18

Title	The class of all ordinals is an ordinal class `#ThmOrdinalsIsOrdinal` `#label-the-class-of-all-ordinals-is-an-ordinal-class`
Classification	Theorem
Formula	0Ord(On) 0\(\href{../symbols/ord-pred.html}{\mathrm{Ord}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpOrd`
Scheme of Types	0`Ord(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsIsOrdinal`) → · (3.18) · `#ThmOrdinalsIsOrdinal`

3.19

Title	Union of the elements of a class `#DefUnaryUnion` `#label-union-of-the-elements-of-a-class`
Classification	Definition
Formula	0(∀(K:Class)(⋃K={x\|∃(y:Class)((y∈K)∧(x∈y))})) 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/bigunion-op.html}{\bigcup} \href{../symbols/variables.html}{K} \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}{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}{y} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{K} \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}{y} \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	`CpUnion`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])(⋃[K@Class.Expression]={[x@Class.Expression]\|∃([y@Variable]:[Class@Type])(([y@Class.Expression]∈[K@Class.Expression])∧([x@Class.Expression]∈[y@Class.Expression]))}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefUnaryUnion`) → · (3.19) · `#DefUnaryUnion`

3.20

Title	Intersection of the elements of a class `#DefUnaryIntersection` `#label-intersection-of-the-elements-of-a-class`
Classification	Definition
Formula	0(∀(K:Class)(⋂K={x\|∀(y:Class)((y∈K)→(x∈y))})) 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/biginter-op.html}{\bigcap} \href{../symbols/variables.html}{K} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \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}{y} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{K} \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}{y} \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	`CpInter`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])(⋂[K@Class.Expression]={[x@Class.Expression]\|∀([y@Variable]:[Class@Type])(([y@Class.Expression]∈[K@Class.Expression])→([x@Class.Expression]∈[y@Class.Expression]))}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefUnaryIntersection`) → · (3.20) · `#DefUnaryIntersection`

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.48

Title	Singleton set `#DefSingletonSet` `#label-singleton-set`
Classification	Definition
Formula	0(∀(a:Class)({a}={x\|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/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{a} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpSingleton`
Scheme of Types	0`(∀([a@Variable]:[Class@Type])({[a@Class.Expression]}={[x@Class.Expression]\|[x@Class.Expression]=[a@Class.Expression]}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSingletonSet`) → · (3.48) · `#DefSingletonSet`

3.49

Title	Unordered pair `#DefUnorderedPair` `#label-unordered-pair`
Classification	Definition
Formula	0(∀(a:Class)∀(b:Class)({a,b}={x\|(x=a)∨(x=b)})) 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/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/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{a} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/or-conn.html}{\lor} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpUPair`
Scheme of Types	0`(∀([a@Variable]:[Class@Type])∀([b@Variable]:[Class@Type])({[a@Class.Expression],[b@Class.Expression]}={[x@Class.Expression]\|([x@Class.Expression]=[a@Class.Expression])∨([x@Class.Expression]=[b@Class.Expression])}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefUnorderedPair`) → · (3.49) · `#DefUnorderedPair`

3.50

Title	Set-theoretic models of natural numbers(TBI) `#DefNaturalNumberModels` `#label-set-theoretic-models-of-natural-numbers-tbi`
Classification	Definition
Formula	0((0 :Class ) = ∅) ∧ (((1 :Class ) = {∅}) ∧ (((2 :Class ) = {∅,{∅}}) ∧ ((3 :Class ) = {∅,{∅},{∅,{∅}}}))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-0.html}{0} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-1.html}{1} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-2.html}{2} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-3.html}{3} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpNatModel`
Scheme of Types	0`((0:Class) = ∅) ∧ (((1:Class) = {∅}) ∧ (((2:Class) = {∅,{∅}}) ∧ ((3:Class) = {∅,{∅},{∅,{∅}}})))`
Kernel Note	Explicit typed term interpretation / valuation (μ_Nat : Nat.Expression → Class.Expression) mapping numeral terms 0, 1, 2, 3 into their von Neumann ordinal classes in the fixed background model.
Verification	Definitional (Kernel AST) · Standalone Entry (`DefNaturalNumberModels`) → · (3.50) · `#DefNaturalNumberModels`

3.51

Title	General definition of lists of classes which applicable not only for sets, but for proper classes too(TBI) `#DefClassLists` `#label-general-definition-of-lists-of-classes-which-applicable-not-only-for-sets-but-for-proper-classes-too-tbi`
Classification	Definition
Formula	0(mark (A,n) = ({{0 ,n}} ∪ {({{{a}},n}:Class ) \| (a ∈ A)})) ∧ (([] = ∅) ∧ (([A] = mark (A,1 )) ∧ (([A,B] = (mark (A,1 ) ∪ mark (B,2 ))) ∧ (((A,B) = [A,B]) ∧ ((pr1 (L) = {a \| ({{{a}},1 } ∈ L)}) ∧ (pr2 (L) = {b \| ({{{b}},2 } ∈ L)})))))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/mark-op.html}{\mathrm{mark}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{n} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/numeral-0.html}{0} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{n} \href{../symbols/upair-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{n} \href{../symbols/upair-op.html}{\}} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{ \mid } \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/class-comprehension.html}{\}} \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/empty-list-const.html}{[\,]} \href{../symbols/eq-pred.html}{=} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/image-op.html}{[} \href{../symbols/variables.html}{A} \href{../symbols/image-op.html}{]} \href{../symbols/eq-pred.html}{=} \href{../symbols/mark-op.html}{\mathrm{mark}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/numeral-1.html}{1} \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/image-op.html}{[} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{B} \href{../symbols/image-op.html}{]} \href{../symbols/eq-pred.html}{=} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/mark-op.html}{\mathrm{mark}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/numeral-1.html}{1} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/mark-op.html}{\mathrm{mark}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{B} \href{../symbols/comma-delim.html}{,} \href{../symbols/numeral-2.html}{2} \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/delimiters-brackets.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/eq-pred.html}{=} \href{../symbols/image-op.html}{[} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{B} \href{../symbols/image-op.html}{]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/pr1-op.html}{\mathrm{pr}_1} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{L} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/numeral-1.html}{1} \href{../symbols/upair-op.html}{\}} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{L} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/pr2-op.html}{\mathrm{pr}_2} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{L} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/numeral-2.html}{2} \href{../symbols/upair-op.html}{\}} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{L} \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}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpOPair`
Scheme of Types	0`(mark(A,n) = ({{0,n}} ∪ {({{{a}},n}:Class) \| (a ∈ A)})) ∧ (([] = ∅) ∧ (([A] = mark(A,1)) ∧ (([A,B] = (mark(A,1) ∪ mark(B,2))) ∧ (((A,B) = [A,B]) ∧ ((pr1(L) = {a \| ({{{a}},1} ∈ L)}) ∧ (pr2(L) = {b \| ({{{b}},2} ∈ L)}))))))`
Judgements	1[(A:Class ), (B:Class ), (L:Class ), (n:Class )] 1\(\href{../symbols/image-op.html}{[} \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/comma-delim.html}{,} \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/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{L} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{n} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/image-op.html}{]} \)
Verification	Definitional (Kernel AST) · Standalone Entry (`DefClassLists`) → · (3.51) · `#DefClassLists`

3.52

Title	Ordered pair(Kuratowsky's) `#DefKuratowskiPair` `#label-ordered-pair-kuratowsky-s`
Classification	Definition
Formula	0(∀(a:Class)∀(b:Class)((a,b)={{a,a},{a,b}})) 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/comma-delim.html}{,} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{a} \href{../symbols/upair-op.html}{\}} \href{../symbols/comma-delim.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/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpKuratowskiPair`
Scheme of Types	0`(∀([a@Variable]:[Class@Type])∀([b@Variable]:[Class@Type])(([a@Class.Expression],[b@Class.Expression])={{[a@Class.Expression],[a@Class.Expression]},{[a@Class.Expression],[b@Class.Expression]}}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefKuratowskiPair`) → · (3.52) · `#DefKuratowskiPair`

3.53

Title	Binary union `#DefBinaryUnion` `#label-binary-union`
Classification	Definition
Formula	0(∀(A:Class)∀(B:Class)((A∪B)={x\|(x∈A)∨(x∈B)})) 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/binunion-op.html}{\cup} \href{../symbols/variables.html}{B} \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/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/or-conn.html}{\lor} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpBinUnion`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression]∪[B@Class.Expression])={[x@Class.Expression]\|([x@Class.Expression]∈[A@Class.Expression])∨([x@Class.Expression]∈[B@Class.Expression])}))`
Kernel Note	Special Def.: (x ∪ y) = ⋃{x,y} (set-restricted); General Def.: (A ∪ B) = {z \| (z ∈ A) ∨ (z ∈ B)} (general class definition).
Verification	Definitional (Kernel AST) · Standalone Entry (`DefBinaryUnion`) → · (3.53) · `#DefBinaryUnion`

3.54

Title	Binary intersection `#DefBinaryIntersection` `#label-binary-intersection`
Classification	Definition
Formula	0(∀(A:Class)∀(B:Class)((A∩B)={x\|(x∈A)∧(x∈B)})) 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/bininter-op.html}{\cap} \href{../symbols/variables.html}{B} \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/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/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpBinInter`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression]∩[B@Class.Expression])={[x@Class.Expression]\|([x@Class.Expression]∈[A@Class.Expression])∧([x@Class.Expression]∈[B@Class.Expression])}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefBinaryIntersection`) → · (3.54) · `#DefBinaryIntersection`

3.55

Title	“Is successor-inductive (Peano-inductive)” predicate `#DefInductiveClass` `#label-is-successor-inductive-peano-inductive-predicate`
Classification	Definition
Formula	0(∀(X:Class)(Ind(X)⟷((∅∈X)∧∀(a:Class)((a∈X)→((a∪{a})∈X))))) 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/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \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}{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}{X} \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}{a} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/in-pred.html}{\in} \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	`TpInd`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(Ind([X@Class.Expression])⟷((∅∈[X@Class.Expression])∧∀([a@Variable]:[Class@Type])(([a@Class.Expression]∈[X@Class.Expression])→(([a@Class.Expression]∪{[a@Class.Expression]})∈[X@Class.Expression])))))`
Kernel Note	Successor-inductive (Peano 0-successor-inductive) in the narrowest sense: closed under 0 = ∅ and ordinal successor a \|-> a ∪ {a}, as distinguished from transfinite ∈-induction (3.70) or 𝒫-induction.
Verification	Definitional (Kernel AST) · Standalone Entry (`DefInductiveClass`) → · (3.55) · `#DefInductiveClass`

3.56

Title	The intersection class of all successor-inductive (Peano-inductive) classes is called omega (⊆-minimal successor-inductive class and smallest successor-inductive ordinal) `#DefOmega` `#label-the-intersection-class-of-all-successor-inductive-peano-inductive-classes-is-called-omega-minimal-successor-inductive-class-and-smallest-successor-inductive-ordinal`
Classification	Definition
Formula	0(∀(x:Class)((x∈ω)⟷(∀(Q:Class)(Ind(Q)→(x∈Q))))) 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/omega-const.html}{\omega} \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}{Q} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{Q} \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}{Q} \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	`CpOmega`
Scheme of Types	0`(∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈ω)⟷(∀([Q@Variable]:[Class@Type])(Ind([Q@Class.Expression])→([x@Class.Expression]∈[Q@Class.Expression])))))`
Kernel Note	By definition, ω is not only the smallest successor-inductive ordinal, but also the ⊆-minimal (least) element among all successor-inductive (Peano-inductive) classes in the subclass (⊆) order (Ind(ω) ∧ ∀(Q:Class), Ind(Q) → (ω ⊆ Q)), directly expressing simple countable mathematical (Peano) induction up to ω. \| Special Def.: ω = ⋂{q \| Ind(q)}; General Def.: ∀(x:Class), (x ∈ ω) ⟷ (∀(Q:Class), Ind(Q) → (x ∈ Q)).
Verification	Definitional (Kernel AST) · Standalone Entry (`DefOmega`) → · (3.56) · `#DefOmega`

3.57

Title	“Infinity”(ω is a set) `#AxmOmegaIsSet` `#label-infinity-is-a-set`
Classification	Axiom
Formula	0(ω set ) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`POmegaSetAx_prf`
Scheme of Types	0`(ω set)`
Kernel Note	Asserts that the ⊆-minimal successor-inductive (Peano-inductive) class ω is a set.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmOmegaIsSet`) → · (3.57) · `#AxmOmegaIsSet`

3.58

Title	Class of all sets is successor-inductive (Peano-inductive) `#ThmUniversalClassInductive` `#label-class-of-all-sets-is-successor-inductive-peano-inductive`
Classification	Theorem
Formula	0Ind(V) 0\(\href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(V)`
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassInductive`) → · (3.58) · `#ThmUniversalClassInductive`

3.59

Title	Intersection of all successor-inductive (Peano-inductive) classes is a successor-inductive class itself (ω is the ⊆-least successor-inductive class) `#ThmOmegaInductive` `#label-intersection-of-all-successor-inductive-peano-inductive-classes-is-a-successor-inductive-class-itself-is-the-least-successor-inductive-class`
Classification	Theorem
Formula	0Ind(ω) 0\(\href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(ω)`
Kernel Note	Establishes that ω itself satisfies Ind(ω), making ω the ⊆-least (minimal) element among all successor-inductive classes in the ⊆ order.
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaInductive`) → · (3.59) · `#ThmOmegaInductive`

3.60

Title	Class of all ordinal numbers is successor-inductive (Peano-inductive) `#ThmOrdinalsInductive` `#label-class-of-all-ordinal-numbers-is-successor-inductive-peano-inductive`
Classification	Theorem
Formula	0Ind(On) 0\(\href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsInductive`) → · (3.60) · `#ThmOrdinalsInductive`

3.61

Title	ω is transitive `#ThmOmegaTransitive` `#label-is-transitive`
Classification	Theorem
Formula	0Tr(ω) 0\(\href{../symbols/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpTrans`
Scheme of Types	0`Tr(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaTransitive`) → · (3.61) · `#ThmOmegaTransitive`

3.62

Title	ω is ordinal `#ThmOmegaOrdinal` `#label-is-ordinal`
Classification	Theorem
Formula	0Ord(ω) 0\(\href{../symbols/ord-pred.html}{\mathrm{Ord}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpOrd`
Scheme of Types	0`Ord(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaOrdinal`) → · (3.62) · `#ThmOmegaOrdinal`

3.63

Title	ω is in the class of all ordinal numbers(=sets) `#ThmOmegaInOrdinals` `#label-is-in-the-class-of-all-ordinal-numbers-sets`
Classification	Theorem
Formula	0(ω∈On) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/in-pred.html}{\in} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpOn`
Scheme of Types	0`(ω∈On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaInOrdinals`) → · (3.63) · `#ThmOmegaInOrdinals`

3.64

Title	“Is cardinal” predicate `#DefIsCardinal` `#label-is-cardinal-predicate`
Classification	Theorem
Formula	0(∀(C:Class)(Card(C)⟷(∃(K:Class)(\|K\|=C)))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{C} \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-pred.html}{\mathrm{Card}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{C} \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}{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/variables.html}{C} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`(∀([C@Variable]:[Class@Type])(Card([C@Class.Expression])⟷(∃([K@Variable]:[Class@Type])(\|[K@Class.Expression]\|=[C@Class.Expression]))))`
Verification	Verified (Kernel) · Standalone Entry (`DefIsCardinal`) → · (3.64) · `#DefIsCardinal`

3.65

Title	ω is cardinal `#ThmOmegaCardinal` `#label-is-cardinal`
Classification	Theorem
Formula	0Card(ω) 0\(\href{../symbols/card-pred.html}{\mathrm{Card}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`Card(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaCardinal`) → · (3.65) · `#ThmOmegaCardinal`

3.66

Title	On is a cardinal class `#ThmOrdinalsCardinal` `#label-on-is-a-cardinal-class`
Classification	Theorem
Formula	0Card(On) 0\(\href{../symbols/card-pred.html}{\mathrm{Card}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`Card(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsCardinal`) → · (3.66) · `#ThmOrdinalsCardinal`

3.67

Title	Class of all sets is not a cardinal class `#ThmUniversalClassNotCardinal` `#label-class-of-all-sets-is-not-a-cardinal-class`
Classification	Theorem
Formula	0(¬Card(V)) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/neg-conn.html}{\neg} \href{../symbols/card-pred.html}{\mathrm{Card}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`(¬Card(V))`
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassNotCardinal`) → · (3.67) · `#ThmUniversalClassNotCardinal`

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`

3.72

Title	Soundness of the theory 𝘛 `#AxmSoundnessOfBaseTheory` `#label-soundness-of-the-theory`
Classification	Axiom
Formula	0(∀(𝛗:Fm)((𝘛,[]⊢𝛗)→eval (𝛗))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-tau.html}{\mathcal{T}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/eval.html}{\mathsf{eval}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpHolds`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])((𝘛,[]⊢[𝛗@Fm.Expression])→eval([𝛗@Fm.Expression])))`
Kernel Note	Local reflection / soundness schema for the recursively enumerable (r.e.) base theory of classes 𝘛: if (𝘛, [] ⊢ φ), then the explicit formula valuation ⟦φ⟧ holds in the fixed background model.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmSoundnessOfBaseTheory`) → · (3.72) · `#AxmSoundnessOfBaseTheory`

3.73

Title	Soundness of the theory 𝘍 `#AxmSoundnessOfFullTheory` `#label-soundness-of-the-theory`
Classification	Axiom
Formula	0(∀(𝛗:Fm)((𝘍,[]⊢𝛗)→eval (𝛗))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/eval.html}{\mathsf{eval}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PCredo_prf`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])((𝘍,[]⊢[𝛗@Fm.Expression])→eval([𝛗@Fm.Expression])))`
Kernel Note	𝘍 is a non-recursively-enumerable (non-r.e.), Henkin-complete extension of the r.e. base theory 𝘛 (𝘛 ⊆ 𝘍). Because 𝘍 is non-r.e., Gödel's incompleteness theorems do not apply to 𝘍 itself, and 𝘍 is postulated with full soundness (𝘍, [] ⊢ φ) → ⟦φ⟧.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmSoundnessOfFullTheory`) → · (3.73) · `#AxmSoundnessOfFullTheory`

3.74

Title	Completeness of the theory 𝘍 `#AxmCompletenessOfFullTheory` `#label-completeness-of-the-theory`
Classification	Definition
Formula	0(∀(𝛗:Fm)(eval (𝛗)→(𝘍,[]⊢𝛗))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/eval.html}{\mathsf{eval}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`POmnis_prf`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])(eval([𝛗@Fm.Expression])→(𝘍,[]⊢[𝛗@Fm.Expression])))`
Kernel Note	Negation-completeness of the non-r.e. Henkin extension 𝘍: for every sentence φ, if ¬φ is not derivable in 𝘍, then φ is derivable in 𝘍.
Verification	Definitional (Kernel AST) · Standalone Entry (`AxmCompletenessOfFullTheory`) → · (3.74) · `#AxmCompletenessOfFullTheory`

3.75

Title	If a formula is derivable in 𝘛, then it is derivable in 𝘍 `#AxmBaseSubtheoryOfFull` `#label-if-a-formula-is-derivable-in-then-it-is-derivable-in`
Classification	Axiom
Formula	0(∀(Γ:Ctx)∀(𝛗:Fm)((𝘛,Γ⊢𝛗)→(𝘍,Γ⊢𝛗))) 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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-tau.html}{\mathcal{T}} \href{../symbols/comma-delim.html}{,} \href{../symbols/formula-metavariables.html}{\Gamma} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/formula-metavariables.html}{\Gamma} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpHolds`
Scheme of Types	0`(∀([Γ@Variable]:[Ctx@Type])∀([𝛗@Variable]:[Fm@Type])((𝘛,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])→(𝘍,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])))`
Kernel Note	Theory extension monotonicity (𝘛 ⊆ 𝘍): every theorem of the r.e. base theory 𝘛 is also a theorem of its non-r.e. Henkin completion 𝘍.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmBaseSubtheoryOfFull`) → · (3.75) · `#AxmBaseSubtheoryOfFull`

3.76

Title	Ordered pair(Dunaev's tagged class pair) `#DefDunaevOrderedPair` `#label-ordered-pair-dunaev-s-tagged-class-pair`
Classification	Definition
Formula	0(∀(A:Class)∀(B:Class)((A,B)=(({{∅,{∅}}}∪{x\|∃(a:Class)((a∈A)∧(x={{{{a}}},{∅}}))})∪({{∅,{∅,{∅}}}}∪{x\|∃(a:Class)((a∈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/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/comma-delim.html}{,} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/binunion-op.html}{\cup} \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}{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}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/binunion-op.html}{\cup} \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}{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}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.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	`CpOPair`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression],[B@Class.Expression])=(({{∅,{∅}}}∪{[x@Class.Expression]\|∃([a@Variable]:[Class@Type])(([a@Class.Expression]∈[A@Class.Expression])∧([x@Class.Expression]={{{{[a@Class.Expression]}}},{∅}}))})∪({{∅,{∅,{∅}}}}∪{[x@Class.Expression]\|∃([a@Variable]:[Class@Type])(([a@Class.Expression]∈[B@Class.Expression])∧([x@Class.Expression]={{{{[a@Class.Expression]}}},{∅,{∅}}}))}))))`
Kernel Note	Dunaev tagged class ordered pair (A,B) = mark(A,1) ∪ mark(B,2), sound for arbitrary proper classes.
Verification	Definitional (Kernel AST) · Standalone Entry (`DefDunaevOrderedPair`) → · (3.76) · `#DefDunaevOrderedPair`

3.77

Title	First projection of Dunaev's tagged ordered pair `#ThmDunaevFirstProjection` `#label-first-projection-of-dunaev-s-tagged-ordered-pair`
Classification	Theorem
Formula	0(∀(A:Class)∀(B:Class)({a\|{{{{a}}},{∅}}∈(A,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/class-comprehension.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/in-pred.html}{\in} \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/class-comprehension.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPr1`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])({[a@Class.Expression]\|{{{{[a@Class.Expression]}}},{∅}}∈([A@Class.Expression],[B@Class.Expression])}=[A@Class.Expression]))`
Kernel Note	Recovers A from (A,B) via tag 1 without requiring A or B to be sets.
Verification	Verified (Kernel) · Standalone Entry (`ThmDunaevFirstProjection`) → · (3.77) · `#ThmDunaevFirstProjection`

3.78

Title	Second projection of Dunaev's tagged ordered pair `#ThmDunaevSecondProjection` `#label-second-projection-of-dunaev-s-tagged-ordered-pair`
Classification	Theorem
Formula	0(∀(A:Class)∀(B:Class)({b\|{{{{b}}},{∅,{∅}}}∈(A,B)}=B)) 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/class-comprehension.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/in-pred.html}{\in} \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/class-comprehension.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPr2`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])({[b@Class.Expression]\|{{{{[b@Class.Expression]}}},{∅,{∅}}}∈([A@Class.Expression],[B@Class.Expression])}=[B@Class.Expression]))`
Kernel Note	Recovers B from (A,B) via tag 2 without requiring A or B to be sets.
Verification	Verified (Kernel) · Standalone Entry (`ThmDunaevSecondProjection`) → · (3.78) · `#ThmDunaevSecondProjection`