Q:\FS\FS-CUP.TXT 2000 March 9 Theorem FS-CUP was inspired by Theorem 3.12 on page 26 of the book "Introduction to Set Theory," Third Edition, by Karel Hrbacek and Thomas Jech. It caught my eye because they refer to it in their proof of the iteration theorem. It is the latter that really is my goal. Theorem FS-CUP is described by Hrbacek and Jech as "the union of a compatible collection of functions is a function." The condition of compatibility they show to be equivalent to the condition that the union of any pair of functions in the collection is a function. When one eliminates the quantifiers that latter conditions becomes the hypothesis subclass(image(CUP,cart(x,x)),FUNS). So my initial inclination was to formulate this theorem as: (all x ((subclass(x,FUNS) & subclass(image(CUP,cart(x,x)),FUNS)) -> FUNCTION(U(x)))). I tried to get the GOEDEL program to do the quantifier elimination, but it came up with something unexpected which seemed to indicate that it somehow "knows" this theorem in some implicit form. I was not able to fathom this situation, but it did occur to me while working on this that the hypothesis subclass(x,FUNS) is dispensible. I proved as a lemma the following theorem (CUP-IM1 in the CUP group): (all x (subclass(x,FUNS) -> subclass(image(CUP,cart(x,x)),FUNS))). This lemma was not difficult, and by using it, one can therefore reformulate Hrbacek and Jech's compatibility theorem in the following elegant form: (all x (subclass(image(CUP,cart(x,x)),FUNS) -> FUNCTION(U(x)))). I managed to prove this, although it took all day. The proof obtained has length 19 and depth 9.