| 3.01 |
| Title |
Class comprehension #RulClassComprehension #label-class-comprehension |
| Classification |
Inference Rule |
| Formula |
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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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 |
|
| 3.19 |
| Title |
Union of the elements of a class #DefUnaryUnion #label-union-of-the-elements-of-a-class |
| Classification |
Definition |
| Formula |
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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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 |
|
| 3.59 |
|
| 3.60 |
|
| 3.61 |
|
| 3.62 |
|
| 3.63 |
|
| 3.64 |
| Title |
βIs cardinalβ predicate #DefIsCardinal #label-is-cardinal-predicate |
| Classification |
Theorem |
| Formula |
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 |
|
| 3.66 |
|
| 3.67 |
|
| 3.68 |
| Title |
βIs a universeβ predicate #DefGrothendieckUniverse #label-is-a-universe-predicate |
| Classification |
Definition |
| Formula |
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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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\(\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 |
|