IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory func_ZF_1 imports ZF.Order Order_ZF_1a func_ZF
begin

In this theory we consider some properties of functions related to order relations

Functions and order

This section deals with functions between ordered sets.

If every value of a function on a set is bounded below by a constant, then the image of the set is bounded below.

lemma func_ZF_8_L1:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle L,f(x)\rangle \in r \)

shows \( \text{IsBoundedBelow}(f(A),r) \)proof
from assms have \( \forall y \in f(A).\ \langle L,y\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedBelow}(f(A),r) \) by (rule Order_ZF_3_L9 )
qed

If every value of a function on a set is bounded above by a constant, then the image of the set is bounded above.

lemma func_ZF_8_L2:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle f(x),U\rangle \in r \)

shows \( \text{IsBoundedAbove}(f(A),r) \)proof
from assms have \( \forall y \in f(A).\ \langle y,U\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedAbove}(f(A),r) \) by (rule Order_ZF_3_L10 )
qed

Identity is an order isomorphism.

lemma id_ord_iso:

shows \( id(X) \in ord\_iso(X,r,X,r) \) using id_bij, id_def, ord_iso_def

Identity is the only order automorphism of a singleton.

lemma id_ord_auto_singleton:

shows \( ord\_iso(\{x\},r,\{x\},r) = \{id(\{x\})\} \) using id_ord_iso, ord_iso_def, single_bij_id

The image of a maximum by an order isomorphism is a maximum. Note that from the fact the \(r\) is antisymmetric and \(f\) is an order isomorphism between \((A,r)\) and \((B,R)\) we can not conclude that \(R\) is antisymmetric (we can only show that \(R\cap (B\times B)\) is).

lemma max_image_ord_iso:

assumes A1: \( \text{antisym}(r) \) and A2: \( \text{antisym}(R) \) and A3: \( f \in ord\_iso(A,r,B,R) \) and A4: \( \text{HasAmaximum}(r,A) \)

shows \( \text{HasAmaximum}(R,B) \) and \( \text{Maximum}(R,B) = f( \text{Maximum}(r,A)) \)proof
let \( M = \text{Maximum}(r,A) \)
from A1, A4 have \( M \in A \) using Order_ZF_4_L3
from A3 have \( f:A\rightarrow B \) using ord_iso_def, bij_is_fun
with \( M \in A \) have I: \( f(M) \in B \) using apply_funtype
{
fix \( y \)
assume \( y \in B \)
let \( x = converse(f)(y) \)
from A3 have \( converse(f) \in ord\_iso(B,R,A,r) \) using ord_iso_sym
then have \( converse(f): B \rightarrow A \) using ord_iso_def, bij_is_fun
with \( y \in B \) have \( x \in A \)
with A1, A3, A4, \( x \in A \), \( M \in A \) have \( \langle f(x), f(M)\rangle \in R \) using Order_ZF_4_L3, ord_iso_apply
with A3, \( y \in B \) have \( \langle y, f(M)\rangle \in R \) using right_inverse_bij, ord_iso_def
}
then have II: \( \forall y \in B.\ \langle y, f(M)\rangle \in R \)
with A2, I show \( \text{Maximum}(R,B) = f(M) \) by (rule Order_ZF_4_L14 )
from I, II show \( \text{HasAmaximum}(R,B) \) using HasAmaximum_def
qed

Maximum is a fixpoint of order automorphism.

lemma max_auto_fixpoint:

assumes \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,A,r) \) and \( \text{HasAmaximum}(r,A) \)

shows \( \text{Maximum}(r,A) = f( \text{Maximum}(r,A)) \) using assms, max_image_ord_iso

If two sets are order isomorphic and we remove \(x\) and \(f(x)\), respectively, from the sets, then they are still order isomorphic.

lemma ord_iso_rem_point:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( a \in A \)

shows \( \text{restrict}(f,A-\{a\}) \in ord\_iso(A-\{a\},r,B-\{f(a)\},R) \)proof
let \( f_0 = \text{restrict}(f,A-\{a\}) \)
have \( A-\{a\} \subseteq A \)
with A1 have \( f_0 \in ord\_iso(A-\{a\},r,f(A-\{a\}),R) \) using ord_iso_restrict_image
moreover
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_def, bij_def
with A2 have \( f(A-\{a\}) = f(A) - f\{a\} \) using inj_image_dif
moreover
from A1 have \( f(A) = B \) using ord_iso_def, bij_def, surj_range_image_domain
moreover
from A1 have \( f: A\rightarrow B \) using ord_iso_def, bij_is_fun
with A2 have \( f\{a\} = \{f(a)\} \) using singleton_image
ultimately show \( thesis \)
qed

