Let a and b are functions on a poset. Let a ∼ b iﬀ there exist an order isomorphism f such that
a = b ◦ f . Evidently ∼ is an equivalence r elation.
Obvious 33. concat a = concat b ⇔ uncurry(a) ∼ uncurry(b) for every ordinal indexed families a
and b of functions taking an ordinal number of arguments.
Thank to the above, we can reduce properties of concat to properties of uncurry.
Lemma 34. a ∼ b ⇒ uncurry a ∼ uncurry b for every ordinal indexed families a and b of functions
taking an ordinal number of arguments.
Proof. There exist an order isomorphism f such that a = b ◦ f.
uncurry(a)(x; y) = (ax)y = (bfx)y = uncurry(b)(fx; y) = uncurry(b)g(x; y) where g(x; y) = (fx;
y).
g is an order isomorphism because g(x
0
; y
0
) > g(x
1
; y
1
) ⇔ (x
0
; y
0
) > (x
1
; y
1
). (In jectivity and
surjectivity are obvious.)
Lemma 35. Let a
i
∼ b
i
where f
i
for every i. Then uncurry a ∼ uncurry b for every ordinal indexed
families a and b of ordinal indexed families of fu nc tio ns taking an ordinal number of arguments.
Proof. L e t a
i
= b
i
◦ f
i
where f
i
is an order isomorphism for every i.
uncurry(a)(i; y) = a
i
y = b
i
f
i
y = uncurry(b)(i; f
i
y) = uncurry(b)g(i; y) = (uncurry(b) ◦ g)(i; y)
where g(i; y) = (i; f
i
y).
g is an order isomorphism because g(i; y
0
) > g(i; y
1
) ⇔ f
i
y
0
> f
i
y
1
⇔ y
0
> y
1
and i
0
> i
1
⇒ g(i
0
;
y
0
) > g(i
1
; y
1
). (Injectivity and surjectivity are obvious.)
Let now S is an ordinal indexed family of ordinal indexed families of functions taking an ordinal
number of arguments.
Lemma 36. uncurry(uncurry ◦ S) ∼ uncurry(uncurry S).
Proof. uncurry ◦ S = λi ∈ S: uncurry(S
i
);
uncurry(uncurry ◦ S)(i; (x; y)) = (uncurry S
i
)(x; y) = (S
i
x)y;
(uncurry(uncurry S))((i; x); y) = ((uncurry S)(i; x))y = (S
i
x)y.
Thus uncurry(uncurry ◦ S)(i; (x; y)) = (uncurry(uncurry S))((i; x); y) and thus evidently
uncurry(uncurry ◦ S) ∼ uncurry(uncurry S).
Theorem 37. concat is an inﬁnitely associative function.
Proof. conc at(JxK) = x for a function x taking an ordinal number of argument is obvious. It is
remained to prove
concat(concat ◦ S) = concat(concat S);
We have, using the lemmas, concat(concat ◦ S) ∼ uncurry(concat ◦ S) ∼ (by lemma 35)∼
uncurry(uncurry ◦ S) ∼ uncurry(uncurry S) ∼ uncurry(concat S) ∼ concat(concat S).
Corollary 38. O rdinated product is an inﬁnitely a ssociative function.
Bib liography
[1] K. Ciesielski. Set Theory for the Working Mathematician. Cambridge, England: Cambridge University Press,
1997.
[2] J. E. Rubin. Set Theory for the Mathematician. New York: Holden-Day, 1967.
[3] P. Suppes. Axiomatic Set Theory. New York: Dover, 1972.
Bibliography 7