Re: (no subject)

[Andrzej Trybulec <trybulec@edserve.cs.shinshu-u.ac.jp>]

> I have just noticed that above, the reference to the commutativity
> of the onordered pair functor is irrelevant.  Simply, two different
> instances of ZFMISC_1:10 are used to disprove the four disjuncts
> of the negated proposition.
> 
> --
> Piotr (Peter) Rudnicki

Right. ZFMISC_1:10 should be revised (because of the commutativity
of {a,b}) to

{x1,x2} = {y1,y2} implies x1 = y1 or x = y2.

But it is not the point. The inference (in full form)

    for x1,x2,y1,y2 st {x1,x2} = {y1,y2} holds x1 = y1 or x1 = y2
    --------------------------------------------------------------
     {A,B} = {C,D} implies A = C & B = D or A = D & B = C
is not obvious. At least it does not look obvious to me.

It is a nice example of Davis Thesis.

Martin Davis (1981 ?) claimed, that an inference is obvious if
only one substitution of universally bind variables is used
in its justification. In the case above we have to use 4 different
substitutions.

Do we want steps in Mizar proofs to be obvious ?

Andrzej Trybulec