The Mizar article:

Some Basic Properties of Many Sorted Sets

by
Artur Kornilowicz

Received September 29, 1995

Copyright (c) 1995 Association of Mizar Users

MML identifier: PZFMISC1
[ MML identifier index ]


environ

 vocabulary FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, CAT_1, BOOLE, MATRIX_1,
      ZF_REFLE, PRE_CIRC, FINSET_1, CAT_4, TARSKI, PRALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1,
      CQC_LANG, PBOOLE, PRE_CIRC, PRALG_2, MBOOLEAN;
 constructors CQC_LANG, PRE_CIRC, PRALG_2, MBOOLEAN;
 clusters FINSET_1, PBOOLE, CQC_LANG, XBOOLE_0;
 requirements BOOLE;
 definitions PRE_CIRC, PBOOLE;
 theorems ALTCAT_1, BORSUK_1, CQC_LANG, ENUMSET1, FUNCT_4, MBOOLEAN, PARTFUN1,
      PBOOLE, PRALG_2, SETWISEO, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0;
 schemes MSUALG_1;

begin :: Preliminaries

 reserve i, I for set,
         f for Function,
         x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I,
         J for non empty set,
         NJ for ManySortedSet of J;

theorem Th1:
for X be set for M be ManySortedSet of I st i in I
 holds dom (M +* (i .--> X)) = I
  proof
   let X be set,
       M be ManySortedSet of I such that
A1:  i in I;
   thus dom (M +* (i .--> X)) = dom M \/ dom (i .--> X) by FUNCT_4:def 1
                             .= I \/ dom (i .--> X) by PBOOLE:def 3
                             .= I \/ {i} by CQC_LANG:5
                             .= I by A1,ZFMISC_1:46;
  end;

theorem
  f = {} implies f is ManySortedSet of {} by PBOOLE:def 3,RELAT_1:60;

theorem
  I is non empty implies
 not ex X st X is empty-yielding & X is non-empty
  proof
    assume
A1:   I is non empty;
    given X such that
A2:   X is empty-yielding and
A3:   X is non-empty;
    consider i such that
A4:   i in I by A1,XBOOLE_0:def 1;
      X.i is empty & X.i is non empty by A2,A3,A4,PBOOLE:def 15,def 16;
    hence contradiction;
  end;

begin :: Singelton and unordered pairs

definition let I, A;
 func {A} -> ManySortedSet of I means :Def1:
  for i st i in I holds it.i = {A.i};
existence
proof
 deffunc F(set) = {A.$1};
 thus ex M be ManySortedSet of I st for i st i in I holds M.i = F(i)
  from MSSLambda;
end;
uniqueness
  proof
   let X, Y be ManySortedSet of I such that
A1: (for i st i in I holds X.i = {A.i}) and
A2: for i st i in I holds Y.i = {A.i};
     now
    let i; assume
A3:  i in I;
    hence X.i = {A.i} by A1
            .= Y.i by A2,A3;
   end;
   hence X = Y by PBOOLE:3;
  end;
end;

definition let I, A;
 cluster {A} -> non-empty locally-finite;
coherence
  proof
    thus {A} is non-empty
    proof
      let i such that
A1:     i in I;
        {A.i} <> {};
      hence {A}.i is non empty by A1,Def1;
    end;
    let i such that
A2:   i in I;
      {A.i} is finite;
    hence {A}.i is finite by A2,Def1;
  end;
end;

definition let I, A, B;
 func {A,B} -> ManySortedSet of I means :Def2:
  for i st i in I holds it.i = {A.i,B.i};
existence
proof
 deffunc F(set) = {A.$1,B.$1};
 thus ex M be ManySortedSet of I st for i st i in I holds M.i = F(i)
  from MSSLambda;
end;
uniqueness
  proof
   let X, Y be ManySortedSet of I such that
A1: (for i st i in I holds X.i = {A.i,B.i}) and
A2: for i st i in I holds Y.i = {A.i,B.i};
     now
    let i; assume
A3:  i in I;
    hence X.i = {A.i,B.i} by A1
            .= Y.i by A2,A3;
   end;
   hence X = Y by PBOOLE:3;
  end;
 commutativity;
end;

definition let I, A, B;
 cluster {A,B} -> non-empty locally-finite;
coherence
  proof
    thus {A,B} is non-empty
    proof
      let i such that
A1:     i in I;
        {A.i,B.i} <> {};
      hence {A,B}.i is non empty by A1,Def2;
    end;
    let i such that
A2:   i in I;
      {A.i,B.i} is finite;
    hence {A,B}.i is finite by A2,Def2;
  end;
end;

theorem     :: Tarski:3
  X = { y } iff for x holds x in X iff x = y
  proof
    thus X = { y } implies for x holds x in X iff x = y
    proof
      assume
A1:     X = {y};
      let x;
      thus x in X implies x = y
      proof
        assume
A2:       x in X;
          now
          let i; assume
A3:         i in I;
then A4:       x.i in X.i by A2,PBOOLE:def 4;
            X.i = {y.i} by A1,A3,Def1;
          hence x.i = y.i by A4,TARSKI:def 1;
        end;
        hence thesis by PBOOLE:3;
      end;
      assume
A5:     x = y;
      let i;
      assume i in I;
      then X.i = {y.i} by A1,Def1;
      hence x.i in X.i by A5,TARSKI:def 1;
    end;
    assume
A6:   for x holds x in X iff x = y;
then A7: y in X;
      now
      let i such that
A8:     i in I;
        now
        let a be set;
        thus a in X.i iff a = y.i
        proof
          thus a in X.i implies a = y.i
          proof
            assume
A9:           a in X.i;
A10:         dom (i .--> a) = {i} by CQC_LANG:5;
           dom (y +* (i .--> a)) = I by A8,Th1;
            then reconsider x1 = y +* (i .--> a) as ManySortedSet of I
                           by PBOOLE:def 3;
              i in {i} by TARSKI:def 1;
then A11:         x1.i = (i .--> a).i by A10,FUNCT_4:14
                .= a by CQC_LANG:6;
              x1 in X
            proof
              let q be set such that
A12:             q in I;
              per cases;
              suppose i = q;
                hence x1.q in X.q by A9,A11;
              suppose i <> q;
                then not q in dom (i .--> a) by A10,TARSKI:def 1;
                then x1.q = y.q by FUNCT_4:12;
                hence x1.q in X.q by A7,A12,PBOOLE:def 4;
            end;
            hence a = y.i by A6,A11;
          end;
          assume a = y.i;
          hence a in X.i by A7,A8,PBOOLE:def 4;
        end;
      end;
      then X.i = {y.i} by TARSKI:def 1;
      hence X.i = {y}.i by A8,Def1;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: Tarski:4 a
  (for x holds x in X iff x = x1 or x = x2) implies X = { x1,x2 }
  proof
    assume
A1:   for x holds x in X iff x = x1 or x = x2;
then A2: x1 in X;
A3: x2 in X by A1;
      now
      let i such that
A4:     i in I;
        now
        let a be set;
        thus a in X.i iff a = x1.i or a = x2.i
        proof
          thus a in X.i implies a = x1.i or a = x2.i
          proof
            assume that
A5:           a in X.i and
A6:           a <> x1.i;
A7:         dom (i .--> a) = {i} by CQC_LANG:5;
           dom (x2 +* (i .--> a)) = I by A4,Th1;
            then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I
                       by PBOOLE:def 3;
              i in {i} by TARSKI:def 1;
then A8:         k2.i = (i .--> a).i by A7,FUNCT_4:14
                .= a by CQC_LANG:6;
              k2 in X
            proof
              let q be set such that
A9:             q in I;
              per cases;
              suppose i = q;
                hence k2.q in X.q by A5,A8;
              suppose i <> q;
                then not q in dom (i .--> a) by A7,TARSKI:def 1;
                then k2.q = x2.q by FUNCT_4:12;
                hence k2.q in X.q by A3,A9,PBOOLE:def 4;
            end;
            hence a = x2.i by A1,A6,A8;
          end;
          assume
A10:         a = x1.i or a = x2.i;
          per cases by A10;
          suppose a = x1.i;
            hence a in X.i by A2,A4,PBOOLE:def 4;
          suppose a = x2.i;
            hence a in X.i by A3,A4,PBOOLE:def 4;
        end;
      end;
      then X.i = {x1.i,x2.i} by TARSKI:def 2;
      hence X.i = { x1,x2 }.i by A4,Def2;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: Tarski:4 b
  X = { x1,x2 } implies for x holds x = x1 or x = x2 implies x in X
  proof
    assume
A1:   X = { x1,x2 };
    let x;
    assume
A2:   x = x1 or x = x2;
    let i; assume
     i in I;
