Symbol Reference: pr2 — Second Class-Pair Projection Functional Symbol (pr2, Entries DefDunaevOrderedPair (3.76) & ThmDunaevSecondProjection (3.78))

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

Formula Display:
Proof Trees:

pr2 \(\mathrm{pr}_2\) — Second Class-Pair Projection Functional Symbol (pr2, Entries DefDunaevOrderedPair (3.76) & ThmDunaevSecondProjection (3.78))

Unary functional symbol pr2(L) = {b | {{{{b}}}, 2} ∈ L} extracting the second component of a 3-layer marker-tagged Dunaev class-pair (Entries DefDunaevOrderedPair (3.76) 3.76, ThmDunaevSecondProjection (3.78) 3.78).

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

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