If two sets are order isomorphic and we remove maxima from the sets, then they are still order isomorphic.

corollary ord_iso_rem_max:

assumes A1: \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,B,R) \) and A4: \( \text{HasAmaximum}(r,A) \) and A5: \( M = \text{Maximum}(r,A) \)

shows \( \text{restrict}(f,A-\{M\}) \in ord\_iso(A-\{M\}, r, B-\{f(M)\},R) \) using assms, Order_ZF_4_L3, ord_iso_rem_point

Lemma about extending order isomorphisms by adding one point to the domain.

lemma ord_iso_extend:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( M_A \notin A \), \( M_B \notin B \) and A3: \( \forall a\in A.\ \langle a, M_A\rangle \in r \), \( \forall b\in B.\ \langle b, M_B\rangle \in R \) and A4: \( \text{antisym}(r) \), \( \text{antisym}(R) \) and A5: \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \)

shows \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \)proof
let \( g = f \cup \{\langle M_A,M_B\rangle \} \)
from A1, A2 have \( g : A\cup \{M_A\} \rightarrow B\cup \{M_B\} \) and I: \( \forall x\in A.\ g(x) = f(x) \) and II: \( g(M_A) = M_B \) using ord_iso_def, bij_def, inj_def, func1_1_L11D
from A1, A2 have \( g \in \text{bij}(A\cup \{M_A\},B\cup \{M_B\}) \) using ord_iso_def, bij_extend_point
moreover
have \( \forall x \in A\cup \{M_A\}.\ \forall y \in A\cup \{M_A\}.\ \) \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)proof
{
fix \( x \) \( y \)
assume \( x \in A\cup \{M_A\} \) and \( y \in A\cup \{M_A\} \)
then have \( x\in A \wedge y \in A \vee x\in A \wedge y = M_A \vee \) \( x = M_A \wedge y \in A \vee x = M_A \wedge y = M_A \)
moreover {
assume \( x\in A \wedge y \in A \)
with A1, I have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \) using ord_iso_def
} moreover {
assume \( x\in A \wedge y = M_A \)
with A1, A3, I, II have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \) using ord_iso_def, bij_def, inj_def, apply_funtype
} moreover {
assume \( x = M_A \wedge y \in A \)
with A2, A3, A4 have \( \langle x,y\rangle \notin r \) using antisym_def
moreover {
assume A6: \( \langle g(x), g(y)\rangle \in R \)
from A1, I, II, \( x = M_A \wedge y \in A \) have III: \( g(y) \in B \), \( g(x) = M_B \) using ord_iso_def, bij_def, inj_def, apply_funtype
with A3 have \( \langle g(y), g(x)\rangle \in R \)
with A4, A6 have \( g(y) = g(x) \) using antisym_def
with A2, III have \( False \)
}
hence \( \langle g(x), g(y)\rangle \notin R \)
ultimately have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
} moreover {
assume \( x = M_A \wedge y = M_A \)
with A5, II have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
} ultimately have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
}
thus \( thesis \)
qed
ultimately show \( thesis \) using ord_iso_def
qed

A kind of converse to ord_iso_rem_max: if two linearly ordered sets sets are order isomorphic after removing the maxima, then they are order isomorphic.

lemma rem_max_ord_iso:

assumes A1: \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and A2: \( \text{HasAmaximum}(r,X) \), \( \text{HasAmaximum}(R,Y) \), \( ord\_iso(X - \{ \text{Maximum}(r,X)\},r,Y - \{ \text{Maximum}(R,Y)\},R) \neq 0 \)

shows \( ord\_iso(X,r,Y,R) \neq 0 \)proof
let \( M_A = \text{Maximum}(r,X) \)
let \( A = X - \{M_A\} \)
let \( M_B = \text{Maximum}(R,Y) \)
let \( B = Y - \{M_B\} \)
from A2 obtain \( f \) where \( f \in ord\_iso(A,r,B,R) \)
moreover
have \( M_A \notin A \) and \( M_B \notin B \)
moreover
from A1, A2 have \( \forall a\in A.\ \langle a,M_A\rangle \in r \) and \( \forall b\in B.\ \langle b,M_B\rangle \in R \) using IsLinOrder_def, Order_ZF_4_L3
moreover
from A1 have \( \text{antisym}(r) \) and \( \text{antisym}(R) \) using IsLinOrder_def
moreover
from A1, A2 have \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \) using IsLinOrder_def, Order_ZF_4_L3, IsLinOrder_def, total_is_refl, refl_def
ultimately have \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \) by (rule ord_iso_extend )
moreover
from A1, A2 have \( A\cup \{M_A\} = X \) and \( B\cup \{M_B\} = Y \) using IsLinOrder_def, Order_ZF_4_L3
ultimately show \( ord\_iso(X,r,Y,R) \neq 0 \) using ord_iso_extend
qed

