ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$⋃ ⋂ (a, b) = a$ for all $a$ and $b$ , and $⋃ (a, b) = {a, b}$ , so both coordinates are recovered from the pair as a set

Example

For all sets $a$ and $b$ ,

$⋂ (a, b) = {a}, ⋃ ⋂ (a, b) = a, ⋃ (a, b) = {a, b},$

and the second coordinate is recovered as well: if $⋃ (a, b) ∖ ⋂ (a, b) = \emptyset$ then $b = a$ , and otherwise $b$ is the only element of that difference. Both coordinates are therefore determined by the pair as a set, by operations of the language alone.

Facts & Assumptions

Given: sets $a$ and $b$ .

[L1]

$(a, b) : = {{a}, {a, b}}$ (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ ).

[L2]

${x, y}$ is the set whose elements are exactly $x$ and $y$ , and ${x} : = {x, x}$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

[L3]

$⋃ {a} = a$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L4]

$⋂ {a, b} = a \cap b$ , and $z \in a \cap b$ holds if and only if $z \in a$ and $z \in b$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L5]

$⋃ {a, b} = a \cup b$ , and $z \in a \cup b$ holds if and only if $z \in a$ or $z \in b$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L6]

$z \in a ∖ b$ holds exactly when $z \in a$ and $z \notin b$ (The difference $a ∖ b$ , the symmetric difference $a △ b$ , and the complement $X ∖ a$ relative to a set $X$ ).

[L7]

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ).

[L8]

$(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ( $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ).

[L9]

There is exactly one set with no elements (There is exactly one set with no elements, written $\emptyset$ ).

[L10]

$⋃ x$ is the set whose elements are exactly the elements of the elements of $x$ , and $a \cup b : = ⋃ {a, b}$ (The union $⋃ x$ of a set, and the binary union $a \cup b : = ⋃ {a, b}$ ).

[L11]

For $x \neq \emptyset$ , $⋂ x$ is the set whose elements are exactly the sets belonging to every element of $x$ , and $a \cap b : = ⋂ {a, b}$ (The intersection $⋂ x$ of a nonempty set, the binary intersection $a \cap b : = ⋂ {a, b}$ , and disjointness).

Verification

technique · direct

1.1

$(a, b)$ is the unordered pair whose members are ${a}$ and ${a, b}$ , so $⋂ (a, b) = {a} \cap {a, b}$ ; and $z$ lies in that intersection exactly when $z = a$ , and $z = a$ or $z = b$ , which is exactly $z = a$ . Hence $⋂ (a, b) = {a}$ .

L1L2L4L7L11

1.2

Likewise $⋃ (a, b) = {a} \cup {a, b}$ , and $z$ lies in that union exactly when $z = a$ , or $z = a$ or $z = b$ , which is exactly $z = a$ or $z = b$ . Hence $⋃ (a, b) = {a, b}$ .

L1L2L5L7L10

2.1

Applying $⋃$ to step 1.1 gives $⋃ ⋂ (a, b) = ⋃ {a} = a$ , so the first coordinate is recovered.

L3step 1.1

2.2

By steps 1.1 and 1.2, $⋃ (a, b) ∖ ⋂ (a, b) = {a, b} ∖ {a}$ , whose elements are the $z$ with $z = a$ or $z = b$ , and $z \neq a$ ; that is, it is $\emptyset$ when $b = a$ and has $b$ as its only element when $b \neq a$ .

L2L6L7L9step 1.1step 1.2

3.1

Both coordinates are therefore determined by the set $(a, b)$ , which is the content of the characterising property made explicit.

L8step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ordered pair (Wikipedia) (standard reference, not scraped)
B. Kaya, MATH 320 Set Theory (METU), Def. 1 (standard reference, not scraped)
C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.6 (standard reference, not scraped)

⋃⋂(a,b)=a⋃⋂(a,b)=a for all aa and bb, and ⋃(a,b)={a,b}⋃(a,b)={a,b}, so both coordinates are recovered from the pair as a set