DefSigmaModel (3.38, Definition): “Dependent Sum (Sigma-Type)” model over a family

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

Formula Display:
Proof Trees:

DefSigmaModel (3.38) — “Dependent Sum (Sigma-Type)” model over a family

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

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