Functions in cartesian products

In this section we consider maps arising naturally in cartesian products.

There is a natural bijection etween \(X=Y\times \{ y\}\) (a "slice") and \(Y\). We will call this the \( \text{SliceProjection}(Y\times \{y\}) \). This is really the ZF equivalent of the meta-function \( \text{fst}(x) \).

definition

\( \text{SliceProjection}(X) \equiv \{\langle p,\text{fst}(p)\rangle .\ p \in X \} \)

A slice projection is a bijection between \(X\times\{ y\}\) and \(X\).

lemma slice_proj_bij:

shows \( \text{SliceProjection}(X\times \{y\}): X\times \{y\} \rightarrow X \), \( domain( \text{SliceProjection}(X\times \{y\})) = X\times \{y\} \), \( \forall p\in X\times \{y\}.\ \text{SliceProjection}(X\times \{y\})(p) = \text{fst}(p) \), \( \text{SliceProjection}(X\times \{y\}) \in \text{bij}(X\times \{y\},X) \)proof
let \( P = \text{SliceProjection}(X\times \{y\}) \)
have \( \forall p \in X\times \{y\}.\ \text{fst}(p) \in X \)
moreover
from this have \( \{\langle p,\text{fst}(p)\rangle .\ p \in X\times \{y\} \} : X\times \{y\} \rightarrow X \) by (rule ZF_fun_from_total )
ultimately show I: \( P: X\times \{y\} \rightarrow X \) and II: \( \forall p\in X\times \{y\}.\ P(p) = \text{fst}(p) \) using ZF_fun_from_tot_val, SliceProjection_def
hence \( \forall a \in X\times \{y\}.\ \forall b \in X\times \{y\}.\ P(a) = P(b) \longrightarrow a=b \)
with I have \( P \in \text{inj}(X\times \{y\},X) \) using inj_def
moreover
from II have \( \forall x\in X.\ \exists p\in X\times \{y\}.\ P(p) = x \)
with I have \( P \in \text{surj}(X\times \{y\},X) \) using surj_def
ultimately show \( P \in \text{bij}(X\times \{y\},X) \) using bij_def
from I show \( domain( \text{SliceProjection}(X\times \{y\})) = X\times \{y\} \) using func1_1_L1
qed

Given 2 functions \(f:A\to B\) and \(g:C\to D\) , we can consider a function \(h:A\times C \to B\times D\) such that \(h(x,y)=\langle f(x),g(y)\rangle\)

definition

\( \text{ProdFunction}(f,g) \equiv \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in domain(f)\times domain(g)\} \)

For given functions \(f:A\to B\) and \(g:C\to D\) the function \( \text{ProdFunction}(f,g) \) maps \(A\times C\) to \(B\times D\).

lemma prodFunction:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \)

shows \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \)proof
from assms have \( \forall z \in domain(f)\times domain(g).\ \langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \in B\times D \) using func1_1_L1, apply_type
with assms show \( thesis \) unfolding ProdFunction_def using func1_1_L1, ZF_fun_from_total
qed

For given functions \(f:A\to B\) and \(g:C\to D\) and points \(x\in A\), \(y\in C\) the value of the function \( \text{ProdFunction}(f,g) \) on \(\langle x,y \rangle\) is \(\langle f(x),g(y) \rangle\).

lemma prodFunctionApp:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \), \( x\in A \), \( y\in C \)

shows \( \text{ProdFunction}(f,g)\langle x,y\rangle = \langle f(x),g(y)\rangle \)proof
let \( z = \langle x,y\rangle \)
from assms have \( z \in A\times C \) and \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \) using prodFunction
moreover
from assms(1,2) have \( \text{ProdFunction}(f,g) = \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in A\times C\} \) unfolding ProdFunction_def using func1_1_L1
ultimately show \( thesis \) using ZF_fun_from_tot_val
qed

Somewhat technical lemma about inverse image of a set by a \( \text{ProdFunction}(f,f) \).

lemma prodFunVimage:

assumes \( x\in X \), \( f:X\rightarrow Y \)

shows \( \langle x,t\rangle \in \text{ProdFunction}(f,f)^{-1}(V) \longleftrightarrow t\in X \wedge \langle fx,ft\rangle \in V \)proof
from assms(2) have T: \( \text{ProdFunction}(f,f)^{-1}(V) = \{z \in X\times X.\ \text{ProdFunction}(f,f)(z) \in V\} \) using prodFunction, func1_1_L15
with assms show \( thesis \) using prodFunctionApp
qed

