image[FIX, WO]

Johan G. F. Belinfante
2008 May 17

SetDirectory["l:"]; << goedel.08may15a; <<  tools.m

summary

Tentative rewrite rules are derived for the class image[FIX, WO] of all well-orderable sets.  This class is hereditary and is shown to contain the class image[Q, OMEGA] of all sets that are equipollent to an ordinal.

image[Q, x] rules

Lemma.

SubstTest[implies, subclass[x, z], 
        subclass[image[t, x], image[t, z]], {t -> Q, 
          z -> image[Q, y]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.   The implication in the lemma is actually a logical equivalence, which can be made into a rewrite rule.

equiv[subclass[image[Q, x], image[Q, y]], 
      subclass[x, image[Q, y]]]

subclass[image[Q, x_], image[Q, y_]] := 
      subclass[x, image[Q, y]]

Theorem.

ImageComp[IMG, composite[id[cart[BIJ, V]], inverse[SECOND]], x] // 
      Reverse

image[IMG, cart[BIJ, x_]] := image[Q, image[inverse[S], x]]

image[FIX, WO] is hereditary

Theorem.

ImageComp[FIX, 
      composite[CAP, id[cart[V, image[CART, Id]]], inverse[FIRST]], 
      WO]

image[inverse[S], image[IMAGE[inverse[DUP]], WO]] := 
      image[IMAGE[inverse[DUP]], WO]

one-to-one transforms

Lemma.

composite[IMAGE[inverse[DUP]], IMAGE[cross[oopart[x], oopart[x]]]] // 
      ReifNormality

composite[IMAGE[inverse[DUP]], IMAGE[cross[oopart[x_], oopart[x_]]]] := 
      composite[IMAGE[oopart[x]], IMAGE[inverse[DUP]]]

Theorem.  Fixed point sets of one-to-one transforms.

ImageComp[IMAGE[inverse[DUP]], IMAGE[cross[oopart[x], oopart[x]]], y] // 
      Reverse

image[IMAGE[inverse[DUP]], 
        image[IMAGE[cross[oopart[x_], oopart[x_]]], y_]] := 
      image[IMAGE[oopart[x]], image[IMAGE[inverse[DUP]], y]]

Corollary.  Application to one-to-one transforms of wellorder relations.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], 
{t -> FIX, 
          u -> image[IMAGE[cross[oopart[x], oopart[x]]], WO], v -> WO}] // 
      Reverse

subclass[image[IMAGE[oopart[x_]], image[IMAGE[inverse[DUP]], WO]], 
        image[IMAGE[inverse[DUP]], WO]] := True

Lemma.   The variable x is eliminated using reification.

Map[empty[composite[Id, complement[#]]] &, 
      SubstTest[reify, x, complement[dif[image[IMAGE[oopart[x]], w], w]], 
        w -> image[IMAGE[inverse[DUP]], WO]]]

% /. Equal -> SetDelayed

Theorem.  The inclusion in the lemma can be strengthened to an equation that can be made into a rewrite rule.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> image[Q, image[IMAGE[inverse[DUP]], WO]], 
        v -> image[IMAGE[inverse[DUP]], WO]}]

image[Q, image[IMAGE[inverse[DUP]], WO]] := 
      image[IMAGE[inverse[DUP]], WO]

ordinals are wellorderable

Theorem.  The restriction of S to any ordinal is a wellordering.

SubstTest[subclass, x, 
      image[inverse[IMAGE[id[S]]], y], {x -> image[CART, id[OMEGA]], 
        y -> WO}]

subclass[image[IMAGE[id[S]], image[CART, id[OMEGA]]], WO] := 
      True

Lemma.

ImageComp[FIX, composite[IMAGE[id[S]], CART, DUP], OMEGA] // 
      Reverse

image[IMAGE[inverse[DUP]], 
        image[IMAGE[id[S]], image[CART, id[OMEGA]]]] := OMEGA

Theorem.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], 
{t -> FIX, 
          u -> image[IMAGE[id[S]], image[CART, id[OMEGA]]], v -> WO}] // 
      Reverse

subclass[OMEGA, image[IMAGE[inverse[DUP]], WO]] := True

Corollary.  Any set equipollent to an ordinal is wellorderable.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], image[t, v]], 
{t -> Q, 
          u -> OMEGA, v -> image[IMAGE[inverse[DUP]], WO]}] // 
      Reverse

subclass[image[Q, OMEGA], image[IMAGE[inverse[DUP]], WO]] := 
      True

Corollary.  Any set of ordinals is wellorderable.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], 
{t -> inverse[S], u -> OMEGA, 
          v -> image[IMAGE[inverse[DUP]], WO]}] // Reverse

subclass[P[OMEGA], image[IMAGE[inverse[DUP]], WO]] := True