then A3: X.i = {x1.i,x2.i} by A1,Def2;
    per cases by A2;
    suppose x = x1;
      hence x.i in X.i by A3,TARSKI:def 2;
    suppose x = x2;
      hence x.i in X.i by A3,TARSKI:def 2;
  end;

theorem
  { NJ } <> [0]I
  proof
    assume
        { NJ } = [0]I;
    hence contradiction by PBOOLE:141;
  end;

theorem     :: ENUMSET1:3
  x in { A } implies x = A
 proof
   assume
A1:  x in { A };
     now
     let i; assume
A2:    i in I;
     then x.i in {A}.i by A1,PBOOLE:def 4;
     then x.i in {A.i} by A2,Def1;
     hence x.i = A.i by TARSKI:def 1;
   end;
   hence thesis by PBOOLE:3;
 end;

theorem     :: ENUMSET1:4
  x in { x }
 proof
   let i such that
A1:  i in I;
     x.i in {x.i} by TARSKI:def 1;
   hence x.i in {x}.i by A1,Def1;
 end;

theorem     :: ENUMSET1:9
  x = A or x = B implies x in { A,B }
  proof
    assume
A1:   x=A or x=B;
    per cases by A1;
    suppose
A2:   x=A;
      let i such that
A3:     i in I;
        x.i in {A.i,B.i} by A2,TARSKI:def 2;
      hence x.i in { A,B }.i by A3,Def2;
    suppose
A4:   x=B;
      let i such that
A5:     i in I;
        x.i in {A.i,B.i} by A4,TARSKI:def 2;
      hence x.i in { A,B }.i by A5,Def2;
  end;

theorem     ::ENUMSET1:41
  {A} \/ {B} = {A,B}
  proof
      now
      let i; assume
A1:     i in I;
      hence ({A} \/ {B}).i = {A}.i \/ {B}.i by PBOOLE:def 7
                        .= {A}.i \/ {B.i} by A1,Def1
                        .= {A.i} \/ {B.i} by A1,Def1
                        .= {A.i,B.i} by ENUMSET1:41
                        .= {A,B}.i by A1,Def2;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ENUMSET1:69
  { x,x } = { x }
  proof
      now
      let i; assume
A1:     i in I;
      hence { x,x }.i = {x.i,x.i} by Def2
                    .= {x.i} by ENUMSET1:69
                    .= { x }.i by A1,Def1;
    end;
    hence thesis by PBOOLE:3;
  end;

canceled;

theorem     :: SETWISEO:1
  {A} c= {B} implies A = B
  proof
    assume
A1:   {A} c= {B};
      now
      let i; assume
A2:     i in I;
      then {A}.i c= {B}.i by A1,PBOOLE:def 5;
      then {A}.i c= {B.i} by A2,Def1;
      then {A.i} c= {B.i} by A2,Def1;
      hence A.i = B.i by ZFMISC_1:24;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:6
  {x} = {y} implies x = y
  proof
    assume
A1:   {x} = {y};
      now
      let i; assume
A2:     i in I;
      then {x.i} = {x}.i by Def1
           .= {y.i} by A1,A2,Def1;
      hence x.i = y.i by ZFMISC_1:6;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:8
  {x} = {A,B} implies x = A & x = B
  proof
    assume
A1:   {x} = {A,B};
      now
      let i; assume
A2:     i in I;
      then {x.i} = {x}.i by Def1
           .= {A.i,B.i} by A1,A2,Def2;
      hence x.i = A.i by ZFMISC_1:8;
    end;
    hence x = A by PBOOLE:3;
      now
      let i; assume
A3:     i in I;
      then {x.i} = {x}.i by Def1
           .= {A.i,B.i} by A1,A3,Def2;
      hence x.i = B.i by ZFMISC_1:8;
    end;
    hence x = B by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:9
  {x} = {A,B} implies A = B
  proof
    assume
A1:   {x} = {A,B};
      now
      let i; assume
A2:     i in I;
      then {x.i} = {x}.i by Def1
           .= {A.i,B.i} by A1,A2,Def2;
      hence A.i = B.i by ZFMISC_1:9;
    end;
    hence A = B by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:12
  {x} c= {x,y} & {y} c= {x,y}
  proof
    thus {x} c= {x,y}
    proof
      let i such that
A1:     i in I;
        {x.i} c= {x.i,y.i} by ZFMISC_1:12;
      then {x}.i c= {x.i,y.i} by A1,Def1;
      hence {x}.i c= {x,y}.i by A1,Def2;
    end;
    let i such that
A2:   i in I;
      {y.i} c= {x.i,y.i} by ZFMISC_1:12;
    then {y}.i c= {x.i,y.i} by A2,Def1;
    hence {y}.i c= {x,y}.i by A2,Def2;
  end;

theorem     :: ZFMISC_1:13
  {x} \/ {y} = {x} or {x} \/ {y} = {y} implies x = y
  proof
    assume
A1:   {x} \/ {y} = {x} or {x} \/ {y} = {y};
      now
      let i such that
A2:     i in I;
      per cases by A1;
      suppose
A3:       {x} \/ {y} = {x};
          {x.i} \/ {y.i} = {x.i} \/ {y}.i by A2,Def1
                     .= {x}.i \/ {y}.i by A2,Def1
                     .= ({x} \/ {y}).i by A2,PBOOLE:def 7
                     .= {x.i} by A2,A3,Def1;
        hence x.i = y.i by ZFMISC_1:13;
      suppose
A4:       {x} \/ {y} = {y};
          {x.i} \/ {y.i} = {x.i} \/ {y}.i by A2,Def1
                     .= {x}.i \/ {y}.i by A2,Def1
                     .= ({x} \/ {y}).i by A2,PBOOLE:def 7
                     .= {y.i} by A2,A4,Def1;
        hence x.i = y.i by ZFMISC_1:13;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:14
  {x} \/ {x,y} = {x,y}
  proof
      now
      let i; assume
A1:     i in I;
      hence ({x} \/ {x,y}).i = {x}.i \/ {x,y}.i by PBOOLE:def 7
                          .= {x.i} \/ {x,y}.i by A1,Def1
                          .= {x.i} \/ {x.i,y.i} by A1,Def2
                          .= {x.i,y.i} by ZFMISC_1:14
                          .= {x,y}.i by A1,Def2;
    end;
    hence thesis by PBOOLE:3;
  end;

canceled;

theorem     :: ZFMISC_1:16
  I is non empty & {x} /\ {y} = [0]I implies x <> y
  proof
    assume that
A1:   I is non empty and
A2:   {x} /\ {y} = [0]I;
      now
      consider i such that
A3:     i in I by A1,XBOOLE_0:def 1;
      take i;
        {x.i} /\ {y.i} = {x}.i /\ {y.i} by A3,Def1
                   .= {x}.i /\ {y}.i by A3,Def1
                   .= ({x} /\ {y}).i by A3,PBOOLE:def 8
                   .= {} by A2,A3,PBOOLE:5;
      hence x.i <> y.i;
    end;
    hence thesis;
  end;

theorem     :: ZFMISC_1:18
  {x} /\ {y} = {x} or {x} /\ {y} = {y} implies x = y
  proof
    assume
A1:   {x} /\ {y} = {x} or {x} /\ {y} = {y};
    per cases by A1;
    suppose
A2:    {x} /\ {y} = {x};
        now
        let i; assume
A3:       i in I;
        then {x.i} /\ {y.i} = {x.i} /\ {y}.i by Def1
                     .= {x}.i /\ {y}.i by A3,Def1
                     .= ({x} /\ {y}).i by A3,PBOOLE:def 8
                     .= {x.i} by A2,A3,Def1;
        hence x.i = y.i by ZFMISC_1:18;
      end;
      hence thesis by PBOOLE:3;
    suppose
A4:     {x} /\ {y} = {y};
        now
        let i; assume
A5:       i in I;
        then {x.i} /\ {y.i} = {x.i} /\ {y}.i by Def1
                     .= {x}.i /\ {y}.i by A5,Def1
                     .= ({x} /\ {y}).i by A5,PBOOLE:def 8
                     .= {y.i} by A4,A5,Def1;
        hence x.i = y.i by ZFMISC_1:18;
      end;
      hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:19
  {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y}
  proof
    thus {x} /\ {x,y} = {x}
    proof
        now
        let i; assume
A1:       i in I;
        hence ({x} /\ {x,y}).i = {x}.i /\ {x,y}.i by PBOOLE:def 8
                            .= {x.i} /\ {x,y}.i by A1,Def1
                            .= {x.i} /\ {x.i,y.i} by A1,Def2
                            .= {x.i} by ZFMISC_1:19
                            .= {x}.i by A1,Def1;
      end;
      hence thesis by PBOOLE:3;
    end;
    thus {y} /\ {x,y} = {y}
    proof
        now
        let i; assume