Induced relations and order isomorphisms

When we have two sets \(X,Y\), function \(f:X\rightarrow Y\) and a relation \(R\) on \(Y\) we can define a relation \(r\) on \(X\) by saying that \(x\ r\ y\) if and only if \(f(x) \ R \ f(y)\). This is especially interesting when \(f\) is a bijection as all reasonable properties of \(R\) are inherited by \(r\). This section treats mostly the case when \(R\) is an order relation and \(f\) is a bijection. The standard Isabelle's Order theory defines the notion of a space of order isomorphisms between two sets relative to a relation. We expand that material proving that order isomrphisms preserve interesting properties of the relation.

We call the relation created by a relation on \(Y\) and a mapping \(f:X\rightarrow Y\) the \( \text{InducedRelation}(f,R) \).

definition

\( \text{InducedRelation}(f,R) \equiv \) \( \{p \in domain(f)\times domain(f).\ \langle f(\text{fst}(p)),f(\text{snd}(p))\rangle \in R\} \)

A reformulation of the definition of the relation induced by a function.

lemma def_of_ind_relA:

assumes \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)

shows \( \langle f(x),f(y)\rangle \in R \) using assms, InducedRelation_def

A reformulation of the definition of the relation induced by a function, kind of converse of def_of_ind_relA.

lemma def_of_ind_relB:

assumes \( f:A\rightarrow B \) and \( x\in A \), \( y\in A \) and \( \langle f(x),f(y)\rangle \in R \)

shows \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \) using assms, func1_1_L1, InducedRelation_def

A property of order isomorphisms that is missing from standard Isabelle's Order.thy.

lemma ord_iso_apply_conv:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( \langle f(x),f(y)\rangle \in R \) and \( x\in A \), \( y\in A \)

shows \( \langle x,y\rangle \in r \) using assms, ord_iso_def

The next lemma tells us where the induced relation is defined

lemma ind_rel_domain:

assumes \( R \subseteq B\times B \) and \( f:A\rightarrow B \)

shows \( \text{InducedRelation}(f,R) \subseteq A\times A \) using assms, func1_1_L1, InducedRelation_def

A bijection is an order homomorphisms between a relation and the induced one.

lemma bij_is_ord_iso:

assumes A1: \( f \in \text{bij}(A,B) \)

shows \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \)proof
let \( r = \text{InducedRelation}(f,R) \)
{
fix \( x \) \( y \)
assume A2: \( x\in A \), \( y\in A \)
have \( \langle x,y\rangle \in r \longleftrightarrow \langle f(x),f(y)\rangle \in R \)proof
assume \( \langle x,y\rangle \in r \)
then show \( \langle f(x),f(y)\rangle \in R \) using def_of_ind_relA
next
assume \( \langle f(x),f(y)\rangle \in R \)
with A1, A2 show \( \langle x,y\rangle \in r \) using bij_is_fun, def_of_ind_relB
qed
}
with A1 show \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \) using ord_isoI
qed

An order isomoprhism preserves antisymmetry.

lemma ord_iso_pres_antsym:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{antisym}(R) \)

shows \( \text{antisym}(r) \)proof
{
fix \( x \) \( y \)
assume A4: \( \langle x,y\rangle \in r \), \( \langle y,x\rangle \in r \)
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
moreover
from A1, A2, A4 have \( \langle f(x), f(y)\rangle \in R \) and \( \langle f(y), f(x)\rangle \in R \) using ord_iso_apply
with A3 have \( f(x) = f(y) \) by (rule Fol1_L4 )
moreover
from A2, A4 have \( x\in A \), \( y\in A \)
ultimately have \( x=y \) by (rule inj_apply_equality )
}
then have \( \forall x y.\ \langle x,y\rangle \in r \wedge \langle y,x\rangle \in r \longrightarrow x=y \)
then show \( \text{antisym}(r) \) using imp_conj, antisym_def
qed

Order isomoprhisms preserve transitivity.

lemma ord_iso_pres_trans:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{trans}(R) \)

shows \( \text{trans}(r) \)proof
{
fix \( x \) \( y \) \( z \)
assume A4: \( \langle x, y\rangle \in r \), \( \langle y, z\rangle \in r \)
note A1
moreover
from A1, A2, A4 have \( \langle f(x), f(y)\rangle \in R \wedge \langle f(y), f(z)\rangle \in R \) using ord_iso_apply
with A3 have \( \langle f(x),f(z)\rangle \in R \) by (rule Fol1_L3 )
moreover
from A2, A4 have \( x\in A \), \( z\in A \)
ultimately have \( \langle x, z\rangle \in r \) using ord_iso_apply_conv
}
then have \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)
then show \( \text{trans}(r) \) by (rule Fol1_L2 )
qed

