ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

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

Example

For all sets $a$ and $b$ ,

$\bigcap (a,b) = \{a\}, \qquad \bigcup \bigcap (a,b) = a, \qquad \bigcup (a,b) = \{a,b\},$

and the second coordinate is recovered as well: if $\bigcup(a,b) \setminus \bigcap(a,b) = \varnothing$ 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]

$\bigcup \{a\} = a$ ( $\bigcup \varnothing = \varnothing$ , $\bigcup \{a\} = a$ , $\bigcup \{a,b\} = a \cup b$ , $\bigcap \{a\} = a$ , and $\bigcap \{a,b\} = a \cap b$ ).

[L4]

$\bigcap \{a,b\} = a \cap b$ , and $z \in a \cap b$ holds if and only if $z \in a$ and $z \in b$ ( $\bigcup \varnothing = \varnothing$ , $\bigcup \{a\} = a$ , $\bigcup \{a,b\} = a \cup b$ , $\bigcap \{a\} = a$ , and $\bigcap \{a,b\} = a \cap b$ ).

[L5]

$\bigcup \{a,b\} = a \cup b$ , and $z \in a \cup b$ holds if and only if $z \in a$ or $z \in b$ ( $\bigcup \varnothing = \varnothing$ , $\bigcup \{a\} = a$ , $\bigcup \{a,b\} = a \cup b$ , $\bigcap \{a\} = a$ , and $\bigcap \{a,b\} = a \cap b$ ).

[L6]

$z \in a \setminus b$ holds exactly when $z \in a$ and $z \notin b$ (The difference $a \setminus b$ , the symmetric difference $a \triangle b$ , and the complement $X \setminus 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 $\varnothing$ ).

[L10]

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

[L11]

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

Verification

technique · direct

1.1

$(a,b)$ is the unordered pair whose members are $\{a\}$ and $\{a,b\}$ , so $\bigcap(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 $\bigcap(a,b) = \{a\}$ .

L1L2L4L7L11

1.2

Likewise $\bigcup(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 $\bigcup(a,b) = \{a,b\}$ .

L1L2L5L7L10

2.1

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

L3step 1.1

2.2

By steps 1.1 and 1.2, $\bigcup(a,b) \setminus \bigcap(a,b) = \{a,b\} \setminus \{a\}$ , whose elements are the $z$ with $z = a$ or $z = b$ , and $z \neq a$ ; that is, it is $\varnothing$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 16 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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\bigcup \bigcap (a,b) = a⋃⋂(a,b)=a for all aaa and bbb, and ⋃(a,b)={a,b}\bigcup(a,b) = \{a,b\}⋃(a,b)={a,b}, so both coordinates are recovered from the pair as a set