A2:       i in I;
        hence ({y} /\ {x,y}).i = {y}.i /\ {x,y}.i by PBOOLE:def 8
                            .= {y.i} /\ {x,y}.i by A2,Def1
                            .= {y.i} /\ {x.i,y.i} by A2,Def2
                            .= {y.i} by ZFMISC_1:19
                            .= {y}.i by A2,Def1;
      end;
      hence thesis by PBOOLE:3;
    end;
  end;

theorem     :: ZFMISC_1:20
  I is non empty & {x} \ {y} = {x} implies x <> y
  proof
    assume that
A1:   I is non empty and
A2:   {x} \ {y} = {x};
      now
      consider i such that
A3:     i in I by A1,XBOOLE_0:def 1;
      take i;
        {x.i} \ {y.i} = {x}.i \ {y.i} by A3,Def1
                   .= {x}.i \ {y}.i by A3,Def1
                   .= ({x} \ {y}).i by A3,PBOOLE:def 9
                   .= {x.i} by A2,A3,Def1;
      hence x.i <> y.i by ZFMISC_1:20;
    end;
    hence thesis;
  end;

theorem     :: ZFMISC_1:21
  {x} \ {y} = [0]I implies x = y
  proof
    assume
A1:   {x} \ {y} = [0]I;
      now
      let i; assume
A2:     i in I;
      then {x.i} \ {y.i} = {x}.i \ {y.i} by Def1
                   .= {x}.i \ {y}.i by A2,Def1
                   .= ({x} \ {y}).i by A2,PBOOLE:def 9
                   .= {} by A1,A2,PBOOLE:5;
      hence x.i = y.i by ZFMISC_1:21;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:22
  {x} \ {x,y} = [0]I & {y} \ {x,y} = [0]I
  proof
    thus {x} \ {x,y} = [0]I
    proof
        now
        let i; assume
A1:       i in I;
        hence ({x} \ {x,y}).i = {x}.i \ {x,y}.i by PBOOLE:def 9
                            .= {x.i} \ {x,y}.i by A1,Def1
                            .= {x.i} \ {x.i,y.i} by A1,Def2
                            .= {} by ZFMISC_1:22
                            .= [0]I.i by A1,PBOOLE:5;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A2:     i in I;
      hence ({y} \ {x,y}).i = {y}.i \ {x,y}.i by PBOOLE:def 9
                          .= {y.i} \ {x,y}.i by A2,Def1
                          .= {y.i} \ {x.i,y.i} by A2,Def2
                          .= {} by ZFMISC_1:22
                          .= [0]I.i by A2,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:24
  {x} c= {y} implies {x} = {y}
  proof
    assume
A1:   {x} c= {y};
      now
      let i; assume
A2:     i in I;
      then {x}.i c= {y}.i by A1,PBOOLE:def 5;
      then {x.i} c= {y}.i by A2,Def1;
then A3:   {x.i} c= {y.i} by A2,Def1;
      thus {x}.i = {x.i} by A2,Def1
                .= {y.i} by A3,ZFMISC_1:24
                .= {y}.i by A2,Def1;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:26
  {x,y} c= {A} implies x = A & y = A
  proof
    assume
A1:   {x,y} c= {A};
    thus x = A
    proof
        now
        let i; assume
A2:       i in I;
        then {x,y}.i c= {A}.i by A1,PBOOLE:def 5;
        then {x,y}.i c= {A.i} by A2,Def1;
        then {x.i,y.i} c= {A.i} by A2,Def2;
        hence x.i = A.i by ZFMISC_1:26;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A3:     i in I;
      then {x,y}.i c= {A}.i by A1,PBOOLE:def 5;
      then {x,y}.i c= {A.i} by A3,Def1;
      then {x.i,y.i} c= {A.i} by A3,Def2;
      hence y.i = A.i by ZFMISC_1:26;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:27
  {x,y} c= {A} implies {x,y} = {A}
  proof
    assume
A1:   {x,y} c= {A};
      now
      let i; assume
A2:     i in I;
      then {x,y}.i c= {A}.i by A1,PBOOLE:def 5;
      then {x.i,y.i} c= {A}.i by A2,Def2;
then A3:   {x.i,y.i} c= {A.i} by A2,Def1;
      thus {x,y}.i = {x.i,y.i} by A2,Def2
                  .= {A.i} by A3,ZFMISC_1:27
                  .= {A}.i by A2,Def1;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:30
  bool { x } = { [0]I, {x} }
  proof
      now
      let i; assume
A1:     i in I;
      hence (bool {x}).i = bool ({x}.i) by MBOOLEAN:def 1
                       .= bool ({x.i}) by A1,Def1
                       .= {{}, {x.i}} by ZFMISC_1:30
                       .= {[0]I.i, {x.i}} by A1,PBOOLE:5
                       .= {[0]I.i, {x}.i} by A1,Def1
                       .= { [0]I, {x} }.i by A1,Def2;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:80
  { A } c= bool A
  proof
    let i such that
A1:   i in I;
      {A.i} c= bool (A.i) by ZFMISC_1:80;
    then {A}.i c= bool (A.i) by A1,Def1;
    hence {A}.i c= (bool A).i by A1,MBOOLEAN:def 1;
  end;

theorem     :: ZFMISC_1:31
  union { x } = x
  proof
      now
      let i; assume
A1:     i in I;
      hence (union { x }).i = union ({x}.i) by MBOOLEAN:def 2
                          .= union {x.i} by A1,Def1
                          .= x.i by ZFMISC_1:31;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:32
  union { {x},{y} } = {x,y}
  proof
      now
      let i; assume
A1:     i in I;
      hence (union { {x},{y} }).i = union ({{x},{y}}.i) by MBOOLEAN:def 2
                                .= union {{x}.i,{y}.i} by A1,Def2
                                .= union {{x.i},{y}.i} by A1,Def1
                                .= union {{x.i},{y.i}} by A1,Def1
                                .= {x.i,y.i} by ZFMISC_1:32
                                .= {x,y}.i by A1,Def2;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:93
  union { A,B } = A \/ B
  proof
      now
      let i; assume
A1:     i in I;
      hence (union { A,B }).i = union ({A,B}.i) by MBOOLEAN:def 2
                            .= union {A.i,B.i} by A1,Def2
                            .= A.i \/ B.i by ZFMISC_1:93
                            .= (A \/ B).i by A1,PBOOLE:def 7;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:37
  {x} c= X iff x in X
  proof
    thus {x} c= X implies x in X
    proof
      assume
A1:     {x} c= X;
      let i; assume
A2:     i in I;
      then {x}.i c= X.i by A1,PBOOLE:def 5;
      then {x.i} c= X.i by A2,Def1;
      hence x.i in X.i by ZFMISC_1:37;
    end;
    assume
A3:   x in X;
    let i; assume
A4:   i in I;
    then x.i in X.i by A3,PBOOLE:def 4;
    then {x.i} c= X.i by ZFMISC_1:37;
    hence {x}.i c= X.i by A4,Def1;
  end;

theorem     :: ZFMISC_1:38
  {x1,x2} c= X iff x1 in X & x2 in X
  proof
    thus {x1,x2} c= X implies x1 in X & x2 in X
    proof
      assume
A1:     {x1,x2} c= X;
      thus x1 in X
      proof
        let i; assume
A2:       i in I;
        then {x1,x2}.i c= X.i by A1,PBOOLE:def 5;
        then {x1.i,x2.i} c= X.i by A2,Def2;
        hence thesis by ZFMISC_1:38;
      end;
      let i; assume
A3:     i in I;
      then {x1,x2}.i c= X.i by A1,PBOOLE:def 5;
      then {x1.i,x2.i} c= X.i by A3,Def2;
      hence thesis by ZFMISC_1:38;
    end;
    assume
A4:   x1 in X & x2 in X;
    let i; assume
A5:   i in I;
    then x1.i in X.i & x2.i in X.i by A4,PBOOLE:def 4;
    then {x1.i,x2.i} c= X.i by ZFMISC_1:38;
    hence thesis by A5,Def2;
  end;

theorem     :: ZFMISC_1:42
  A = [0]I or A = {x1} or A = {x2} or A = {x1,x2} implies A c= {x1,x2}
  proof
    assume
A1:   A = [0]I or A = {x1} or A = {x2} or A = {x1,x2};
    let i such that