Order isomorphisms preserve totality.

lemma ord_iso_pres_tot:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( R \text{ is total on } B \)

shows \( r \text{ is total on } A \)proof
{
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \), \( \langle x,y\rangle \notin r \)
with A1 have \( \langle f(x),f(y)\rangle \notin R \) using ord_iso_apply_conv
moreover
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
with A3, \( x\in A \), \( y\in A \) have \( \langle f(x),f(y)\rangle \in R \vee \langle f(y),f(x)\rangle \in R \) using apply_funtype, IsTotal_def
ultimately have \( \langle f(y),f(x)\rangle \in R \)
with A1, \( x\in A \), \( y\in A \) have \( \langle y,x\rangle \in r \) using ord_iso_apply_conv
}
then have \( \forall x\in A.\ \forall y\in A.\ \langle x,y\rangle \in r \vee \langle y,x\rangle \in r \)
then show \( r \text{ is total on } A \) using IsTotal_def
qed

Order isomorphisms preserve linearity.

lemma ord_iso_pres_lin:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsLinOrder}(B,R) \)

shows \( \text{IsLinOrder}(A,r) \) using assms, ord_iso_pres_antsym, ord_iso_pres_trans, ord_iso_pres_tot, IsLinOrder_def

If a relation is a linear order, then the relation induced on another set by a bijection is also a linear order.

lemma ind_rel_pres_lin:

assumes A1: \( f \in \text{bij}(A,B) \) and A2: \( \text{IsLinOrder}(B,R) \)

shows \( \text{IsLinOrder}(A, \text{InducedRelation}(f,R)) \)proof
let \( r = \text{InducedRelation}(f,R) \)
from A1 have \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) using bij_is_ord_iso, domain_of_bij, InducedRelation_def
with A2 show \( \text{IsLinOrder}(A,r) \) using ord_iso_pres_lin
qed

The image by an order isomorphism of a bounded above and nonempty set is bounded above.

lemma ord_iso_pres_bound_above:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)

shows \( \text{IsBoundedAbove}(f(C),R) \), \( f(C) \neq 0 \)proof
from A3 obtain \( u \) where I: \( \forall x\in C.\ \langle x,u\rangle \in r \) using IsBoundedAbove_def
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
from A2, A3 have \( C\subseteq A \) using Order_ZF_3_L1A
from A3 obtain \( x \) where \( x\in C \)
with A2, I have \( u\in A \)
{
fix \( y \)
assume \( y \in f(C) \)
with \( f:A\rightarrow B \), \( C\subseteq A \) obtain \( x \) where \( x\in C \) and \( y = f(x) \) using func_imagedef
with A1, I, \( C\subseteq A \), \( u\in A \) have \( \langle y,f(u)\rangle \in R \) using ord_iso_apply
}
then have \( \forall y \in f(C).\ \langle y,f(u)\rangle \in R \)
then show \( \text{IsBoundedAbove}(f(C),R) \) by (rule Order_ZF_3_L10 )
from A3, \( f:A\rightarrow B \), \( C\subseteq A \) show \( f(C) \neq 0 \) using func1_1_L15A
qed

Order isomorphisms preserve the property of having a minimum.

lemma ord_iso_pres_has_min:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( C\subseteq A \) and A4: \( \text{HasAminimum}(R,f(C)) \)

shows \( \text{HasAminimum}(r,C) \)proof
from A4 obtain \( m \) where I: \( m \in f(C) \) and II: \( \forall y \in f(C).\ \langle m,y\rangle \in R \) using HasAminimum_def
let \( k = converse(f)(m) \)
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
with A3, I have \( k \in C \) and III: \( f(k) = m \) using inj_inv_back_in_set
moreover {
fix \( x \)
assume A5: \( x\in C \)
with A3, II, \( f:A\rightarrow B \), \( k \in C \), III have \( k \in A \), \( x\in A \), \( \langle f(k),f(x)\rangle \in R \) using func_imagedef
with A1 have \( \langle k,x\rangle \in r \) using ord_iso_apply_conv
}
then have \( \forall x\in C.\ \langle k,x\rangle \in r \)
ultimately show \( \text{HasAminimum}(r,C) \) using HasAminimum_def
qed

Order isomorhisms preserve the images of relations. In other words taking the image of a point by a relation commutes with the function.

