Lemma·L01
Characteristic property of ordered pairs
Two ordered pairs are equal exactly when their coordinates agree in order.
where
is the ordered pair of D010.
In words
Two ordered pairs are equal exactly when their first coordinates are equal and their second coordinates are equal.
Never needed: F05 · F08 · F10 · F11 · F12 · F13 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1The direction from right to left is immediate: if and , then and are built from equal ingredients, hence equal by substitutivity. For the converse, assume , that is, by D010.
- 2First suppose . Then by Extensionality, so , a set with the single member . Since , we get , hence . Since as well, , hence . Both coordinates agree.
- 3
- 4It remains to show . The member of equals or . If then , again contradicting . So using and substitutivity. Then gives or ; the first is excluded, so , completing the proof by cases (disjunction elimination).
∎
Remarks
This is the only fact about ordered pairs that the rest of the library uses; every later construction (products, relations, functions) depends on the coding solely through this lemma. The proof is pure bookkeeping with Extensionality and unordered pairs, and its fussiness is the price of encoding order into unordered sets.