DefClassLists (3.51, Definition): General definition of lists of classes which applicable not only for sets, but for proper classes too(TBI)

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

Formula Display:

Proof Trees:

DefClassLists (3.51) — General definition of lists of classes which applicable not only for sets, but for proper classes too(TBI)

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

Num Entity Database Record (Vertical Field Table)

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