lemma ord_iso_pres_rel_image:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( a\in A \)

shows \( f(r\{a\}) = R\{f(a)\} \)proof
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
moreover
from A2, A3 have I: \( r\{a\} \subseteq A \)
ultimately have I: \( f(r\{a\}) = \{f(x).\ x \in r\{a\} \} \) using func_imagedef
{
fix \( y \)
assume A4: \( y \in f(r\{a\}) \)
with I obtain \( x \) where \( x \in r\{a\} \) and II: \( y = f(x) \)
with A1, A2 have \( \langle f(a),f(x)\rangle \in R \) using ord_iso_apply
with II have \( y \in R\{f(a)\} \)
}
then show \( f(r\{a\}) \subseteq R\{f(a)\} \)
{
fix \( y \)
assume A5: \( y \in R\{f(a)\} \)
let \( x = converse(f)(y) \)
from A2, A5 have \( \langle f(a),y\rangle \in R \), \( f(a) \in B \) and IV: \( y\in B \)
with A1 have III: \( \langle converse(f)(f(a)),x\rangle \in r \) using ord_iso_converse
moreover
from A1, A3 have \( converse(f)(f(a)) = a \) using ord_iso_is_bij, left_inverse_bij
ultimately have \( f(x) \in \{f(x).\ x \in r\{a\} \} \)
moreover
from A1, IV have \( f(x) = y \) using ord_iso_is_bij, right_inverse_bij
moreover
from A1, I have \( f(r\{a\}) = \{f(x).\ x \in r\{a\} \} \) using ord_iso_is_bij, bij_is_fun, func_imagedef
ultimately have \( y \in f(r\{a\}) \)
}
then show \( R\{f(a)\} \subseteq f(r\{a\}) \)
qed

Order isomorphisms preserve collections of upper bounds.

lemma ord_iso_pres_up_bounds:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( C\subseteq A \)

shows \( \{f(r\{a\}).\ a\in C\} = \{R\{b\}.\ b \in f(C)\} \)proof
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
{
fix \( Y \)
assume \( Y \in \{f(r\{a\}).\ a\in C\} \)
then obtain \( a \) where \( a\in C \) and I: \( Y = f(r\{a\}) \)
from A3, \( a\in C \) have \( a\in A \)
with A1, A2 have \( f(r\{a\}) = R\{f(a)\} \) using ord_iso_pres_rel_image
moreover
from A3, \( f:A\rightarrow B \), \( a\in C \) have \( f(a) \in f(C) \) using func_imagedef
ultimately have \( f(r\{a\}) \in \{ R\{b\}.\ b \in f(C) \} \)
with I have \( Y \in \{ R\{b\}.\ b \in f(C) \} \)
}
then show \( \{f(r\{a\}).\ a\in C\} \subseteq \{R\{b\}.\ b \in f(C)\} \)
{
fix \( Y \)
assume \( Y \in \{R\{b\}.\ b \in f(C)\} \)
then obtain \( b \) where \( b \in f(C) \) and II: \( Y = R\{b\} \)
with A3, \( f:A\rightarrow B \) obtain \( a \) where \( a\in C \) and \( b = f(a) \) using func_imagedef
with A3, II have \( a\in A \) and \( Y = R\{f(a)\} \)
with A1, A2 have \( Y = f(r\{a\}) \) using ord_iso_pres_rel_image
with \( a\in C \) have \( Y \in \{f(r\{a\}).\ a\in C\} \)
}
then show \( \{R\{b\}.\ b \in f(C)\} \subseteq \{f(r\{a\}).\ a\in C\} \)
qed

The image of the set of upper bounds is the set of upper bounds of the image.

lemma ord_iso_pres_min_up_bounds:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( C\subseteq A \) and A4: \( C\neq 0 \)

shows \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \)proof
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
moreover
note A4
moreover
from A2, A3 have \( \forall a\in C.\ r\{a\} \subseteq A \)
ultimately have \( f(\bigcap a\in C.\ r\{a\}) = ( \bigcap a\in C.\ f(r\{a\}) ) \) using inj_image_of_Inter
also
from A1, A2, A3 have \( ( \bigcap a\in C.\ f(r\{a\}) ) = ( \bigcap b\in f(C).\ R\{b\} ) \) using ord_iso_pres_up_bounds
finally show \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \)
qed

Order isomorphisms preserve completeness.

lemma ord_iso_pres_compl:

assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( R \text{ is complete } \)

