Definition·D011
Cartesian product
The set of all ordered pairs with first coordinate in A and second in B.
where
is the ordered pair.
In words
p belongs to the cartesian product of A and B exactly when there are some a and b with a from A and b from B and p equal to the ordered pair of a and b.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Existence: if
and
, then
and
are subsets of
(binary union as in D004, built by Union and Pairing), so both are members of
, so
is a subset of
, hence a member of
, with power sets provided by Power set. Separation then carves
out of
with the displayed property. The product is the stage on which relations and functions live.