subclass[RS[x], y]

Johan G. F. Belinfante
2004 November 5

SetDirectory["i:"]; << goedel63.02a; << tools.m

summary

A rewrite rule is derived which has as an application a reformulation of the ac1 version of the axiom of choice.  The rewrite rule itself is generally valid, and does not depend on whether the axiom of choice does or does not hold.

derivation

Lemma 1.  (Temporary rewrite rule using thinpart wrapper.)

equal[V, 
        image[inverse[IMAGE[composite[id[thinpart[x]], inverse[FIRST]]]], 
          y]] // AssertTest

A better result will be derived shortly, eliminating the need for the thinpart wrapper.

equal[V, 
        image[inverse[IMAGE[composite[id[thinpart[x_]], inverse[FIRST]]]], 
          y_]] := subclass[RS[x], y]

Removing the thinpart wrapper yields Lemma 2:

SubstTest[implies, 
      and[equal[z, thinpart[x]], 
        equal[V, 
          image[inverse[IMAGE[composite[id[z], inverse[FIRST]]]], y]]], 
      subclass[RS[x], y], z -> composite[Id, x]]

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

Lemma 3:  The thin-ness hypothesis in Lemma 2 is not needed.

Map[
      implies[#, 
          thin[x]] &, (equal[V, 
              image[inverse[
                  IMAGE[composite[id[composite[x, id[z]]], inverse[FIRST]]]], 
                y]] // AssertTest) /. z -> V]

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

Using Lemma 3 to simplify Lemma 2 yields Lemma. 4:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        not[implies[p1, p3]], {p1 -> 
            equal[V, 
              image[inverse[IMAGE[composite[id[x], inverse[FIRST]]]], y]], 
          p2 -> thin[x], p3 -> subclass[RS[x], y]}]]

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

Lemma 5 is an implication in the opposite direction:

SubstTest[implies, and[equal[z, thinpart[x]], subclass[RS[x], y]], 
      equal[V, image[inverse[IMAGE[composite[id[z], inverse[FIRST]]]], y]], 
      z -> composite[Id, x]]

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

Main Theorem.  Combining all these lemmas yields a logical equivalence.

equiv[
          equal[V, 
            image[inverse[IMAGE[composite[id[x], inverse[FIRST]]]], y]], 
          and[equal[V, domain[VERTSECT[x]]], subclass[RS[x], y]]] // not // 
      not

This is made into a new rewrite rule.

equal[V, image[inverse[IMAGE[composite[id[x_], inverse[FIRST]]]], y_]] := 
      and[equal[V, domain[VERTSECT[x]]], subclass[RS[x], y]]

connection with the axiom of choice

When  x  is replaced with  inverse[E]  and  y  with  SELECT, one obtains a restatement of the  ac1 set-form of the axiom of choice.

equal[V, 
      image[inverse[IMAGE[composite[id[inverse[E]], inverse[FIRST]]]], 
        SELECT]]

The effect of the new rewrite rule is to transform this statement first to  subclass[RS[inverse[E]], SELECT], and then to axch.