A2:   i in I;
    per cases by A1;
    suppose A = [0]I;
      then A.i = {} by A2,PBOOLE:5;
      then A.i c= {x1.i,x2.i} by ZFMISC_1:42;
      hence A.i c= {x1,x2}.i by A2,Def2;
    suppose A = {x1};
      then A.i = {x1.i} by A2,Def1;
      then A.i c= {x1.i,x2.i} by ZFMISC_1:42;
      hence A.i c= {x1,x2}.i by A2,Def2;
    suppose A = {x2};
      then A.i = {x2.i} by A2,Def1;
      then A.i c= {x1.i,x2.i} by ZFMISC_1:42;
      hence A.i c= {x1,x2}.i by A2,Def2;
    suppose A = {x1,x2};
      hence A.i c= {x1,x2}.i;
  end;

begin :: Sum of an unordered pairs (or a singelton) and a set

theorem     :: SETWISEO:6
  x in A or x = B implies x in A \/ {B}
  proof
    assume
A1:   x in A or x = B;
    let i such that
A2:   i in I;
    per cases by A1;
    suppose x in A;
      then x.i in A.i by A2,PBOOLE:def 4;
      then x.i in A.i \/ {B.i} by SETWISEO:6;
      then x.i in A.i \/ {B}.i by A2,Def1;
      hence x.i in (A \/ {B}).i by A2,PBOOLE:def 7;
    suppose x = B;
      then x.i in A.i \/ {B.i} by SETWISEO:6;
      then x.i in A.i \/ {B}.i by A2,Def1;
      hence x.i in (A \/ {B}).i by A2,PBOOLE:def 7;
  end;

theorem     :: SETWISEO:8
  A \/ {x} c= B iff x in B & A c= B
  proof
    thus A \/ {x} c= B implies x in B & A c= B
    proof
      assume
A1:     A \/ {x} c= B;
A2:   now
        let i; assume
A3:       i in I;
        then (A \/ {x}).i c= B.i by A1,PBOOLE:def 5;
        then A.i \/ {x}.i c= B.i by A3,PBOOLE:def 7;
        hence A.i \/ {x.i} c= B.i by A3,Def1;
      end;
      thus x in B
      proof
        let i;
        assume i in I;
        then A.i \/ {x.i} c= B.i by A2;
        hence x.i in B.i by SETWISEO:8;
      end;
      let i;
      assume i in I;
      then A.i \/ {x.i} c= B.i by A2;
      hence A.i c= B.i by SETWISEO:8;
    end;
    assume
A4:   x in B & A c= B;
    let i; assume
A5:   i in I;
    then x.i in B.i & A.i c= B.i by A4,PBOOLE:def 4,def 5;
    then A.i \/ {x.i} c= B.i by SETWISEO:8;
    then A.i \/ {x}.i c= B.i by A5,Def1;
    hence (A \/ {x}).i c= B.i by A5,PBOOLE:def 7;
  end;

theorem     :: ZFMISC_1:45
  {x} \/ X = X implies x in X
 proof
   assume
A1:  {x} \/ X = X;
   let i; assume
A2:  i in I;
   then {x.i} \/ X.i = {x}.i \/ X.i by Def1
              .= X.i by A1,A2,PBOOLE:def 7;
   hence thesis by ZFMISC_1:45;
 end;

theorem     :: ZFMISC_1:46
  x in X implies {x} \/ X = X
 proof
   assume
A1:  x in X;
     now
     let i; assume
A2:    i in I;
then A3:  x.i in X.i by A1,PBOOLE:def 4;
     thus ({x} \/ X).i = {x}.i \/ X.i by A2,PBOOLE:def 7
                     .= {x.i} \/ X.i by A2,Def1
                     .= X.i by A3,ZFMISC_1:46;
   end;
   hence thesis by PBOOLE:3;
 end;

theorem     :: ZFMISC_1:47, 48
  {x,y} \/ A = A iff x in A & y in A
  proof
    thus {x,y} \/ A = A implies x in A & y in A
    proof
     assume
A1:     {x,y} \/ A = A;
      thus x in A
      proof
        let i; assume
A2:       i in I;
        then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2
                       .= A.i by A1,A2,PBOOLE:def 7;
        hence x.i in A.i by ZFMISC_1:47;
      end;
      let i; assume
A3:     i in I;
      then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2
                     .= A.i by A1,A3,PBOOLE:def 7;
      hence y.i in A.i by ZFMISC_1:47;
    end;
    assume
A4:   x in A & y in A;
      now
      let i; assume
A5:     i in I;
then A6:   x.i in A.i & y.i in A.i by A4,PBOOLE:def 4;
      thus ({x,y} \/ A).i = {x,y}.i \/ A.i by A5,PBOOLE:def 7
                        .= {x.i,y.i} \/ A.i by A5,Def2
                        .= A.i by A6,ZFMISC_1:48;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:49
  I is non empty implies {x} \/ X <> [0]I
  proof
    assume that
A1:   I is non empty and
A2:   {x} \/ X = [0]I;
    consider i such that
A3:   i in I by A1,XBOOLE_0:def 1;
      {x.i} \/ X.i <> {};
    then {x}.i \/ X.i <> {} by A3,Def1;
    then ({x} \/ X).i <> {} by A3,PBOOLE:def 7;
    hence contradiction by A2,A3,PBOOLE:5;
  end;

theorem     :: ZFMISC_1:50
  I is non empty implies {x,y} \/ X <> [0]I
  proof
    assume that
A1:   I is non empty and
A2:   {x,y} \/ X = [0]I;
    consider i such that
A3:   i in I by A1,XBOOLE_0:def 1;
      {x.i,y.i} \/ X.i <> {};
    then {x,y}.i \/ X.i <> {} by A3,Def2;
    then ({x,y} \/ X).i <> {} by A3,PBOOLE:def 7;
    hence contradiction by A2,A3,PBOOLE:5;
  end;

begin :: Intersection of an unordered pairs (or a singelton) and a set

theorem     :: ZFMISC_1:51
  X /\ {x} = {x} implies x in X
  proof
    assume
A1:   X /\ {x} = {x};
    let i; assume
A2:   i in I;
    then X.i /\ {x.i} = X.i /\ {x}.i by Def1
               .= (X /\ {x}).i by A2,PBOOLE:def 8
               .= {x.i} by A1,A2,Def1;
    hence x.i in X.i by ZFMISC_1:51;
  end;

theorem     :: ZFMISC_1:52
  x in X implies X /\ {x} = {x}
  proof
    assume
A1:   x in X;
    thus X /\ {x} = {x}
    proof
        now
        let i; assume
A2:       i in I;
then A3:     x.i in X.i by A1,PBOOLE:def 4;
        thus (X /\ {x}).i = X.i /\ {x}.i by A2,PBOOLE:def 8
                        .= X.i /\ {x.i} by A2,Def1
                        .= {x.i} by A3,ZFMISC_1:52
                        .= {x}.i by A2,Def1;
      end;
      hence thesis by PBOOLE:3;
    end;
  end;

theorem     :: ZFMISC_1:53, 63
  x in X & y in X iff {x,y} /\ X = {x,y}
  proof
    thus x in X & y in X implies {x,y} /\ X = {x,y}
    proof
      assume
A1:     x in X & y in X;
        now
        let i; assume
A2:       i in I;
then A3:     x.i in X.i & y.i in X.i by A1,PBOOLE:def 4;
        thus ({x,y} /\ X).i = {x,y}.i /\ X.i by A2,PBOOLE:def 8
                          .= {x.i,y.i} /\ X.i by A2,Def2
                          .= {x.i,y.i} by A3,ZFMISC_1:53
                          .= {x,y}.i by A2,Def2;
      end;
      hence thesis by PBOOLE:3;
    end;
    assume
A4:   {x,y} /\ X = {x,y};
    thus x in X
    proof
      let i; assume
A5:     i in I;
      then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
                     .= ({x,y} /\ X).i by A5,PBOOLE:def 8
                     .= {x.i,y.i} by A4,A5,Def2;
      hence thesis by ZFMISC_1:63;
    end;
    let i; assume
A6:     i in I;
    then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
                   .= ({x,y} /\ X).i by A6,PBOOLE:def 8
                   .= {x.i,y.i} by A4,A6,Def2;
    hence thesis by ZFMISC_1:63;
  end;

theorem     :: ZFMISC_1:54
  I is non empty & {x} /\ X = [0]I implies not x in X
  proof
    assume that
A1:   I is non empty and
A2:   {x} /\ X = [0]I and
A3:   x in X;
    consider i such that
A4:   i in I by A1,XBOOLE_0:def 1;
      {x.i} /\ X.i = {x}.i /\ X.i by A4,Def1
               .= ({x} /\ X).i by A4,PBOOLE:def 8
               .= {} by A2,A4,PBOOLE:5;
    then {x.i} misses X.i by XBOOLE_0:def 7;
    then not x.i in X.i by ZFMISC_1:54;
    hence contradiction by A3,A4,PBOOLE:def 4;
  end;

