:: Consequences of Regularity Axiom
:: by Andrzej Trybulec
::
:: Received January 30, 2012
:: Copyright (c) 2012-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0, ENUMSET1;
constructors TARSKI, XBOOLE_0, ENUMSET1;
registrations XBOOLE_0;
requirements BOOLE;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ENUMSET1;
schemes XFAMILY;
begin
reserve x,y,X1,X2,X3,X4,X5,X6,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set;
reserve X for non empty set;
:: To jest po prostu "poprawne" sformulowanie aksjomatu regularnosci
:: W TARSKI 'misses' jest rozekspandowane, zeby uniknac definiowania 'misses'
theorem Th1:
ex Y st Y in X & Y misses X
proof
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
consider Y such that
A2: Y in X and
A3: not ex x be object st x in X & x in Y by A1,TARSKI:3;
take Y;
not ex x being object st x in X & x in Y by A3;
hence thesis by A2,XBOOLE_0:3;
end;
theorem
ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X
proof
defpred P[set] means $1 meets X;
consider Z such that
A1: for Y holds Y in Z iff Y in union X & P[Y] from XFAMILY:sch 1;
consider Y such that
A2: Y in X \/ Z and
A3: Y misses X \/ Z by Th1;
assume
A4: not thesis;
now
assume
A5: Y in X;
then consider Y1 such that
A6: Y1 in Y and
A7: not Y1 misses X by A4;
Y1 in union X by A5,A6,TARSKI:def 4;
then Y1 in Z by A1,A7;
then Y1 in X \/ Z by XBOOLE_0:def 3;
hence contradiction by A3,A6,XBOOLE_0:3;
end;
then Y in Z by A2,XBOOLE_0:def 3;
then Y meets X by A1;
hence contradiction by A3,XBOOLE_1:70;
end;
theorem
ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X
proof
defpred P[set] means ex Y1 st Y1 in $1 & Y1 meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from XFAMILY:sch 1;
defpred Q[set] means $1 meets X;
consider Z2 such that
A2: for Y holds Y in Z2 iff Y in union union X & Q[Y] from XFAMILY:sch 1;
consider Y such that
A3: Y in X \/ Z1 \/ Z2 and
A4: Y misses X \/ Z1 \/ Z2 by Th1;
A5: now
assume
A6: Y in Z1;
then consider Y1 such that
A7: Y1 in Y and
A8: Y1 meets X by A1;
Y in union X by A1,A6;
then Y1 in union union X by A7,TARSKI:def 4;
then Y1 in Z2 by A2,A8;
then Y1 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
hence contradiction by A4,A7,XBOOLE_0:3;
end;
assume
A9: not thesis;
A10: now
assume
A11: Y in X;
then consider Y1,Y2 such that
A12: Y1 in Y2 and
A13: Y2 in Y and
A14: not Y1 misses X by A9;
Y2 in union X by A11,A13,TARSKI:def 4;
then Y2 in Z1 by A1,A12,A14;
then Y2 in X \/ Z1 by XBOOLE_0:def 3;
then Y2 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
hence contradiction by A4,A13,XBOOLE_0:3;
end;
Y in X \/ (Z1 \/ Z2) by A3,XBOOLE_1:4;
then Y in Z1 \/ Z2 by A10,XBOOLE_0:def 3;
then Y in Z2 by A5,XBOOLE_0:def 3;
then Y meets X by A2;
then Y meets X \/ Z1 by XBOOLE_1:70;
hence contradiction by A4,XBOOLE_1:70;
end;
theorem
ex Y st Y in X &
for Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X
proof
defpred P[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from XFAMILY:sch 1;
defpred R[set] means $1 meets X;
defpred Q[set] means ex Y1 st Y1 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 XFAMILY:sch
1;
consider Z3 such that
A3: for Y holds Y in Z3 iff Y in union union union X & R[Y]
from XFAMILY:sch 1;
consider Y such that
A4: Y in X \/ Z1 \/ Z2 \/ Z3 and
A5: Y misses X \/ Z1 \/ Z2 \/ Z3 by Th1;
A6: now
assume
A7: Y in Z2;
then consider Y1 such that
A8: Y1 in Y and
A9: Y1 meets X by A2;
Y in union union X by A2,A7;
then Y1 in union union union X by A8,TARSKI:def 4;
then Y1 in Z3 by A3,A9;
then Y1 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
hence contradiction by A5,A8,XBOOLE_0:3;
end;
A10: now
assume
A11: Y in Z1;
then consider Y1,Y2 such that
A12: Y1 in Y2 and
A13: Y2 in Y and
A14: Y1 meets X by A1;
Y in union X by A1,A11;
then Y2 in union union X by A13,TARSKI:def 4;
then Y2 in Z2 by A2,A12,A14;
then Y2 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y meets X \/ Z1 \/ Z2 by A13,XBOOLE_0:3;
hence contradiction by A5,XBOOLE_1:70;
end;
set V = X \/ Z1 \/ Z2 \/ Z3;
A15: V = X \/ (Z1 \/ Z2) \/ Z3 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3) by XBOOLE_1:4;
assume
A16: not thesis;
now
assume
A17: Y in X;
then consider Y1,Y2,Y3 such that
A18: Y1 in Y2 & Y2 in Y3 and
A19: Y3 in Y and
A20: not Y1 misses X by A16;
Y3 in union X by A17,A19,TARSKI:def 4;
then Y3 in Z1 by A1,A18,A20;
then Y3 in X \/ Z1 by XBOOLE_0:def 3;
then Y3 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y3 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
hence contradiction by A5,A19,XBOOLE_0:3;
end;
then Y in Z1 \/ Z2 \/ Z3 by A15,A4,XBOOLE_0:def 3;
then Y in Z1 \/ (Z2 \/ Z3) by XBOOLE_1:4;
then Y in Z2 \/ Z3 by A10,XBOOLE_0:def 3;
then Y in Z3 by A6,XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A15,A5,XBOOLE_1:70;
end;
theorem
ex Y st Y in X &
for Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y
holds Y1 misses X
proof
defpred P[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1
meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from XFAMILY:sch 1;
defpred S[set] means $1 meets X;
defpred R[set] means ex Y1 st Y1 in $1 & Y1 meets X;
defpred Q[set] means ex Y1,Y2 st Y1 in Y2 & Y2 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 XFAMILY:sch
1;
consider Z4 such that
A3: for Y holds Y in Z4 iff Y in union union union union X & S[Y] from
XFAMILY:sch 1;
consider Z3 such that
A4: for Y holds Y in Z3 iff Y in union union union X & R[Y] from
XFAMILY:sch 1;
consider Y such that
A5: Y in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 and
A6: Y misses X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by Th1;
A7: now
assume
A8: Y in Z3;
then consider Y1 such that
A9: Y1 in Y and
A10: Y1 meets X by A4;
Y in union union union X by A4,A8;
then Y1 in union union union union X by A9,TARSKI:def 4;
then Y1 in Z4 by A3,A10;
then Y1 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 3;
hence contradiction by A6,A9,XBOOLE_0:3;
end;
A11: now
assume
A12: Y in Z1;
then consider Y1,Y2,Y3 such that
A13: Y1 in Y2 & Y2 in Y3 and
A14: Y3 in Y and
A15: Y1 meets X by A1;
Y in union X by A1,A12;
then Y3 in union union X by A14,TARSKI:def 4;
then Y3 in Z2 by A2,A13,A15;
then Y3 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y meets X \/ Z1 \/ Z2 by A14,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70;
hence contradiction by A6,XBOOLE_1:70;
end;
A16: X \/ Z1 \/ Z2 \/ Z3 \/ Z4 = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) by XBOOLE_1:4;
A17: now
assume
A18: Y in Z2;
then consider Y1,Y2 such that
A19: Y1 in Y2 and
A20: Y2 in Y and
A21: Y1 meets X by A2;
Y in union union X by A2,A18;
then Y2 in union union union X by A20,TARSKI:def 4;
then Y2 in Z3 by A4,A19,A21;
then Y2 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 by A20,XBOOLE_0:3;
hence contradiction by A6,XBOOLE_1:70;
end;
assume
A22: not thesis;
now
assume
A23: Y in X;
then consider Y1,Y2,Y3,Y4 such that
A24: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 and
A25: Y4 in Y and
A26: not Y1 misses X by A22;
Y4 in union X by A23,A25,TARSKI:def 4;
then Y4 in Z1 by A1,A24,A26;
then Y4 in X \/ Z1 by XBOOLE_0:def 3;
then Y4 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y4 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 3;
hence contradiction by A6,A25,XBOOLE_0:3;
end;
then Y in Z1 \/ Z2 \/ Z3 \/ Z4 by A16,A5,XBOOLE_0:def 3;
then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 by XBOOLE_1:4;
then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) by XBOOLE_1:4;
then Y in Z2 \/ Z3 \/ Z4 by A11,XBOOLE_0:def 3;
then Y in Z2 \/ (Z3 \/ Z4) by XBOOLE_1:4;
then Y in Z3 \/ Z4 by A17,XBOOLE_0:def 3;
then Y in Z4 by A7,XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A16,A6,XBOOLE_1:70;
end;
theorem
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y
holds Y1 misses X
proof
defpred P[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4
in $1 & Y1 meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P[Y] from XFAMILY:sch 1;
defpred T[set] means $1 meets X;
defpred S[set] means ex Y1 st Y1 in $1 & Y1 meets X;
defpred R[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
defpred Q[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 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 XFAMILY:sch
1;
consider Z5 such that
A3: for Y holds Y in Z5 iff Y in union union union union union X & T[Y]
from XFAMILY:sch 1;
consider Z3 such that
A4: for Y holds Y in Z3 iff Y in union union union X & R[Y] from
XFAMILY:sch 1;
consider Z4 such that
A5: for Y holds Y in Z4 iff Y in union union union union X & S[Y] from
XFAMILY:sch 1;
set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5;
consider Y such that
A6: Y in V and
A7: Y misses V by Th1;
A8: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) by XBOOLE_1:4;
A9: now
assume
A10: Y in Z1;
then consider Y1,Y2,Y3,Y4 such that
A11: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 and
A12: Y4 in Y and
A13: Y1 meets X by A1;
Y in union X by A1,A10;
then Y4 in union union X by A12,TARSKI:def 4;
then Y4 in Z2 by A2,A11,A13;
then Y4 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y meets X \/ Z1 \/ Z2 by A12,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;
hence contradiction by A7,XBOOLE_1:70;
end;
A14: now
assume
A15: Y in Z2;
then consider Y1,Y2,Y3 such that
A16: Y1 in Y2 & Y2 in Y3 and
A17: Y3 in Y and
A18: Y1 meets X by A2;
Y in union union X by A2,A15;
then Y3 in union union union X by A17,TARSKI:def 4;
then Y3 in Z3 by A4,A16,A18;
then Y3 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 3;
then Y3 in V by XBOOLE_0:def 3;
hence contradiction by A7,A17,XBOOLE_0:3;
end;
A19: now
assume
A20: Y in Z3;
then consider Y1,Y2 such that
A21: Y1 in Y2 and
A22: Y2 in Y and
A23: Y1 meets X by A4;
Y in union union union X by A4,A20;
then Y2 in union union union union X by A22,TARSKI:def 4;
then Y2 in Z4 by A5,A21,A23;
then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 3;
then Y2 in V by XBOOLE_0:def 3;
hence contradiction by A7,A22,XBOOLE_0:3;
end;
A24: now
assume
A25: Y in Z4;
then consider Y1 such that
A26: Y1 in Y and
A27: Y1 meets X by A5;
Y in union union union union X by A5,A25;
then Y1 in union union union union union X by A26,TARSKI:def 4;
then Y1 in Z5 by A3,A27;
then Y1 in V by XBOOLE_0:def 3;
hence contradiction by A7,A26,XBOOLE_0:3;
end;
assume
A28: not thesis;
now
assume
A29: Y in X;
then consider Y1,Y2,Y3,Y4,Y5 such that
A30: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 and
A31: Y5 in Y and
A32: not Y1 misses X by A28;
Y5 in union X by A29,A31,TARSKI:def 4;
then Y5 in Z1 by A1,A30,A32;
then Y5 in X \/ Z1 by XBOOLE_0:def 3;
then Y5 in X \/ Z1 \/ Z2 by XBOOLE_0:def 3;
then Y5 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 by A31,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70;
hence contradiction by A7,XBOOLE_1:70;
end;
then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A8,A6,XBOOLE_0:def 3;
then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 by XBOOLE_1:4;
then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 by XBOOLE_1:4;
then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) by XBOOLE_1:4;
then Y in Z2 \/ Z3 \/ Z4 \/ Z5 by A9,XBOOLE_0:def 3;
then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 by XBOOLE_1:4;
then Y in Z2 \/ (Z3 \/ Z4 \/ Z5) by XBOOLE_1:4;
then Y in Z3 \/ Z4 \/ Z5 by A14,XBOOLE_0:def 3;
then Y in Z3 \/ (Z4 \/ Z5) by XBOOLE_1:4;
then Y in Z4 \/ Z5 by A19,XBOOLE_0:def 3;
then Y in Z5 by A24,XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A8,A7,XBOOLE_1:70;
end;
:: Opuszczone dwa przypadki, ktore odpowiadaja irrefleksywnosci
:: i asymetri
theorem
not ( X1 in X2 & X2 in X3 & X3 in X1)
proof
A1: X2 in { X1,X2,X3 } & X3 in { X1,X2,X3 } by ENUMSET1:def 1;
A2: X1 in { X1,X2,X3 } by ENUMSET1:def 1;
then consider T being set such that
A3: T in { X1,X2,X3 } and
A4: { X1,X2,X3 } misses T by Th1;
T = X1 or T = X2 or T = X3 by A3,ENUMSET1:def 1;
hence thesis by A2,A1,A4,XBOOLE_0:3;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X1)
proof
A1: X2 in { X1,X2,X3,X4 } & X3 in { X1,X2,X3,X4 } by ENUMSET1:def 2;
A2: X4 in { X1,X2,X3,X4 } by ENUMSET1:def 2;
A3: X1 in { X1,X2,X3,X4 } by ENUMSET1:def 2;
then consider T being set such that
A4: T in { X1,X2,X3,X4 } and
A5: { X1,X2,X3,X4 } misses T by Th1;
T = X1 or T = X2 or T = X3 or T = X4 by A4,ENUMSET1:def 2;
hence thesis by A3,A1,A2,A5,XBOOLE_0:3;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1)
proof
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X1;
set Z = { X1,X2,X3,X4,X5 };
A6: for Y st Y in Z holds Z meets Y
proof
let Y such that
A7: Y in Z;
now
per cases by A7,ENUMSET1:def 3;
suppose
A8: Y = X1;
take y = X5;
thus y in Z & y in Y by A5,A8,ENUMSET1:def 3;
end;
suppose
A9: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A9,ENUMSET1:def 3;
end;
suppose
A10: Y = X3;
take y = X2;
thus y in Z & y in Y by A2,A10,ENUMSET1:def 3;
end;
suppose
A11: Y = X4;
take y = X3;
thus y in Z & y in Y by A3,A11,ENUMSET1:def 3;
end;
suppose
A12: Y = X5;
take y = X4;
thus y in Z & y in Y by A4,A12,ENUMSET1:def 3;
end;
end;
hence thesis by XBOOLE_0:3;
end;
X1 in { X1,X2,X3,X4,X5 } by ENUMSET1:def 3;
hence contradiction by A6,Th1;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1)
proof
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X6 and
A6: X6 in X1;
set Z = { X1,X2,X3,X4,X5,X6 };
A7: for Y st Y in Z holds Z meets Y
proof
let Y such that
A8: Y in Z;
now
per cases by A8,ENUMSET1:def 4;
suppose
A9: Y = X1;
take y = X6;
thus y in Z & y in Y by A6,A9,ENUMSET1:def 4;
end;
suppose
A10: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A10,ENUMSET1:def 4;
end;
suppose
A11: Y = X3;
take y = X2;
thus y in Z & y in Y by A2,A11,ENUMSET1:def 4;
end;
suppose
A12: Y = X4;
take y = X3;
thus y in Z & y in Y by A3,A12,ENUMSET1:def 4;
end;
suppose
A13: Y = X5;
take y = X4;
thus y in Z & y in Y by A4,A13,ENUMSET1:def 4;
end;
suppose
A14: Y = X6;
take y = X5;
thus y in Z & y in Y by A5,A14,ENUMSET1:def 4;
end;
end;
hence thesis by XBOOLE_0:3;
end;
X1 in { X1,X2,X3,X4,X5,X6 } by ENUMSET1:def 4;
hence contradiction by A7,Th1;
end;