The Mizar article:

$N$-Tuples and Cartesian Products for $n=5$

by
Michal Muzalewski, and
Wojciech Skaba

Received October 13, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: MCART_2
[ MML identifier index ]


environ

 vocabulary BOOLE, MCART_1, TARSKI, MCART_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1;
 constructors TARSKI, MCART_1, MEMBERED, XBOOLE_0;
 clusters MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 theorems TARSKI, ZFMISC_1, MCART_1, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0;

begin

  reserve x,x1,x2,x3,x4,x5, y,y1,y2,y3,y4,y5,
          X,X1,X2,X3,X4,X5, Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,
          Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7 for set;
  reserve xx1 for Element of X1, xx2 for Element of X2,
          xx3 for Element of X3, xx4 for Element of X4,
          xx5 for Element of X5;

Lm1:
 X1 <> {} & X2 <> {} implies
 for x being Element of [:X1,X2:]
  ex xx1 being (Element of X1),
     xx2 being Element of X2 st x = [xx1,xx2]
 proof
   assume
A1:  X1 <> {} & X2 <> {};
then A2:  [:X1,X2:] <> {} by ZFMISC_1:113;
   let x be Element of [:X1,X2:];
   reconsider xx1 = x`1 as Element of X1 by A2,MCART_1:10;
   reconsider xx2 = x`2 as Element of X2 by A2,MCART_1:10;
   take xx1,xx2;
   thus x = [xx1,xx2] by A1,MCART_1:24;
 end;

Lm2:
 X1 <> {} & X2 <> {} & X3 <> {} implies
 for x being Element of [:X1,X2,X3:]
  ex xx1,xx2,xx3 st x = [xx1,xx2,xx3]
 proof
    assume
A1:  X1 <> {} & X2 <> {} & X3 <> {};
then A2:  [:X1,X2:] <> {} by ZFMISC_1:113;
    let x be Element of [:X1,X2,X3:];
    reconsider x'=x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
    consider x12 being (Element of [:X1,X2:]), xx3 such that
A3:    x' = [x12,xx3] by A1,A2,Lm1;
    consider xx1,xx2 such that
A4:    x12 = [xx1,xx2] by A1,Lm1;
    take xx1,xx2,xx3;
    thus x = [xx1,xx2,xx3] by A3,A4,MCART_1:def 3;
 end;

Lm3:
 X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies
 for x being Element of [:X1,X2,X3,X4:]
  ex xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4]
 proof
   assume
A1:  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {};
then A2:  [:X1,X2,X3:] <> {} by MCART_1:35;
   let x be Element of [:X1,X2,X3,X4:];
   reconsider x'=x as Element of [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
   consider x123 being (Element of [:X1,X2,X3:]), xx4 such that
A3:   x' = [x123,xx4] by A1,A2,Lm1;
   consider xx1,xx2,xx3 such that
A4:   x123 = [xx1,xx2,xx3] by A1,Lm2;
   take xx1,xx2,xx3,xx4;
   thus x = [xx1,xx2,xx3,xx4] by A3,A4,MCART_1:def 4;
 end;

theorem
   X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3,Y4,Y5,Y6
    st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
        holds Y1 misses X
 proof
  defpred P[set] means
    ex Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1
                                             & Y1 meets X;
  consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from Separation;
  defpred Q[set] means
    ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X;
  consider Z2 such that
A2:  for Y holds Y in Z2 iff Y in union union X & Q[Y] from Separation;
  defpred R[set] means
    ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;
  consider Z3 such that
