V = transvar[x,y]

Johan G. F. Belinfante
2004 October 18

SetDirectory["i:"]; << goedel62.17b; << tools.m

summary

It is shown that  transvar[x,y]  equals  V  if and only if  composite[Id,x]  is a subclass of  y.   This result is used to show that if the range of a relation  x  is a subclass of the class  OMEGA  of ordinal numbers, then the function which selects the least member in each vertical section is a subclass of  x.

the transvar theorem

Recall that  transvar[x,y]  is the class of all  z  such that  image[x, z]  is a subclass of  image[y, z].  If this holds for every set  z, then in particular, it holds for all singletons, so in this case every vertical section of  x  is contained in the corresponding one for  y.

SubstTest[implies, and[member[u, v], equal[v, w]], 
      member[u, w], {u -> singleton[z], v -> V, 
        w -> transvar[x, y]}]

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

It follows that  composite[Id, x]  is a subclass of  y.

Map[equal[V, #] &, 
        SubstTest[class, z, 
          implies[equal[V, v], 
            subclass[image[x, singleton[z]], image[y, singleton[z]]]], 
          v -> transvar[x, y]]] // Reverse

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

The converse also holds:

Map[equal[V, class[z, #]] &, 
      SubstTest[implies, subclass[w, y], subclass[image[w, z], image[y, z]], 
        w -> composite[Id, x]]]

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

Thus the following logical equivalence holds:

equiv[equal[V, transvar[x, y]], 
      subclass[composite[Id, x], y]]

This result can be formulated as a new rewrite rule, which replaces a weaker existing rule.

equal[V, transvar[x_, y_]] := subclass[composite[Id, x], y]

application

Every nonempty collection of ordinal numbers has a least member.  It follows that if the range of a relation  x  is contained in the class  OMEGA  of all ordinals, then one can chose in each vertical section the least member, obtaining the function  composite[BIGCAP, VERTSECT[x]]  which is a subclass of  x.  To show this, the following lemma is convenient:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> image[VERTSECT[x], y], 
        v -> P[image[x, y]], w -> BIGCAP}]

subclass[image[BIGCAP, image[VERTSECT[x_], y_]], 
        Aclosure[image[x, y_]]] := True

Every subclass of  OMEGA  is closed under arbitrary intersections, so  image[x, y] here is its own Aclosure:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], implies[p3, p4], 
        not[implies[p1, p4]], {p1 -> subclass[range[x], OMEGA], 
          p2 -> subclass[image[x, y], OMEGA], 
          p3 -> equal[Aclosure[image[x, y]], image[x, y]], 
          p4 -> subclass[image[BIGCAP, image[VERTSECT[x], y]], 
              image[x, y]]}]]

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

Eliminating the variable  y  produces an expression involving  transvar, which is simplified by the rewrite rule derived in the preceding section.  The main result follows:

Map[equal[V, #] &, 
        SubstTest[class, y, 
          implies[subclass[u, v], 
            subclass[image[w, y], image[x, y]]], {u -> range[x], 
            v -> OMEGA, w -> composite[BIGCAP, VERTSECT[x]]}]] // 
      Reverse

or[not[subclass[range[x_], OMEGA]], 
        subclass[composite[BIGCAP, VERTSECT[x_]], x_]] := True

If  x  is thin, then the function composite[BIGCAP, VERTSECT[x]]  has the same domain as  x.

implies[thin[x], 
      equal[domain[composite[BIGCAP, VERTSECT[x]]], domain[x]]]