Symbol Reference: pr1 — First Class-Pair Projection Functional Symbol (pr1, Entries DefDunaevOrderedPair (3.76) & ThmDunaevFirstProjection (3.77))

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

pr1 \(\mathrm{pr}_1\) — First Class-Pair Projection Functional Symbol (pr1, Entries DefDunaevOrderedPair (3.76) & ThmDunaevFirstProjection (3.77))

Unary functional symbol pr1(L) = {a | {{{{a}}}, 1} ∈ L} extracting the first component of a 3-layer marker-tagged Dunaev class-pair (Entries DefDunaevOrderedPair (3.76) 3.76, ThmDunaevFirstProjection (3.77) 3.77).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
pr1
\(\mathrm{pr}_1\)
Category Functional Symbol (Unary Class Operator)
SML AST Constructor Pr1_def_entry [Defined Unary Functional Symbol, entries.ML:DefDunaevOrderedPair (3.76)]
Constructor Arguments 1. Dunaev class-pair L : Class
Metatype / Signature Class → Class
Binder Status No — Unary Functional Symbol (First Class-Pair Projection)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathrm{pr}_1
How to Understand It

SML AST Constructor & Proper-Class Examples: Decodes the tag-1 unordered payload sets {S_3(a), 1} = {{{{a}}}, {∅}} from D_mark(A, B). Holds unconditionally for arbitrary classes A, B : Class, including proper-class and empty components: pr1(D_mark(V, ∅)) = V and pr1(D_mark(∅, V)) = ∅.
Canonical Law / Usage pr1(D_mark(A, B)) = A (including pr1(D_mark(V, ∅)) = V)
Related Symbols & Kernel Entries