A3:  for Y holds Y in Z3 iff Y in union union union X & R[Y]
           from Separation;
  defpred S[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
  consider Z4 such that
A4:  for Y holds Y in Z4 iff
         Y in union union union union X & S[Y] from Separation;
  defpred T[set] means ex Y1 st Y1 in $1 & Y1 meets X;
  consider Z5 such that
A5:  for Y holds Y in Z5 iff
         Y in union union union union union X & T[Y] from Separation;
  defpred U[set] means $1 meets X;
  consider Z6 such that
A6:  for Y holds Y in Z6 iff
         Y in union union union union union union X & U[Y] from Separation;
   set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6;
A7: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4;
  assume X <> {};
  then V <> {} by A7,XBOOLE_1:15;
  then consider Y such that
A8:  Y in V and
A9:  Y misses V by MCART_1:1;
  assume
A10: not thesis;
     now assume
A11:  Y in X;
     then consider Y1,Y2,Y3,Y4,Y5,Y6 such that
A12:   Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
   & not Y1 misses X by A10;
        Y6 in union X & Y1 meets X by A11,A12,TARSKI:def 4;
     then Y6 in Z1 by A1,A12;
     then Y6 in X \/ Z1 by XBOOLE_0:def 2;
     then Y6 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
     then Y6 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
     then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by A12,XBOOLE_0:3;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70;
    hence contradiction by A9,XBOOLE_1:70;
   end;
   then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by A7,A8,XBOOLE_0:def 2;
   then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4;
   then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4;
   then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4;
then A13: Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4;
     now assume
A14:  Y in Z1;
     then consider Y1,Y2,Y3,Y4,Y5 such that
A15:    Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A1;
       Y in union X by A1,A14;
     then Y5 in union union X by A15,TARSKI:def 4;
     then Y5 in Z2 by A2,A15;
     then Y5 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
     then Y meets X \/ Z1 \/ Z2 by A15,XBOOLE_0:3;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70;
    hence contradiction by A9,XBOOLE_1:70;
   end;
   then Y in Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by A13,XBOOLE_0:def 2;
   then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4;
   then Y in Z2 \/ (Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4;
then A16: Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4;
     now assume
A17:  Y in Z2;
     then consider Y1,Y2,Y3,Y4 such that
A18:    Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A2;
       Y in union union X by A2,A17;
     then Y4 in union union union X by A18,TARSKI:def 4;
     then Y4 in Z3 by A3,A18;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y4 in V by XBOOLE_0:def 2;
    hence contradiction by A9,A18,XBOOLE_0:3;
   end;
   then Y in Z3 \/ Z4 \/ Z5 \/ Z6 by A16,XBOOLE_0:def 2;
   then Y in Z3 \/ (Z4 \/ Z5) \/ Z6 by XBOOLE_1:4;
then A19: Y in Z3 \/ (Z4 \/ Z5 \/ Z6) by XBOOLE_1:4;
     now assume
A20:  Y in Z3;
     then consider Y1,Y2,Y3 such that
A21:    Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A3;
       Y in union union union X by A3,A20;
     then Y3 in union union union union X by A21,TARSKI:def 4;
     then Y3 in Z4 by A4,A21;
     then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y3 in V by XBOOLE_0:def 2;
    hence contradiction by A9,A21,XBOOLE_0:3;
   end;
   then Y in Z4 \/ Z5 \/ Z6 by A19,XBOOLE_0:def 2;
then A22: Y in Z4 \/ (Z5 \/ Z6) by XBOOLE_1:4;
     now assume
A23:  Y in Z4;
     then consider Y1,Y2 such that
A24:    Y1 in Y2 & Y2 in Y & Y1 meets X by A4;
       Y in union union union union X by A4,A23;
     then Y2 in union union union union union X by A24,TARSKI:def 4;
     then Y2 in Z5 by A5,A24;
     then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y2 in V by XBOOLE_0:def 2;
    hence contradiction by A9,A24,XBOOLE_0:3;
   end;
   then A25: Y in Z5 \/ Z6 by A22,XBOOLE_0:def 2;
     now assume
A26:  Y in Z5;
     then consider Y1 such that
A27:    Y1 in Y & Y1 meets X by A5;
       Y in union union union union union X by A5,A26;
     then Y1 in union union union union union union X by A27,TARSKI:def 4;
     then Y1 in Z6 by A6,A27;
     then Y1 in V by XBOOLE_0:def 2;
    hence contradiction by A9,A27,XBOOLE_0:3;
   end;
   then Y in Z6 by A25,XBOOLE_0:def 2;
   then Y meets X by A6;
  hence contradiction by A7,A9,XBOOLE_1:70;
 end;

theorem
Th2:
 X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3,Y4,Y5,Y6,Y7
    st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
 Y
        holds Y1 misses X
 proof
  defpred P[set] means
    ex Y1,Y2,Y3,Y4,Y5,Y6 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 &
                            Y5 in Y6 & Y6 in $1 & Y1 meets X;
  consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from Separation;
  defpred Q[set] means
    ex Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 &
                            Y5 in $1 & Y1 meets X;
  consider Z2 such that
A2:  for Y holds Y in Z2 iff Y in union union X & Q[Y] from Separation;
  defpred R[set] means
    ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X;
  consider Z3 such that
A3:  for Y holds Y in Z3 iff Y in union union union X & R[Y] from Separation;
  defpred S[set] means
    ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;
  consider Z4 such that
A4:  for Y holds Y in Z4 iff
         Y in union union union union X & S[Y] from Separation;
  defpred T[set] means
    ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
  consider Z5 such that
A5:  for Y holds Y in Z5 iff
         Y in union union union union union X & T[Y] from Separation;
  defpred U[set] means ex Y1 st Y1 in $1 & Y1 meets X;
  consider Z6 such that
A6:  for Y holds Y in Z6 iff
         Y in union union union union union union X & U[Y] from Separation;
  defpred V[set] means $1 meets X;
  consider Z7 such that
A7:  for Y holds Y in Z7 iff
         Y in union union union union union union union X & V[Y]
                                              from Separation;
   set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7;
A8: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4
    .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4;
  assume X <> {};
  then V <> {} by A8,XBOOLE_1:15;
  then consider Y such that
A9:  Y in V and
A10:  Y misses V by MCART_1:1;
  assume
A11: not thesis;
     now assume
A12:  Y in X;
     then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that
A13:   Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
 Y
   & not Y1 misses X by A11;

        Y7 in union X & Y1 meets X by A12,A13,TARSKI:def 4;
     then Y7 in Z1 by A1,A13;
     then Y7 in X \/ Z1 by XBOOLE_0:def 2;
     then Y7 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
     then Y7 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
     then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A13,XBOOLE_0:3;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
    hence contradiction by A10,XBOOLE_1:70;
   end;
   then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A8,A9,XBOOLE_0:def 2;
   then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4;
then A14: Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4;
     now assume
A15:  Y in Z1;
     then consider Y1,Y2,Y3,Y4,Y5,Y6 such that
A16:    Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
                                                       & Y1 meets X by A1;
       Y in union X by A1,A15;
     then Y6 in union union X by A16,TARSKI:def 4;
     then Y6 in Z2 by A2,A16;
     then Y6 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
     then Y meets X \/ Z1 \/ Z2 by A16,XBOOLE_0:3;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70;
     then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
    hence contradiction by A10,XBOOLE_1:70;
   end;
   then Y in Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A14,XBOOLE_0:def 2;
   then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z2 \/ (Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4;
then A17: Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4;
     now assume
A18:  Y in Z2;
     then consider Y1,Y2,Y3,Y4,Y5 such that
A19:    Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A2;
       Y in union union X by A2,A18;
     then Y5 in union union union X by A19,TARSKI:def 4;
     then Y5 in Z3 by A3,A19;
     then Y5 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
     then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
     then Y5 in V by XBOOLE_0:def 2;
    hence contradiction by A10,A19,XBOOLE_0:3;
   end;
   then Y in Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A17,XBOOLE_0:def 2;
   then Y in Z3 \/ (Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4;
   then Y in Z3 \/ (Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4;
then A20: Y in Z3 \/ (Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4;
     now assume
A21:  Y in Z3;
     then consider Y1,Y2,Y3,Y4 such that
A22:    Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A3;
       Y in union union union X by A3,A21;
     then Y4 in union union union union X by A22,TARSKI:def 4;
     then Y4 in Z4 by A4,A22;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
     then Y4 in V by XBOOLE_0:def 2;
    hence contradiction by A10,A22,XBOOLE_0:3;
   end;
   then Y in Z4 \/ Z5 \/ Z6 \/ Z7 by A20,XBOOLE_0:def 2;
   then Y in Z4 \/ (Z5 \/ Z6) \/ Z7 by XBOOLE_1:4;
then A23: Y in Z4 \/ (Z5 \/ Z6 \/ Z7) by XBOOLE_1:4;
     now assume
A24:  Y in Z4;
     then consider Y1,Y2,Y3 such that
A25:    Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A4;
       Y in union union union union X by A4,A24;
     then Y3 in union union union union union X by A25,TARSKI:def 4;
     then Y3 in Z5 by A5,A25;
     then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
     then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
     then Y3 in V by XBOOLE_0:def 2;
    hence contradiction by A10,A25,XBOOLE_0:3;
   end;
   then Y in Z5 \/ Z6 \/ Z7 by A23,XBOOLE_0:def 2;
then A26: Y in Z5 \/ (Z6 \/ Z7) by XBOOLE_1:4;
     now assume
A27:  Y in Z5;
     then consider Y1,Y2 such that
A28:    Y1 in Y2 & Y2 in Y & Y1 meets X by A5;
       Y in union union union union union X by A5,A27;
     then Y2 in union union union union union union X by A28,TARSKI:def 4;
     then Y2 in Z6 by A6,A28;
     then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
     then Y2 in V by XBOOLE_0:def 2;
    hence contradiction by A10,A28,XBOOLE_0:3;
   end;
   then A29: Y in Z6 \/ Z7 by A26,XBOOLE_0:def 2;
     now assume
A30:  Y in Z6;
     then consider Y1 such that
A31:    Y1 in Y & Y1 meets X by A6;
       Y in union union union union union union X by A6,A30;
     then Y1 in
 union union union union union union union X by A31,TARSKI:def 4;
     then Y1 in Z7 by A7,A31;
     then Y1 in V by XBOOLE_0:def 2;
    hence contradiction by A10,A31,XBOOLE_0:3;
   end;
   then Y in Z7 by A29,XBOOLE_0:def 2;
   then Y meets X by A7;
  hence contradiction by A8,A10,XBOOLE_1:70;
 end;

::
::   Tuples for n=5
::

definition
  let x1,x2,x3,x4,x5;
  func [x1,x2,x3,x4,x5] equals
  :Def1:  [[x1,x2,x3,x4],x5];
  correctness;
end;

theorem
Th3: [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5]
 proof
  thus [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5] by Def1
                       .= [[[x1,x2,x3],x4],x5] by MCART_1:def 4
                       .= [[[[x1,x2],x3],x4],x5] by MCART_1:def 3;
 end;

canceled;

theorem
   [x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5]
  proof
    thus [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5] by Th3
                         .= [[[x1,x2],x3],x4,x5] by MCART_1:def 3
                         .= [[x1,x2,x3],x4,x5] by MCART_1:def 3;
  end;

theorem
Th6: [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5]
  proof
    thus [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5] by Th3
                         .= [[[x1,x2],x3],x4,x5] by MCART_1:def 3
                         .= [[x1,x2],x3,x4,x5] by MCART_1:32;
 end;

theorem Th7:
  [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5]
  implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5
     proof
       assume [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5];
       then [[x1,x2,x3,x4],x5] = [y1,y2,y3,y4,y5] by Def1
                              .= [[y1,y2,y3,y4],y5] by Def1;
       then [x1,x2,x3,x4] = [y1,y2,y3,y4]
          & x5 = y5 by ZFMISC_1:33;
       hence thesis by MCART_1:33;
 end;

theorem Th8:
 X <> {} implies
  ex x st x in X &
   not ex x1,x2,x3,x4,x5 st (x1 in X or x2 in X) & x = [x1,x2,x3,x4,x5]
 proof
   assume X <> {};
   then consider Y such that
A1:  Y in X and
A2:  for Y1,Y2,Y3,Y4,Y5,Y6,Y7
      st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7
in Y
               holds Y1 misses X by Th2;
   take x = Y;
   thus x in X by A1;
   given x1,x2,x3,x4,x5 such that
A3:  x1 in X or x2 in X and
A4:  x = [x1,x2,x3,x4,x5];
   set Y1 = { x1, x2 },
       Y2 = { Y1, {x1} },
       Y3 = { Y2, x3 },
       Y4 = { Y3, {Y2} },
       Y5 = { Y4, x4 },
       Y6 = { Y5, {Y4} },
       Y7 = { Y6, x5 };
     x1 in Y1 & x2 in Y1 by TARSKI:def 2;
   then A5: not Y1 misses X by A3,XBOOLE_0:3;
      Y = [[[[x1,x2],x3],x4],x5] by A4,Th3
     .= [[[ Y2,x3],x4],x5 ] by TARSKI:def 5
     .= [[ Y4,x4],x5 ] by TARSKI:def 5
     .= [ Y6,x5 ] by TARSKI:def 5
     .= { Y7, { Y6 } } by TARSKI:def 5;
   then Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7
in
 Y
                                                               by TARSKI:def 2;
  hence contradiction by A2,A5;
 end;

::
::   Cartesian products of five sets
::

definition
  let X1,X2,X3,X4,X5;
  func [:X1,X2,X3,X4,X5:] -> set equals
  :Def2:  [:[: X1,X2,X3,X4 :],X5 :];
  correctness;
end;

theorem Th9:
 [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:]
  proof
   thus [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] by Def2
                          .= [:[:[:X1,X2,X3:],X4:],X5:] by ZFMISC_1:def 4
                          .= [:[:[:[:X1,X2:],X3:],X4:],X5:] by ZFMISC_1:def 3;
  end;

canceled;

theorem
   [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:]
  proof
    thus [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:] by Th9
                           .= [:[:[:X1,X2:],X3:],X4,X5:] by ZFMISC_1:def 3
                           .= [:[:X1,X2,X3:],X4,X5:] by ZFMISC_1:def 3;
  end;

theorem
Th12: [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:]
  proof
    thus [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:] by Th9
                           .= [:[:[:X1,X2:],X3:],X4,X5:] by ZFMISC_1:def 3
                           .= [:[:X1,X2:],X3,X4,X5:] by MCART_1:54;
 end;

theorem
 Th13: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {}
   iff [:X1,X2,X3,X4,X5:] <> {}
 proof
A1: [:[:X1,X2,X3,X4:],X5:] = [:X1,X2,X3,X4,X5:] by Def2;
     X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {}
   iff [:X1,X2,X3,X4:] <> {} by MCART_1:55;
   hence thesis by A1,ZFMISC_1:113;
 end;

theorem Th14:
 X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
  ( [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:]
    implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 )
proof
A1: [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] by Def2;
 assume
A2: X1<>{} & X2<>{} & X3<>{} & X4<>{};
 then A3: [:X1,X2,X3,X4:] <> {} by MCART_1:55;
 assume
A4: X5<>{};
  assume [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:];
  then [:[:X1,X2,X3,X4:],X5:] = [:[:Y1,Y2,Y3,Y4:],Y5:] by A1,Def2;
  then [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] & X5 = Y5 by A3,A4,ZFMISC_1:134;
  hence thesis by A2,MCART_1:56;
end;

theorem
   [:X1,X2,X3,X4,X5:]<>{} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:]
   implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5
proof
  assume [:X1,X2,X3,X4,X5:]<>{};
  then X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} by Th13;
 hence thesis by Th14;
end;

theorem
    [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:] implies X = Y
proof
 assume [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:];
  then X<>{} or Y<>{} implies thesis by Th14;
  hence X = Y;
end;

theorem Th17:
 X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} implies
 for x being Element of [:X1,X2,X3,X4,X5:]
   ex xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5]
 proof
   assume
A1:  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {};
then A2:  [:X1,X2,X3,X4:] <> {} by MCART_1:55;
  let x be Element of [:X1,X2,X3,X4,X5:];
   reconsider x'=x as Element of [:[:X1,X2,X3,X4:],X5:] by Def2;
   consider x1234 being (Element of [:X1,X2,X3,X4:]), xx5 such that
A3:   x' = [x1234,xx5] by A1,A2,Lm1;
   consider xx1,xx2,xx3,xx4 such that
A4:   x1234 = [xx1,xx2,xx3,xx4] by A1,Lm3;
  take xx1,xx2,xx3,xx4,xx5;
  thus x = [xx1,xx2,xx3,xx4,xx5] by A3,A4,Def1;
 end;

definition
  let X1,X2,X3,X4,X5;
  assume A1:X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{};
  let x be Element of [:X1,X2,X3,X4,X5:];
  func x`1 -> Element of X1 means
:Def3: x = [x1,x2,x3,x4,x5] implies it = x1;
  existence
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A2:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    take xx1;
    thus thesis by A2,Th7;
   end;
  uniqueness
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A3:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    let y,z be Element of X1;
    assume x = [x1,x2,x3,x4,x5] implies y = x1;
then A4:   y = xx1 by A3;
    assume x = [x1,x2,x3,x4,x5] implies z = x1;
    hence thesis by A3,A4;
   end;

  func x`2 -> Element of X2 means
:Def4: x = [x1,x2,x3,x4,x5] implies it = x2;
  existence
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A5:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    take xx2; thus thesis by A5,Th7;
   end;
  uniqueness
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A6:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    let y,z be Element of X2;
    assume x = [x1,x2,x3,x4,x5] implies y = x2;
then A7:   y = xx2 by A6;
    assume x = [x1,x2,x3,x4,x5] implies z = x2;
    hence thesis by A6,A7;
   end;

  func x`3 -> Element of X3 means
:Def5: x = [x1,x2,x3,x4,x5] implies it = x3;
  existence
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A8:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    take xx3; thus thesis by A8,Th7;
   end;
  uniqueness
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A9:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    let y,z be Element of X3;
    assume x = [x1,x2,x3,x4,x5] implies y = x3;
then A10:   y = xx3 by A9;
    assume x = [x1,x2,x3,x4,x5] implies z = x3;
    hence thesis by A9,A10;
   end;

  func x`4 -> Element of X4 means
:Def6: x = [x1,x2,x3,x4,x5] implies it = x4;
  existence
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A11:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    take xx4; thus thesis by A11,Th7;
   end;
  uniqueness
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A12:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    let y,z be Element of X4;
    assume x = [x1,x2,x3,x4,x5] implies y = x4;
then A13:   y = xx4 by A12;
    assume x = [x1,x2,x3,x4,x5] implies z = x4;
    hence thesis by A12,A13;
   end;

  func x`5 -> Element of X5 means
:Def7: x = [x1,x2,x3,x4,x5] implies it = x5;
  existence
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A14:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    take xx5; thus thesis by A14,Th7;
   end;
  uniqueness
   proof
    consider xx1,xx2,xx3,xx4,xx5 such that
A15:   x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
    let y,z be Element of X5;
    assume x = [x1,x2,x3,x4,x5] implies y = x5;
then A16:   y = xx5 by A15;
    assume x = [x1,x2,x3,x4,x5] implies z = x5;
    hence thesis by A15,A16;
   end;
 end;

theorem
  X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
 for x being Element of [:X1,X2,X3,X4,X5:]
  for x1,x2,x3,x4,x5 st x = [x1,x2,x3,x4,x5] holds
   x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5
                                           by Def3,Def4,Def5,Def6,Def7;

theorem Th19:
 X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
 for x being Element of [:X1,X2,X3,X4,X5:] holds x = [x`1,x`2,x`3,x`4,x`5]
 proof
   assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{};
  let x be Element of [:X1,X2,X3,X4,X5:];
  consider xx1,xx2,xx3,xx4,xx5 such that
A2:  x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17;
  thus x = [x`1,xx2,xx3,xx4,xx5] by A1,A2,Def3
        .= [x`1,x`2,xx3,xx4,xx5] by A1,A2,Def4
        .= [x`1,x`2,x`3,xx4,xx5] by A1,A2,Def5
        .= [x`1,x`2,x`3,x`4,xx5] by A1,A2,Def6
        .= [x`1,x`2,x`3,x`4,x`5] by A1,A2,Def7;
 end;

theorem
Th20:
 X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
 for x being Element of [:X1,X2,X3,X4,X5:] holds
   x`1 = (x qua set)`1`1`1`1 &
   x`2 = (x qua set)`1`1`1`2 &
   x`3 = (x qua set)`1`1`2 &
   x`4 = (x qua set)`1`2 &
   x`5 = (x qua set)`2
 proof
   assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{};
  let x be Element of [:X1,X2,X3,X4,X5:];
  thus x`1 = [ x`1, x`2]`1 by MCART_1:7
          .= [[x`1, x`2],x`3]`1`1 by MCART_1:7
          .= [ x`1, x`2 ,x`3]`1`1 by MCART_1:def 3
          .= [[x`1, x`2 ,x`3],x`4]`1`1`1 by MCART_1:7
          .= [ x`1, x`2 ,x`3 ,x`4]`1`1`1 by MCART_1:def 4
          .= [[x`1, x`2 ,x`3 ,x`4], x`5]`1`1`1`1 by MCART_1:7
          .= [ x`1, x`2 ,x`3 ,x`4 , x`5]`1`1`1`1 by Def1
          .= (x qua set)`1`1`1`1 by A1,Th19;
  thus x`2 = [ x`1, x`2]`2 by MCART_1:7
          .= [[x`1, x`2],x`3]`1`2 by MCART_1:7
          .= [ x`1, x`2, x`3]`1`2 by MCART_1:def 3
          .= [[x`1, x`2, x`3],x`4]`1`1`2 by MCART_1:7
          .= [ x`1, x`2, x`3, x`4]`1`1`2 by MCART_1:def 4
          .= [[x`1, x`2, x`3, x`4 ], x`5]`1`1`1`2 by MCART_1:7
          .= [ x`1, x`2, x`3, x`4 , x`5]`1`1`1`2 by Def1
          .= (x qua set)`1`1`1`2 by A1,Th19;
  thus x`3 = [[x`1, x`2],x`3]`2 by MCART_1:7
          .= [ x`1, x`2, x`3]`2 by MCART_1:def 3
          .= [[x`1, x`2, x`3],x`4]`1`2 by MCART_1:7
          .= [ x`1, x`2, x`3, x`4]`1`2 by MCART_1:def 4
          .= [[x`1, x`2, x`3, x`4],x`5]`1`1`2 by MCART_1:7
          .= [ x`1, x`2, x`3, x`4 ,x`5]`1`1`2 by Def1
          .= (x qua set)`1`1`2 by A1,Th19;
  thus x`4 = [[x`1,x`2,x`3],x`4]`2 by MCART_1:7
          .= [ x`1,x`2,x`3, x`4]`2 by MCART_1:def 4
          .= [[x`1,x`2,x`3, x`4],x`5]`1`2 by MCART_1:7
          .= [ x`1,x`2,x`3, x`4 ,x`5]`1`2 by Def1
          .= (x qua set)`1`2 by A1,Th19;
  thus x`5 = [[x`1,x`2,x`3,x`4],x`5]`2 by MCART_1:7
          .= [ x`1,x`2,x`3,x`4 ,x`5]`2 by Def1
          .= (x qua set)`2 by A1,Th19;
 end;

theorem
      X1 c= [:X1,X2,X3,X4,X5:]
 or X1 c= [:X2,X3,X4,X5,X1:]
 or X1 c= [:X3,X4,X5,X1,X2:]
 or X1 c= [:X4,X5,X1,X2,X3:]
 or X1 c= [:X5,X1,X2,X3,X4:]
 implies X1 = {}
proof
  assume that
A1:    X1 c= [:X1,X2,X3,X4,X5:]
   or X1 c= [:X2,X3,X4,X5,X1:]
   or X1 c= [:X3,X4,X5,X1,X2:]
   or X1 c= [:X4,X5,X1,X2,X3:]
   or X1 c= [:X5,X1,X2,X3,X4:]
   and
A2: X1 <> {};
         [:X1,X2,X3,X4,X5:]<>{}
    or [:X2,X3,X4,X5,X1:]<>{}
    or [:X3,X4,X5,X1,X2:]<>{}
    or [:X4,X5,X1,X2,X3:]<>{}
    or [:X5,X1,X2,X3,X4:]<>{} by A1,A2,XBOOLE_1:3;
then A3: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} by Th13;
    now per cases by A1;
   suppose
A4:  X1 c= [:X1,X2,X3,X4,X5:];
     consider x such that
A5:   x in X1 and
A6:   for x1,x2,x3,x4,x5
       st x1 in X1 or x2 in X1 holds x <> [x1,x2,x3,x4,x5] by A2,Th8;
      reconsider x as Element of [:X1,X2,X3,X4,X5:] by A4,A5;
        x = [x`1,x`2,x`3,x`4,x`5] & x`1 in X1 by A3,Th19;
    hence contradiction by A6;

   suppose X1 c= [:X2,X3,X4,X5,X1:];
    then X1 c= [:[:X2,X3:],X4,X5,X1:] by Th12;
    hence thesis by A2,MCART_1:63;

   suppose X1 c= [:X3,X4,X5,X1,X2:];
    then X1 c= [:[:X3,X4:],X5,X1,X2:] by Th12;
    hence thesis by A2,MCART_1:63;

   suppose X1 c= [:X4,X5,X1,X2,X3:];
    then X1 c= [:[:X4,X5:],X1,X2,X3:] by Th12;
    hence thesis by A2,MCART_1:63;

   suppose
A7:  X1 c= [:X5,X1,X2,X3,X4:];
     consider x such that
A8:   x in X1 and
A9:   for x1,x2,x3,x4,x5
      st x1 in X1 or x2 in X1 holds x <> [x1,x2,x3,x4,x5] by A2,Th8;
      reconsider x as Element of [:X5,X1,X2,X3,X4:] by A7,A8;
        x = [x`1,x`2,x`3,x`4,x`5] & x`2 in X1 by A3,Th19;
    hence thesis by A9;
  end;
 hence contradiction;
end;

theorem
   [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] implies
   X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5
proof
A1: [:[:[:[:X1,X2:],X3:],X4:],X5:] = [:X1,X2,X3,X4,X5:]
 & [:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:] = [:Y1,Y2,Y3,Y4,Y5:] by Th9;
 assume [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:];
  then [:[:[:X1,X2:],X3:],X4:] meets [:[:[:Y1,Y2:],Y3:],Y4:]
                                         & X5 meets Y5 by A1,ZFMISC_1:127;
  then [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:]
                          & X4 meets Y4 & X5 meets Y5 by ZFMISC_1:127;
  then [:X1,X2:] meets [:Y1,Y2:]
           & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 by ZFMISC_1:127;
 hence thesis by ZFMISC_1:127;
end;

theorem [:{x1},{x2},{x3},{x4},{x5}:] = { [x1,x2,x3,x4,x5] }
 proof thus
      [:{x1},{x2},{x3},{x4},{x5}:]
  = [:[:{x1},{x2}:],{x3},{x4},{x5}:] by Th12
 .= [:{[x1,x2]}, {x3},{x4},{x5}:] by ZFMISC_1:35
 .= { [[x1,x2], x3, x4, x5]} by MCART_1:65
 .= { [x1,x2,x3,x4,x5] } by Th6;
 end;

reserve A1 for Subset of X1,
        A2 for Subset of X2,
        A3 for Subset of X3,
        A4 for Subset of X4,
        A5 for Subset of X5;

:: 5 - Tuples

reserve x for Element of [:X1,X2,X3,X4,X5:];

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
  for x1,x2,x3,x4,x5 st x = [x1,x2,x3,x4,x5]
   holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 by Def3,Def4,Def5
,Def6,Def7;

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
  (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y1 = xx1)
   implies y1 =x`1
 proof
   assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and
A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y1 = xx1;
     x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19;
  hence thesis by A2;
 end;

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
  (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y2 = xx2)
   implies y2 =x`2
 proof
   assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and
A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y2 = xx2;
     x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19;
  hence thesis by A2;
 end;

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
  (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y3 = xx3)
   implies y3 =x`3
 proof
   assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and
A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y3 = xx3;
     x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19;
  hence thesis by A2;
 end;

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
  (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y4 = xx4)
   implies y4 =x`4
 proof
   assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and
A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y4 = xx4;
     x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19;
  hence thesis by A2;
 end;

theorem
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
  (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y5 = xx5)
   implies y5 =x`5
 proof
   assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and
A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y5 = xx5;
     x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19;
  hence thesis by A2;
 end;

theorem
   y in [: X1,X2,X3,X4,X5 :] implies
  ex x1,x2,x3,x4,x5
  st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & y = [x1,x2,x3,x4,x5]
   proof
     assume y in [: X1,X2,X3,X4,X5 :];
     then y in [:[:X1,X2,X3,X4:],X5:] by Def2;
     then consider x1234, x5 being set such that
A1:   x1234 in [:X1,X2,X3,X4:] and
A2:   x5 in X5 and
A3:   y = [x1234,x5] by ZFMISC_1:def 2;
     consider x1, x2, x3, x4 such that
A4:   x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4
    & x1234 = [x1,x2,x3,x4] by A1,MCART_1:83;
       y = [x1,x2,x3,x4,x5] by A3,A4,Def1;
    hence thesis by A2,A4;
   end;

theorem
       [x1,x2,x3,x4,x5] in [: X1,X2,X3,X4,X5 :]
 iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   proof
A1: [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:] by Th12;
A2: [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5] by Th6;
       [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106;
    hence thesis by A1,A2,MCART_1:84;
   end;

theorem
   (for y holds y in Z iff
  ex x1,x2,x3,x4,x5
  st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & y = [x1,x2,x3,x4,x5])
  implies Z = [: X1,X2,X3,X4,X5 :]
  proof
   assume
A1:   for y holds y in Z iff
       ex x1,x2,x3,x4,x5
       st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
        & y = [x1,x2,x3,x4,x5];
      now let y;
     thus y in Z implies y in [:[:X1,X2,X3,X4:],X5:]
      proof
        assume y in Z; then consider x1,x2,x3,x4,x5 such that
A2:      x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
      & y = [x1,x2,x3,x4,x5] by A1;
A3:      y = [[x1,x2,x3,x4],x5] by A2,Def1;
          [x1,x2,x3,x4] in [:X1,X2,X3,X4:] & x5 in X5 by A2,MCART_1:84;
       hence y in [:[:X1,X2,X3,X4:],X5:] by A3,ZFMISC_1:def 2;
      end;
     assume y in [:[:X1,X2,X3,X4:],X5:];
      then consider x1234,x5 being set such that
A4:     x1234 in [:X1,X2,X3,X4:] and
A5:     x5 in X5 and
A6:     y = [x1234,x5] by ZFMISC_1:def 2;
      consider x1,x2,x3,x4 such that
A7:   x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4
    & x1234 = [x1,x2,x3,x4] by A4,MCART_1:83;
         y = [x1,x2,x3,x4,x5] by A6,A7,Def1;
     hence y in Z by A1,A5,A7;
    end;
    then Z = [:[:X1,X2,X3,X4:],X5:] by TARSKI:2;
   hence Z = [: X1,X2,X3,X4,X5 :] by Def2;
  end;

theorem Th33:
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{}
 & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} implies
  for x being Element of [:X1,X2,X3,X4,X5:],
      y being Element of [:Y1,Y2,Y3,Y4,Y5:]
  holds x = y
  implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5
 proof
   assume that
A1: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} and
A2: Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {};
  let x be Element of [:X1,X2,X3,X4,X5:];
  let y be Element of [:Y1,Y2,Y3,Y4,Y5:];
  assume