shows \( r \text{ is complete } \)proof
{
fix \( C \)
assume A4: \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)
with A1, A2, A3 have \( \text{HasAminimum}(R,\bigcap b \in f(C).\ R\{b\}) \) using ord_iso_pres_bound_above, IsComplete_def
moreover
from A2, \( \text{IsBoundedAbove}(C,r) \) have I: \( C \subseteq A \) using Order_ZF_3_L1A
with A1, A2, \( C\neq 0 \) have \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \) using ord_iso_pres_min_up_bounds
ultimately have \( \text{HasAminimum}(R,f(\bigcap a\in C.\ r\{a\})) \)
moreover
from A2 have \( \forall a\in C.\ r\{a\} \subseteq A \)
with \( C\neq 0 \) have \( ( \bigcap a\in C.\ r\{a\} ) \subseteq A \) using ZF1_1_L7
moreover
note A1, A2
ultimately have \( \text{HasAminimum}(r, \bigcap a\in C.\ r\{a\} ) \) using ord_iso_pres_has_min
}
then show \( r \text{ is complete } \) using IsComplete_def
qed

If the original relation is complete, then the induced one is complete.

lemma ind_rel_pres_compl:

assumes A1: \( f \in \text{bij}(A,B) \) and A2: \( R \subseteq B\times B \) and A3: \( R \text{ is complete } \)

shows \( \text{InducedRelation}(f,R) \text{ is complete } \)proof
let \( r = \text{InducedRelation}(f,R) \)
from A1 have \( f \in ord\_iso(A,r,B,R) \) using bij_is_ord_iso
moreover
from A1, A2 have \( r \subseteq A\times A \) using bij_is_fun, ind_rel_domain
moreover
note A2, A3
ultimately show \( r \text{ is complete } \) using ord_iso_pres_compl
qed
end
lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma Order_ZF_3_L9:

assumes \( \forall a\in A.\ \langle l,a\rangle \in r \)

shows \( \text{IsBoundedBelow}(A,r) \)
lemma Order_ZF_3_L10:

assumes \( \forall a\in A.\ \langle a,u\rangle \in r \)

shows \( \text{IsBoundedAbove}(A,r) \)
lemma id_ord_iso: shows \( id(X) \in ord\_iso(X,r,X,r) \)
lemma single_bij_id: shows \( \text{bij}(\{x\},\{x\}) = \{id(\{x\})\} \)
lemma Order_ZF_4_L3:

assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)

shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \)
lemma Order_ZF_4_L14:

assumes \( \text{antisym}(r) \) and \( M \in A \) and \( \forall a\in A.\ \langle a,M\rangle \in r \)

shows \( \text{Maximum}(r,A) = M \)
Definition of HasAmaximum: \( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
lemma max_image_ord_iso:

assumes \( \text{antisym}(r) \) and \( \text{antisym}(R) \) and \( f \in ord\_iso(A,r,B,R) \) and \( \text{HasAmaximum}(r,A) \)

shows \( \text{HasAmaximum}(R,B) \) and \( \text{Maximum}(R,B) = f( \text{Maximum}(r,A)) \)
lemma inj_image_dif:

assumes \( f \in \text{inj}(A,B) \) and \( C \subseteq A \)

shows \( f(A\setminus C) = f(A)\setminus f(C) \)
lemma surj_range_image_domain:

assumes \( f \in \text{surj}(A,B) \)

shows \( f(A) = B \)
lemma singleton_image:

assumes \( f\in X\rightarrow Y \) and \( x\in X \)

shows \( f\{x\} = \{f(x)\} \)
lemma ord_iso_rem_point:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( a \in A \)

shows \( \text{restrict}(f,A-\{a\}) \in ord\_iso(A-\{a\},r,B-\{f(a)\},R) \)
lemma func1_1_L11D:

assumes \( f:X\rightarrow Y \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \)

shows \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \), \( \forall x\in X.\ g(x) = f(x) \), \( g(a) = b \)
lemma bij_extend_point:

assumes \( f \in \text{bij}(X,Y) \), \( a\notin X \), \( b\notin Y \)

shows \( (f \cup \{\langle a,b\rangle \}) \in \text{bij}(X\cup \{a\},Y\cup \{b\}) \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma total_is_refl:

assumes \( r \text{ is total on } X \)

shows \( \text{refl}(X,r) \)
lemma ord_iso_extend:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( M_A \notin A \), \( M_B \notin B \) and \( \forall a\in A.\ \langle a, M_A\rangle \in r \), \( \forall b\in B.\ \langle b, M_B\rangle \in R \) and \( \text{antisym}(r) \), \( \text{antisym}(R) \) and \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \)