theorem     :: ZFMISC_1:55
  I is non empty & {x,y} /\ X = [0]I implies not x in X & not y in X
  proof
    assume that
A1:   I is non empty and
A2:   {x,y} /\ X = [0]I;
A3: now
      let i; assume
A4:     i in I;
      hence {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
                          .= ({x,y} /\ X).i by A4,PBOOLE:def 8
                          .= {} by A2,A4,PBOOLE:5;
    end;
    thus not x in X
    proof
      assume
A5:     x in X;
        now
        consider i such that
A6:       i in I by A1,XBOOLE_0:def 1;
        take i;
          {x.i,y.i} /\ X.i = {} by A3,A6;
        then {x.i,y.i} misses X.i by XBOOLE_0:def 7;
        hence i in I & not x.i in X.i by A6,ZFMISC_1:55;
      end;
      hence contradiction by A5,PBOOLE:def 4;
    end;
    assume
A7:   y in X;
      now
      consider i such that
A8:       i in I by A1,XBOOLE_0:def 1;
      take i;
        {x.i,y.i} /\ X.i = {} by A3,A8;
      then {x.i,y.i} misses X.i by XBOOLE_0:def 7;
      hence i in I & not y.i in X.i by A8,ZFMISC_1:55;
    end;
    hence contradiction by A7,PBOOLE:def 4;
  end;

begin :: Difference of an unordered pairs (or a singelton) and a set

theorem     :: ZFMISC_1:64 a
  y in X \ {x} implies y in X
  proof
    assume
A1:   y in X \ {x};
    let i; assume
A2:   i in I;
    then y.i in (X \ {x}).i by A1,PBOOLE:def 4;
    then y.i in X.i \ {x}.i by A2,PBOOLE:def 9;
    then y.i in X.i \ {x.i} by A2,Def1;
    hence y.i in X.i by ZFMISC_1:64;
  end;

theorem     :: ZFMISC_1:64 b
  I is non empty & y in X \ {x} implies y <> x
  proof
      assume that
A1:     I is non empty and
A2:     y in X \ {x};
      consider i such that
A3:     i in I by A1,XBOOLE_0:def 1;
        now
        take i;
          y.i in (X \ {x}).i by A2,A3,PBOOLE:def 4;
        then y.i in X.i \ {x}.i by A3,PBOOLE:def 9;
        then y.i in X.i \ {x.i} by A3,Def1;
        hence y.i <> x.i by ZFMISC_1:64;
      end;
      hence thesis;
  end;

theorem     :: ZFMISC_1:65
  I is non empty & X \ {x} = X implies not x in X
  proof
    assume that
A1:   I is non empty and
A2:   X \ {x} = X and
A3:   x in X;
A4: now
      let i; assume
A5:     i in I;
      hence X.i \ {x.i} = X.i \ {x}.i by Def1
                      .= X.i by A2,A5,PBOOLE:def 9;
    end;
      now
      consider i such that
A6:     i in I by A1,XBOOLE_0:def 1;
      take i;
      thus i in I by A6;
        X.i \ {x.i} = X.i by A4,A6;
      hence not x.i in X.i by ZFMISC_1:65;
    end;
    hence contradiction by A3,PBOOLE:def 4;
  end;

theorem     :: ZFMISC_1:67
  I is non empty & {x} \ X = {x} implies not x in X
  proof
    assume that
A1:   I is non empty and
A2:   {x} \ X = {x} and
A3:   x in X;
    consider i such that
A4:   i in I by A1,XBOOLE_0:def 1;
      {x.i} \ X.i = {x}.i \ X.i by A4,Def1
               .= ({x} \ X).i by A4,PBOOLE:def 9
               .= {x.i} by A2,A4,Def1;
    then not x.i in X.i by ZFMISC_1:67;
    hence contradiction by A3,A4,PBOOLE:def 4;
  end;

theorem     :: ZFMISC_1:68
  {x} \ X = [0]I iff x in X
  proof
    thus {x} \ X = [0]I implies x in X
    proof
      assume
A1:      {x} \ X = [0]I;
      let i; assume
A2:     i in I;
      then {x.i} \ X.i = {x}.i \ X.i by Def1
                 .= ({x} \ X).i by A2,PBOOLE:def 9
                 .= {} by A1,A2,PBOOLE:5;
      hence x.i in X.i by ZFMISC_1:68;
    end;
    assume
A3:   x in X;
      now
      let i; assume
A4:     i in I;
then A5:   x.i in X.i by A3,PBOOLE:def 4;
      thus ({x} \ X).i = {x}.i \ X.i by A4,PBOOLE:def 9
                      .= {x.i} \ X.i by A4,Def1
                      .= {} by A5,ZFMISC_1:68
                      .= [0]I.i by A4,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:70
  I is non empty & {x,y} \ X = {x} implies not x in X
  proof
    assume that
A1:   I is non empty and
A2:   {x,y} \ X = {x};
    consider i such that
A3:   i in I by A1,XBOOLE_0:def 1;
      {x.i,y.i} \ X.i = {x,y}.i \ X.i by A3,Def2
                   .= ({x,y} \ X).i by A3,PBOOLE:def 9
                   .= {x.i} by A2,A3,Def1;
    then not x.i in X.i by ZFMISC_1:70;
    hence thesis by A3,PBOOLE:def 4;
  end;

canceled;

theorem     :: ZFMISC_1:72
  I is non empty & {x,y} \ X = {x,y} implies not x in X & not y in X
  proof
    assume I is non empty;
    then consider i such that
A1:   i in I by XBOOLE_0:def 1;
    thus {x,y} \ X = {x,y} implies not x in X & not y in X
    proof
      assume
A2:     {x,y} \ X = {x,y};
      thus not x in X
      proof
        assume
A3:       x in X;
          {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2
                       .= ({x,y} \ X).i by A1,PBOOLE:def 9
                       .= {x.i,y.i} by A1,A2,Def2;
        then not x.i in X.i by ZFMISC_1:72;
        hence contradiction by A1,A3,PBOOLE:def 4;
      end;
      assume
A4:     y in X;
        {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2
                     .= ({x,y} \ X).i by A1,PBOOLE:def 9
                     .= {x.i,y.i} by A1,A2,Def2;
      then not y.i in X.i by ZFMISC_1:72;
      hence contradiction by A1,A4,PBOOLE:def 4;
    end;
  end;

theorem     :: ZFMISC_1:73
  {x,y} \ X = [0]I iff x in X & y in X
  proof
    thus {x,y} \ X = [0]I implies x in X & y in X
    proof
      assume
A1:     {x,y} \ X = [0]I;
      thus x in X
      proof
        let i; assume
A2:       i in I;
        then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2
                       .= ({x,y} \ X).i by A2,PBOOLE:def 9
                       .= {} by A1,A2,PBOOLE:5;
        hence x.i in X.i by ZFMISC_1:73;
      end;
      let i; assume
A3:     i in I;
      then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2
                     .= ({x,y} \ X).i by A3,PBOOLE:def 9
                     .= {} by A1,A3,PBOOLE:5;
      hence y.i in X.i by ZFMISC_1:73;
    end;
    assume
A4:   x in X & y in X;
      now
      let i; assume
A5:     i in I;
then A6:   x.i in X.i & y.i in X.i by A4,PBOOLE:def 4;
      thus ({x,y} \ X).i = {x,y}.i \ X.i by A5,PBOOLE:def 9
                        .= {x.i,y.i} \ X.i by A5,Def2
                        .= {} by A6,ZFMISC_1:73
                        .= [0]I.i by A5,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:75
  X = [0]I or X = {x} or X = {y} or X = {x,y} implies X \ {x,y} = [0]I
  proof
    assume
A1:   X = [0]I or X = {x} or X = {y} or X = {x,y};
      now
      let i such that
A2:     i in I;
      per cases by A1;
        suppose X = [0]I;
then A3:       X.i = {} by A2,PBOOLE:5;
          thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9
                            .= [0]I.i by A2,A3,PBOOLE:5;
        suppose X = {x};
then A4:       X.i = {x.i} by A2,Def1;
          thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9
                            .= X.i \ {x.i,y.i} by A2,Def2
                            .= {} by A4,ZFMISC_1:75
                            .= [0]I.i by A2,PBOOLE:5;
        suppose X = {y};
then A5:       X.i = {y.i} by A2,Def1;
          thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9
                            .= X.i \ {x.i,y.i} by A2,Def2
                            .= {} by A5,ZFMISC_1:75
                            .= [0]I.i by A2,PBOOLE:5;
        suppose X = {x,y};
then A6:       X.i = {x.i,y.i} by A2,Def2;
          thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9
                            .= X.i \ {x.i,y.i} by A2,Def2
                            .= {} by A6,ZFMISC_1:75
                            .= [0]I.i by A2,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

begin :: Cartesian product

theorem     :: ZFMISC_1:113
  X = [0]I or Y = [0]I implies [|X,Y|] = [0]I
  proof
    assume
A1:    X = [0]I or Y = [0]I;
    per cases by A1;
    suppose
A2:   X = [0]I;
      now
      let i; assume
A3:     i in I;
then A4:   X.i = {} by A2,PBOOLE:5;
      thus [|X,Y|].i = [:X.i,Y.i:] by A3,PRALG_2:def 9
                    .= {} by A4,ZFMISC_1:113
                    .= [0]I.i by A3,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
    suppose
A5:   Y = [0]I;
      now
      let i; assume
A6:     i in I;
then A7:   Y.i = {} by A5,PBOOLE:5;
      thus [|X,Y|].i = [:X.i,Y.i:] by A6,PRALG_2:def 9
                    .= {} by A7,ZFMISC_1:113
                    .= [0]I.i by A6,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:114
  X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y
  proof
    assume that
A1:   X is non-empty & Y is non-empty and
A2:   [|X,Y|] = [|Y,X|];
      now
      let i; assume
A3:     i in I;
then A4:   X.i is non empty & Y.i is non empty by A1,PBOOLE:def 16;
        [:X.i,Y.i:] = [|X,Y|].i by A3,PRALG_2:def 9
                 .= [:Y.i,X.i:] by A2,A3,PRALG_2:def 9;
      hence X.i = Y.i by A4,ZFMISC_1:114;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:115
  [|X,X|] = [|Y,Y|] implies X = Y
  proof
    assume
A1:   [|X,X|] = [|Y,Y|];
      now
      let i; assume
A2:     i in I;
      then [:X.i,X.i:] = [|X,X|].i by PRALG_2:def 9
                 .= [:Y.i,Y.i:] by A1,A2,PRALG_2:def 9;
      hence X.i = Y.i by ZFMISC_1:115;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:117
  Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y
  proof
    assume that
A1:   Z is non-empty and
A2:   [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|];
    per cases by A2;
    suppose
A3:   [|X,Z|] c= [|Y,Z|];
    let i; assume
A4:   i in I;
then A5: Z.i is non empty by A1,PBOOLE:def 16;
      [|X,Z|].i c= [|Y,Z|].i by A3,A4,PBOOLE:def 5;
    then [:X.i,Z.i:] c= [|Y,Z|].i by A4,PRALG_2:def 9;
    then [:X.i,Z.i:] c= [:Y.i,Z.i:] by A4,PRALG_2:def 9;
    hence X.i c= Y.i by A5,ZFMISC_1:117;
    suppose
A6:   [|Z,X|] c= [|Z,Y|];
    let i; assume
A7:   i in I;
then A8: Z.i is non empty by A1,PBOOLE:def 16;
      [|Z,X|].i c= [|Z,Y|].i by A6,A7,PBOOLE:def 5;
    then [:Z.i,X.i:] c= [|Z,Y|].i by A7,PRALG_2:def 9;
    then [:Z.i,X.i:] c= [:Z.i,Y.i:] by A7,PRALG_2:def 9;
    hence X.i c= Y.i by A8,ZFMISC_1:117;
  end;

theorem     :: ZFMISC_1:118
  X c= Y implies [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|]
  proof
    assume
A1:   X c= Y;
    thus [|X,Z|] c= [|Y,Z|]
    proof
      let i; assume
A2:     i in I;
      then X.i c= Y.i by A1,PBOOLE:def 5;
      then [:X.i,Z.i:] c= [:Y.i,Z.i:] by ZFMISC_1:118;
      then [|X,Z|].i c= [:Y.i,Z.i:] by A2,PRALG_2:def 9;
      hence [|X,Z|].i c= [|Y,Z|].i by A2,PRALG_2:def 9;
    end;
    let i; assume
A3:   i in I;
    then X.i c= Y.i by A1,PBOOLE:def 5;
    then [:Z.i,X.i:] c= [:Z.i,Y.i:] by ZFMISC_1:118;
    then [|Z,X|].i c= [:Z.i,Y.i:] by A3,PRALG_2:def 9;
    hence [|Z,X|].i c= [|Z,Y|].i by A3,PRALG_2:def 9;
  end;

theorem     :: ZFMISC_1:119
  x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|]
  proof
    assume
A1:   x1 c= A & x2 c= B;
    let i; assume
A2:   i in I;
    then x1.i c= A.i & x2.i c= B.i by A1,PBOOLE:def 5;
    then [:x1.i,x2.i:] c= [:A.i,B.i:] by ZFMISC_1:119;
    then [|x1,x2|].i c= [:A.i,B.i:] by A2,PRALG_2:def 9;
    hence [|x1,x2|].i c= [|A,B|].i by A2,PRALG_2:def 9;
  end;

theorem     :: ZFMISC_1:120
  [|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|]
  & [|Z, X \/ Y|] = [|Z, X|] \/ [|Z, Y|]
  proof
    thus [|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|]
    proof
        now
        let i; assume
A1:       i in I;
        hence [|X \/ Y, Z|].i = [:(X \/ Y).i, Z.i:] by PRALG_2:def 9
                           .= [:X.i \/ Y.i, Z.i:] by A1,PBOOLE:def 7
                           .= [:X.i, Z.i:] \/ [:Y.i, Z.i:] by ZFMISC_1:120
                           .= [|X,Z|].i \/ [:Y.i, Z.i:] by A1,PRALG_2:def 9
                           .= [|X,Z|].i \/ [|Y,Z|].i by A1,PRALG_2:def 9
                           .= ([|X, Z|] \/ [|Y, Z|]).i by A1,PBOOLE:def 7;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A2:     i in I;
      hence [|Z, X \/ Y|].i = [:Z.i, (X \/ Y).i:] by PRALG_2:def 9
                         .= [:Z.i, X.i \/ Y.i:] by A2,PBOOLE:def 7
                         .= [:Z.i,X.i:] \/ [:Z.i,Y.i:] by ZFMISC_1:120
                         .= [|Z,X|].i \/ [:Z.i,Y.i:] by A2,PRALG_2:def 9
                         .= [|Z,X|].i \/ [|Z,Y|].i by A2,PRALG_2:def 9
                         .= ([|Z,X|] \/ [|Z,Y|]).i by A2,PBOOLE:def 7;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:121
  [|x1 \/ x2, A \/ B|] = [|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|]
  proof
      now
      let i; assume
A1:     i in I;
      hence [|x1 \/ x2, A \/ B|].i = [:(x1 \/ x2).i,(A \/ B).i:]
                                                      by PRALG_2:def 9
      .= [:x1.i \/ x2.i, (A \/ B).i:] by A1,PBOOLE:def 7
      .= [:x1.i \/ x2.i, A.i \/ B.i:] by A1,PBOOLE:def 7
      .= [:x1.i,A.i:] \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
              by ZFMISC_1:121
      .= [|x1,A|].i \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
              by A1,PRALG_2:def 9
      .= [|x1,A|].i \/ [|x1,B|].i \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
              by A1,PRALG_2:def 9
      .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [:x2.i,B.i:]
              by A1,PRALG_2:def 9
      .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [|x2,B|].i
              by A1,PRALG_2:def 9
      .= ([|x1,A|] \/ [|x1,B|]).i \/ [|x2,A|].i \/ [|x2,B|].i
              by A1,PBOOLE:def 7
      .= ([|x1,A|] \/ [|x1,B|] \/ [|x2,A|]).i \/ [|x2,B|].i
              by A1,PBOOLE:def 7
      .= ([|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|]).i by A1,PBOOLE:def 7;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:122
  [|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|]
  & [|Z, X /\ Y|] = [|Z, X|] /\ [|Z, Y|]
  proof
    thus [|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|]
    proof
        now
        let i; assume
A1:       i in I;
        hence [|X /\ Y, Z|].i = [:(X /\ Y).i,Z.i:] by PRALG_2:def 9
              .= [:X.i /\ Y.i,Z.i:] by A1,PBOOLE:def 8
              .= [:X.i,Z.i:] /\ [:Y.i,Z.i:] by ZFMISC_1:122
              .= [|X,Z|].i /\ [:Y.i,Z.i:] by A1,PRALG_2:def 9
              .= [|X,Z|].i /\ [|Y,Z|].i by A1,PRALG_2:def 9
              .= ([|X, Z|] /\ [|Y, Z|]).i by A1,PBOOLE:def 8;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A2:       i in I;
      hence [|Z,X /\ Y|].i = [:Z.i,(X /\ Y).i:] by PRALG_2:def 9
            .= [:Z.i,X.i /\ Y.i:] by A2,PBOOLE:def 8
            .= [:Z.i,X.i:] /\ [:Z.i,Y.i:] by ZFMISC_1:122
            .= [|Z,X|].i /\ [:Z.i,Y.i:] by A2,PRALG_2:def 9
            .= [|Z,X|].i /\ [|Z,Y|].i by A2,PRALG_2:def 9
            .= ([|Z,X|] /\ [|Z,Y|]).i by A2,PBOOLE:def 8;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:123
  [|x1 /\ x2, A /\ B|] = [|x1,A|] /\ [|x2, B|]
  proof
      now
      let i; assume
A1:     i in I;
      hence [|x1 /\ x2, A /\ B|].i = [:(x1 /\ x2).i,(A /\ B).i:]
                                   by PRALG_2:def 9
                .= [:x1.i /\ x2.i,(A /\ B).i:] by A1,PBOOLE:def 8
                .= [:x1.i /\ x2.i,A.i /\ B.i:] by A1,PBOOLE:def 8
                .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by ZFMISC_1:123
                .= [|x1,A|].i /\ [:x2.i,B.i:] by A1,PRALG_2:def 9
                .= [|x1,A|].i /\ [|x2,B|].i by A1,PRALG_2:def 9
                .= ([|x1,A|] /\ [|x2, B|]).i by A1,PBOOLE:def 8;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:124
  A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|]
  proof
    assume
A1:   A c= X & B c= Y;
      now
      let i; assume
A2:     i in I;
then A3:   A.i c= X.i & B.i c= Y.i by A1,PBOOLE:def 5;
      thus ([|A,Y|] /\ [|X,B|]).i = [|A,Y|].i /\ [|X,B|].i by A2,PBOOLE:def 8
                   .= [:A.i,Y.i:] /\ [|X,B|].i by A2,PRALG_2:def 9
                   .= [:A.i,Y.i:] /\ [:X.i,B.i:] by A2,PRALG_2:def 9
                   .= [:A.i,B.i:] by A3,ZFMISC_1:124
                   .= [|A,B|].i by A2,PRALG_2:def 9;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:125
  [|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|]
  & [|Z, X \ Y|] = [|Z, X|] \ [|Z, Y|]
  proof
    thus [|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|]
    proof
        now
        let i; assume
A1:       i in I;
        hence [|X \ Y, Z|].i = [:(X \ Y).i,Z.i:] by PRALG_2:def 9
                .= [:X.i \ Y.i,Z.i:] by A1,PBOOLE:def 9
                .= [:X.i,Z.i:] \ [:Y.i,Z.i:] by ZFMISC_1:125
                .= [|X,Z|].i \ [:Y.i,Z.i:] by A1,PRALG_2:def 9
                .= [|X,Z|].i \ [|Y,Z|].i by A1,PRALG_2:def 9
                .= ([|X, Z|] \ [|Y, Z|]).i by A1,PBOOLE:def 9;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A2:       i in I;
      hence [|Z,X \ Y|].i = [:Z.i,(X \ Y).i:] by PRALG_2:def 9
              .= [:Z.i,X.i \ Y.i:] by A2,PBOOLE:def 9
              .= [:Z.i,X.i:] \ [:Z.i,Y.i:] by ZFMISC_1:125
              .= [|Z,X|].i \ [:Z.i,Y.i:] by A2,PRALG_2:def 9
              .= [|Z,X|].i \ [|Z,Y|].i by A2,PRALG_2:def 9
              .= ([|Z,X|] \ [|Z,Y|]).i by A2,PBOOLE:def 9;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:126
  [|x1,x2|] \ [|A,B|] = [|x1\A,x2|] \/ [|x1,x2\B|]
  proof
      now
      let i; assume
A1:     i in I;
      hence ([|x1,x2|] \ [|A,B|]).i = [|x1,x2|].i \ [|A,B|].i
                     by PBOOLE:def 9
             .= [:x1.i,x2.i:] \ [|A,B|].i by A1,PRALG_2:def 9
             .= [:x1.i,x2.i:] \ [:A.i,B.i:] by A1,PRALG_2:def 9
             .= [:x1.i\A.i,x2.i:] \/ [:x1.i,x2.i\B.i:] by ZFMISC_1:126
             .= [:(x1\A).i,x2.i:] \/ [:x1.i,x2.i\B.i:] by A1,PBOOLE:def 9
             .= [:(x1\A).i,x2.i:] \/ [:x1.i,(x2\B).i:] by A1,PBOOLE:def 9
             .= [|x1\A,x2|].i \/ [:x1.i,(x2\B).i:] by A1,PRALG_2:def 9
             .= [|x1\A,x2|].i \/ [|x1,x2\B|].i by A1,PRALG_2:def 9
             .= ([|x1\A,x2|] \/ [|x1,x2\B|]).i by A1,PBOOLE:def 7;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:127
  x1 /\ x2 = [0]I or A /\ B = [0]I implies [|x1,A|] /\ [|x2,B|] = [0]I
  proof
    assume
A1:   x1 /\ x2 = [0]I or A /\ B= [0]I;
    per cases by A1;
    suppose
A2:     x1 /\ x2 = [0]I;
      now
      let i; assume
A3:     i in I;
then x1.i /\ x2.i = (x1 /\ x2).i by PBOOLE:def 8
                 .= {} by A2,A3,PBOOLE:5;
    then x1.i misses x2.i by XBOOLE_0:def 7;
then A4:   [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:127;
      thus ([|x1,A|] /\ [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i
                   by A3,PBOOLE:def 8
           .= [:x1.i,A.i:] /\ [|x2,B|].i by A3,PRALG_2:def 9
           .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A3,PRALG_2:def 9
           .= {} by A4,XBOOLE_0:def 7
           .= [0]I.i by A3,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
    suppose
A5:     A /\ B = [0]I;
      now
      let i; assume
A6:     i in I;
then A.i /\ B.i = (A /\ B).i by PBOOLE:def 8
               .= {} by A5,A6,PBOOLE:5;
then A.i misses B.i by XBOOLE_0:def 7;
then A7:   [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:127;
      thus ([|x1,A|] /\ [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i
                   by A6,PBOOLE:def 8
           .= [:x1.i,A.i:] /\ [|x2,B|].i by A6,PRALG_2:def 9
           .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A6,PRALG_2:def 9
           .= {} by A7,XBOOLE_0:def 7
           .= [0]I.i by A6,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:130
  X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty
  proof
    assume
A1:   X is non-empty;
    thus [|{x},X|] is non-empty
    proof
      let i; assume
A2:     i in I;
      then X.i is non empty by A1,PBOOLE:def 16;
      then [:{x.i},X.i:] is non empty by ZFMISC_1:130;
      then [:{x}.i,X.i:] is non empty by A2,Def1;
      hence [|{x},X|].i is non empty by A2,PRALG_2:def 9;
    end;
    let i; assume
A3:   i in I;
    then X.i is non empty by A1,PBOOLE:def 16;
    then [:X.i,{x.i}:] is non empty by ZFMISC_1:130;
    then [:X.i,{x}.i:] is non empty by A3,Def1;
    hence [|X,{x}|].i is non empty by A3,PRALG_2:def 9;
  end;

theorem     :: ZFMISC_1:132
  [|{x,y},X|] = [|{x},X|] \/ [|{y},X|]
  & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|]
  proof
    thus [|{x,y},X|] = [|{x},X|] \/ [|{y},X|]
    proof
        now
        let i; assume
A1:       i in I;
        hence [|{x,y},X|].i = [:{x,y}.i,X.i:] by PRALG_2:def 9
                          .= [:{x.i,y.i},X.i:] by A1,Def2
                          .= [:{x.i},X.i:] \/ [:{y.i},X.i:] by ZFMISC_1:132
                          .= [:{x}.i,X.i:] \/ [:{y.i},X.i:] by A1,Def1
                          .= [:{x}.i,X.i:] \/ [:{y}.i,X.i:] by A1,Def1
                          .= [|{x},X|].i \/ [:{y}.i,X.i:] by A1,PRALG_2:def 9
                          .= [|{x},X|].i \/ [|{y},X|].i by A1,PRALG_2:def 9
                          .= ([|{x},X|] \/ [|{y},X|]).i by A1,PBOOLE:def 7;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A2:       i in I;
      hence [|X,{x,y}|].i = [:X.i,{x,y}.i:] by PRALG_2:def 9
                        .= [:X.i,{x.i,y.i}:] by A2,Def2
                        .= [:X.i,{x.i}:] \/ [:X.i,{y.i}:] by ZFMISC_1:132
                        .= [:X.i,{x}.i:] \/ [:X.i,{y.i}:] by A2,Def1
                        .= [:X.i,{x}.i:] \/ [:X.i,{y}.i:] by A2,Def1
                        .= [|X,{x}|].i \/ [:X.i,{y}.i:] by A2,PRALG_2:def 9
                        .= [|X,{x}|].i \/ [|X,{y}|].i by A2,PRALG_2:def 9
                        .= ([|X,{x}|] \/ [|X,{y}|]).i by A2,PBOOLE:def 7;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:134
  x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|]
  implies x1 = x2 & A = B
  proof
    assume that
A1:   x1 is non-empty & A is non-empty and
A2:   [|x1,A|] = [|x2,B|];
    thus x1 = x2
    proof
        now
        let i; assume
A3:       i in I;
then A4:     x1.i is non empty & A.i is non empty by A1,PBOOLE:def 16;
          [:x1.i,A.i:] = [|x1,A|].i by A3,PRALG_2:def 9
                    .= [:x2.i,B.i:] by A2,A3,PRALG_2:def 9;
        hence x1.i = x2.i by A4,ZFMISC_1:134;
      end;
      hence thesis by PBOOLE:3;
    end;
      now
      let i; assume
A5:     i in I;
then A6:   x1.i is non empty & A.i is non empty by A1,PBOOLE:def 16;
        [:x1.i,A.i:] = [|x1,A|].i by A5,PRALG_2:def 9
                  .= [:x2.i,B.i:] by A2,A5,PRALG_2:def 9;
      hence A.i = B.i by A6,ZFMISC_1:134;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ZFMISC_1:116, 135
  X c= [|X,Y|] or X c= [|Y,X|] implies X = [0]I
  proof
    assume
A1:   X c= [|X,Y|] or X c= [|Y,X|];
    per cases by A1;
    suppose
A2:   X c= [|X,Y|];
        now
        let i; assume
A3:       i in I;
        then X.i c= [|X,Y|].i by A2,PBOOLE:def 5;
        then X.i c= [:X.i,Y.i:] by A3,PRALG_2:def 9;
        hence X.i = {} by ZFMISC_1:135
                 .= [0]I.i by A3,PBOOLE:5;
      end;
      hence thesis by PBOOLE:3;
    suppose
A4:   X c= [|Y,X|];
        now
        let i; assume
A5:       i in I;
        then X.i c= [|Y,X|].i by A4,PBOOLE:def 5;
        then X.i c= [:Y.i,X.i:] by A5,PRALG_2:def 9;
        hence X.i = {} by ZFMISC_1:135
                 .= [0]I.i by A5,PBOOLE:5;
      end;
      hence thesis by PBOOLE:3;
  end;

theorem     :: BORSUK_1:2
  A in [|x,y|] & A in [|X,Y|] implies A in [|x /\ X, y /\ Y|]
  proof
    assume
A1:   A in [|x,y|] & A in [|X,Y|];
    let i; assume
A2:   i in I;
    then A.i in [|x,y|].i & A.i in [|X,Y|].i by A1,PBOOLE:def 4;
    then A.i in [:x.i,y.i:] & A.i in [:X.i,Y.i:] by A2,PRALG_2:def 9;
    then A.i in [:x.i /\ X.i, y.i /\ Y.i:] by BORSUK_1:2;
    then A.i in [:(x /\ X).i, y.i /\ Y.i:] by A2,PBOOLE:def 8;
    then A.i in [:(x /\ X).i, (y /\ Y).i:] by A2,PBOOLE:def 8;
    hence thesis by A2,PRALG_2:def 9;
  end;

theorem     :: BORSUK_1:7
  [|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y
  proof
    assume that
A1:   [|x,X|] c= [|y,Y|] and
A2:   [|x,X|] is non-empty;
    thus x c= y
    proof
      let i; assume
A3:     i in I;
      then [|x,X|].i c= [|y,Y|].i by A1,PBOOLE:def 5;
      then [:x.i,X.i:] c= [|y,Y|].i by A3,PRALG_2:def 9;
then A4:   [:x.i,X.i:] c= [:y.i,Y.i:] by A3,PRALG_2:def 9;
        [|x,X|].i is non empty by A2,A3,PBOOLE:def 16;
      then [:x.i,X.i:] is non empty by A3,PRALG_2:def 9;
      hence x.i c= y.i by A4,BORSUK_1:7;
    end;
    let i; assume
A5:   i in I;
    then [|x,X|].i c= [|y,Y|].i by A1,PBOOLE:def 5;
    then [:x.i,X.i:] c= [|y,Y|].i by A5,PRALG_2:def 9;
then A6: [:x.i,X.i:] c= [:y.i,Y.i:] by A5,PRALG_2:def 9;
      [|x,X|].i is non empty by A2,A5,PBOOLE:def 16;
    then [:x.i,X.i:] is non empty by A5,PRALG_2:def 9;
    hence X.i c= Y.i by A6,BORSUK_1:7;
  end;

theorem     :: REALSET1:4
  A c= X implies [|A,A|] c= [|X,X|]
  proof
    assume
A1:   A c= X;
    let i; assume
A2:   i in I;
    then A.i c= X.i by A1,PBOOLE:def 5;
    then [:A.i,A.i:] c= [:X.i,X.i:] by ZFMISC_1:119;
    then [|A,A|].i c= [:X.i,X.i:] by A2,PRALG_2:def 9;
    hence [|A,A|].i c= [|X,X|].i by A2,PRALG_2:def 9;
  end;

theorem     :: SYSREL:17
  X /\ Y = [0]I implies [|X,Y|] /\ [|Y,X|] = [0]I
  proof
    assume
A1:   X /\ Y = [0]I;
      now
      let i; assume
A2:     i in I;
then X.i /\ Y.i = (X /\ Y).i by PBOOLE:def 8
               .= {} by A1,A2,PBOOLE:5;
    then X.i misses Y.i by XBOOLE_0:def 7;
then A3:   [:X.i,Y.i:] misses [:Y.i,X.i:] by ZFMISC_1:127;
      thus ([|X,Y|] /\ [|Y,X|]).i = [|X,Y|].i /\ [|Y,X|].i by A2,PBOOLE:def 8
                          .= [:X.i,Y.i:] /\ [|Y,X|].i by A2,PRALG_2:def 9
                          .= [:X.i,Y.i:] /\ [:Y.i,X.i:] by A2,PRALG_2:def 9
                          .= {} by A3,XBOOLE_0:def 7
                          .= [0]I.i by A2,PBOOLE:5;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem     :: ALTCAT_1:1
  A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y
  proof
   assume that
A1:  A is non-empty and
A2:  [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|];
   per cases by A2;
   suppose
A3:    [|A,B|] c= [|X,Y|];
     let i; assume
A4:    i in I;
     then [|A,B|].i c= [|X,Y|].i by A3,PBOOLE:def 5;
     then [:A.i,B.i:] c= [|X,Y|].i by A4,PRALG_2:def 9;
then A5:  [:A.i,B.i:] c= [:X.i,Y.i:] by A4,PRALG_2:def 9;
       A.i is non empty by A1,A4,PBOOLE:def 16;
     hence B.i c= Y.i by A5,ALTCAT_1:1;
   suppose
A6:    [|B,A|] c= [|Y,X|];
     let i; assume
A7:    i in I;
     then [|B,A|].i c= [|Y,X|].i by A6,PBOOLE:def 5;
     then [:B.i,A.i:] c= [|Y,X|].i by A7,PRALG_2:def 9;
then A8:  [:B.i,A.i:] c= [:Y.i,X.i:] by A7,PRALG_2:def 9;
       A.i is non empty by A1,A7,PBOOLE:def 16;
     hence B.i c= Y.i by A8,ALTCAT_1:1;
 end;

theorem     :: PARTFUN1:1
  x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|A \/ X,B \/ Y|]
  proof
    assume
A1:   x c= [|A,B|] & y c= [|X,Y|];
    let i; assume
A2:   i in I;
    then x.i c= [|A,B|].i & y.i c= [|X,Y|].i by A1,PBOOLE:def 5;
    then x.i c= [:A.i,B.i:] & y.i c= [:X.i,Y.i:] by A2,PRALG_2:def 9;
    then x.i \/ y.i c= [:A.i \/ X.i,B.i \/ Y.i:] by PARTFUN1:1;
    then (x \/ y).i c= [:A.i \/ X.i,B.i \/ Y.i:] by A2,PBOOLE:def 7;
    then (x \/ y).i c= [:(A \/ X).i,B.i \/ Y.i:] by A2,PBOOLE:def 7;
    then (x \/ y).i c= [:(A \/ X).i,(B \/ Y).i:] by A2,PBOOLE:def 7;
    hence thesis by A2,PRALG_2:def 9;
  end;

Back to top