A3: x = y;
  thus x`1 = (x qua set)`1`1`1`1 by A1,Th20 .= y`1 by A2,A3,Th20;
  thus x`2 = (x qua set)`1`1`1`2 by A1,Th20 .= y`2 by A2,A3,Th20;
  thus x`3 = (x qua set)`1`1`2 by A1,Th20 .= y`3 by A2,A3,Th20;
  thus x`4 = (x qua set)`1`2 by A1,Th20 .= y`4 by A2,A3,Th20;
  thus x`5 = (x qua set)`2 by A1,Th20 .= y`5 by A2,A3,Th20;
 end;

theorem
   for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:]
   holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5
 proof
   let x be Element of [:X1,X2,X3,X4,X5:];
  assume
A1: x in [:A1,A2,A3,A4,A5:];
   then A2: A1 <> {} & A2 <> {} & A3 <> {} & A4 <> {} & A5 <> {} by Th13;
   reconsider y = x as Element of [:A1,A2,A3,A4,A5:] by A1;
     y`1 in A1 & y`2 in A2 & y`3 in A3 & y`4 in A4 & y`5 in A5 by A2;
  hence x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5 by Th33;
 end;

theorem Th35:
 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5
  implies [:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]
 proof
    assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4;
    then A1: [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] by MCART_1:88;
A2: [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] &
    [:Y1,Y2,Y3,Y4,Y5:] = [:[:Y1,Y2,Y3,Y4:],Y5:] by Def2;
  assume X5 c= Y5;
  hence thesis by A1,A2,ZFMISC_1:119;
 end;

definition
  let X1,X2,X3,X4,X5,A1,A2,A3,A4,A5;
  redefine func [:A1,A2,A3,A4,A5:] -> Subset of [:X1,X2,X3,X4,X5:];
  coherence by Th35;
end;

theorem
   X1 <> {} & X2 <> {} implies
 for xx being Element of [:X1,X2:]
  ex xx1 being (Element of X1),
     xx2 being Element of X2 st xx = [xx1,xx2] by Lm1;

theorem
   X1 <> {} & X2 <> {} & X3 <> {} implies
 for xx being Element of [:X1,X2,X3:]
  ex xx1,xx2,xx3 st xx = [xx1,xx2,xx3] by Lm2;

theorem
   X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies
 for xx being Element of [:X1,X2,X3,X4:]
  ex xx1,xx2,xx3,xx4 st xx = [xx1,xx2,xx3,xx4] by Lm3;


Back to top