U[image[IPD,BIJ]] = Q

Johan G. F. Belinfante
2010 February 24

SetDirectory["l:"]; <<  goedel.10feb23a; << tools.m

summary

In this notebook a connection between the equipollence relation Q and the function IPD is derived.  Recall that the function IPD takes any set x to the restriction of IMAGE[x] to the class of subsets of domain[x].

VERTSECT[reify[x, composite[IMAGE[x], id[P[domain[x]]]]]]

That there should be a connection between IPD and Q is suggested by the following inclusion which plays a key role in the derivation to be presented below.

subclass[composite[IMAGE[oopart[x]], id[P[domain[oopart[x]]]]], 
      Q]

derivation

The orientation of the following rewrite rule has the advantage that it makes manifest the fact that U[image[IPD, x]] is a relation.

Theorem.  An equation for U[image[IPD, x]].

SubstTest[image, intersection[u, v], 
        x, {u -> composite[inverse[FIRST], inverse[S], IMAGE[FIRST]], 
          v -> composite[SWAP, inverse[rotate[composite[IMG, SWAP]]]]}] // 
      Reverse

U[image[IPD, x_]] := 
      composite[IMG, id[composite[inverse[S], IMAGE[FIRST], id[x]]], 
        inverse[SECOND]]

an inclusion in one direction

Lemma.

dif[DORA, composite[inverse[E], IPD]] // FastReifNormality

% /. Equal -> SetDelayed

Theorem.

SubstTest[empty, 
      dif[u, v], {u -> DORA, v -> composite[inverse[E], IPD]}]

subclass[DORA, composite[inverse[E], IPD]] := True

The following inclusion will later be sharpened to an equation.

Corollary.    An inclusion in one direction.

SubstTest[implies, subclass[u, v], 
        subclass[image[u, w], image[v, w]], {u -> DORA, 
          v -> composite[inverse[E], IPD], w -> BIJ}] // 
      Reverse

% /. Equal -> SetDelayed

Serendipity.  The following corollary is not used further.

Corollary.

SubstTest[implies, subclass[u, v], 
        subclass[VERTSECT[v], composite[S, VERTSECT[u]]], {u -> DORA, 
          v -> composite[inverse[E], IPD]}] // Reverse

subclass[IPD, composite[E, DORA]] := True

reverse inclusion

Lemma.   Temporary rewrite rule.

equal[
      composite[intersection[complement[Q], IMAGE[oopart[x]]], 
        id[P[domain[oopart[x]]]]], 0]

composite[intersection[complement[Q], IMAGE[oopart[x_]]], 
        id[P[domain[oopart[x_]]]]] := 0

A variable-free corollary of this will be derived by applying range[reify[x, - ]] to this result.  A series of lemmas is used to simplify the expression obtained when this is done.

Lemma.

Map[range, composite[inverse[E], IPD, OOPART] // FastReifNormality] // 
      Reverse

% /. Equal -> SetDelayed

Lemma.

Map[
      composite[IMAGE[inverse[SINGLETON]], IMAGE[IMG], 
          CART, #] &, composite[
            id[composite[inverse[S], IMAGE[SINGLETON], IMAGE[FIRST], id[BIJ], 
                inverse[SINGLETON]]], inverse[SECOND], IMAGE[SINGLETON]] // 
          FastReifNormality // Reverse]

% /. Equal -> SetDelayed

Lemma.

composite[FIRST, 
        intersection[composite[inverse[SECOND], IMAGE[SINGLETON]], 
          composite[
            inverse[rotate[
                composite[IMAGE[inverse[SINGLETON]], IMAGE[IMG], CART, 
                  SWAP]]], SINGLETON, id[BIJ], inverse[IMAGE[FIRST]], S]]] // 
      FastReifNormality

% /. Equal -> SetDelayed

Lemma.  Variable-free inclusion in the opposite direction obtained by applying range[reify[x, - ]].

Map[empty[range[#]] &, 
      SubstTest[reify, x, 
        dif[composite[IMAGE[oopart[x]], id[P[domain[oopart[x]]]]], t], 
        t -> Q]]

% /. Equal -> SetDelayed

The inclusions in both directions can now be combined into an equation.

Main Theorem.  A formula for the equipollence relation.

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> composite[IMG, 
            id[composite[inverse[S], IMAGE[FIRST], id[BIJ]]], 
            inverse[SECOND]], v -> Q}]

composite[IMG, id[composite[inverse[S], IMAGE[FIRST], id[BIJ]]], 
        inverse[SECOND]] := Q

Restatement.

U[image[IPD, BIJ]]

serendipity

The following related results were also discovered in the course of this work.

Theorem.

ImageComp[IPD, IDP, V] // Reverse

image[IPD, P[Id]] := image[IMAGE[DUP], range[POWER]]

Theorem.

SubstTest[U, image[IPD, x], x -> V] // Reverse

U[range[IPD]] := 
      composite[IMG, id[composite[inverse[S], IMAGE[FIRST]]], 
        inverse[SECOND]]

Theorem.

Map[range[composite[rotate[flip[#]], inverse[FIRST]]] &, 
      intersection[
          inverse[composite[inverse[SECOND], inverse[S], IMAGE[FIRST]]], 
          composite[rotate[composite[IMG, SWAP]]]] // 
        DoubleInverse]

image[IMG, composite[inverse[S], IMAGE[FIRST]]] := V