shows \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \) and \( b(x)\in Y \)
Definition of SliceProjection: \( \text{SliceProjection}(X) \equiv \{\langle p,\text{fst}(p)\rangle .\ p \in X \} \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
Definition of ProdFunction: \( \text{ProdFunction}(f,g) \equiv \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in domain(f)\times domain(g)\} \)
lemma prodFunction:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \)

shows \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \)
lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)
lemma prodFunctionApp:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \), \( x\in A \), \( y\in C \)

shows \( \text{ProdFunction}(f,g)\langle x,y\rangle = \langle f(x),g(y)\rangle \)
Definition of InducedRelation: \( \text{InducedRelation}(f,R) \equiv \) \( \{p \in domain(f)\times domain(f).\ \langle f(\text{fst}(p)),f(\text{snd}(p))\rangle \in R\} \)
lemma def_of_ind_relA:

assumes \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)

shows \( \langle f(x),f(y)\rangle \in R \)
lemma def_of_ind_relB:

assumes \( f:A\rightarrow B \) and \( x\in A \), \( y\in A \) and \( \langle f(x),f(y)\rangle \in R \)

shows \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)
lemma Fol1_L4:

assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)

shows \( a=b \)
lemma Fol1_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)

shows \( \langle a,c\rangle \in r \)
lemma ord_iso_apply_conv:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( \langle f(x),f(y)\rangle \in R \) and \( x\in A \), \( y\in A \)

shows \( \langle x,y\rangle \in r \)
lemma Fol1_L2:

assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)

shows \( \text{trans}(r) \)
Definition of IsTotal: \( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
lemma ord_iso_pres_antsym:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{antisym}(R) \)

shows \( \text{antisym}(r) \)
lemma ord_iso_pres_trans:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{trans}(R) \)

shows \( \text{trans}(r) \)
lemma ord_iso_pres_tot:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( R \text{ is total on } B \)

shows \( r \text{ is total on } A \)
lemma bij_is_ord_iso:

assumes \( f \in \text{bij}(A,B) \)

shows \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \)
lemma domain_of_bij:

assumes \( f \in \text{bij}(X,Y) \)

shows \( domain(f) = X \)
lemma ord_iso_pres_lin:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsLinOrder}(B,R) \)

shows \( \text{IsLinOrder}(A,r) \)
Definition of IsBoundedAbove: \( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
lemma Order_ZF_3_L1A:

assumes \( r \subseteq X\times X \) and \( \text{IsBoundedAbove}(A,r) \)

shows \( A\subseteq X \)
lemma func1_1_L15A:

assumes \( f: X\rightarrow Y \) and \( A\subseteq X \) and \( A\neq \emptyset \)

shows \( f(A) \neq \emptyset \)
Definition of HasAminimum: \( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)
lemma inj_inv_back_in_set:

assumes \( f \in \text{inj}(A,B) \) and \( C\subseteq A \) and \( y \in f(C) \)

shows \( converse(f)(y) \in C \), \( f(converse(f)(y)) = y \)
lemma ord_iso_pres_rel_image:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( a\in A \)

shows \( f(r\{a\}) = R\{f(a)\} \)
lemma inj_image_of_Inter:

assumes \( f \in \text{inj}(A,B) \) and \( I\neq \emptyset \) and \( \forall i\in I.\ P(i) \subseteq A \)

shows \( f(\bigcap i\in I.\ P(i)) = ( \bigcap i\in I.\ f(P(i)) ) \)
lemma ord_iso_pres_up_bounds:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( C\subseteq A \)

shows \( \{f(r\{a\}).\ a\in C\} = \{R\{b\}.\ b \in f(C)\} \)
lemma ord_iso_pres_bound_above:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)

shows \( \text{IsBoundedAbove}(f(C),R) \), \( f(C) \neq 0 \)
Definition of IsComplete: \( r \text{ is complete } \equiv \) \( \forall A.\ \text{IsBoundedAbove}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
lemma ord_iso_pres_min_up_bounds:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( C\subseteq A \) and \( C\neq 0 \)

shows \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \)
lemma ZF1_1_L7:

assumes \( I\neq \emptyset \) and \( \forall i\in I.\ P(i) \subseteq X \)

shows \( ( \bigcap i\in I.\ P(i) ) \subseteq X \)
lemma ord_iso_pres_has_min:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( C\subseteq A \) and \( \text{HasAminimum}(R,f(C)) \)

shows \( \text{HasAminimum}(r,C) \)
lemma ind_rel_domain:

assumes \( R \subseteq B\times B \) and \( f:A\rightarrow B \)

shows \( \text{InducedRelation}(f,R) \subseteq A\times A \)
lemma ord_iso_pres_compl:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( R \text{ is complete } \)

shows \( r \text{ is complete } \)