Re: (no subject)

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

A trybulec wrote:
> 
> I wanted to justify the following step (A,B,C,D fixed):
> 
> { A,B } = { C,D };
> then A = C & B = D or A = D & B = C 
> 
> I looked to Bylinski's ZFMISC_1 (where else), I found a theorem and I
> put
> "by ZFMISC_1:10;" as a justification.
> 
> I called Mizar and then I observed that ZFMISC_1:10 is not what
> I need. It is:
>  {x1,x2} = {y1,y2} implies (x1 = y1 or x1 = y2) & (x2 = y1 or x2 = y2)
> in the situation above e.g. A = C & B = C.
> 
> It was a surprize when Mizar accepted it. I appreciate comments.

The unordered pair functor is commutative.  Therefore from

A: { A, B } = { C, D };

   we have both:

B: (A = C or A = D) & (B = C or B = D) by A, ZFMISC_1:10;
C: (C = A or C = B) & (D = A or D = B) by A, ZFMISC_1:10;

and then

   A = C & B = D or A = D & B = C by B, C;

But I am only guessing how the checker treats commutative functors.

-- 
Piotr (Peter) Rudnicki