:: Boolean Properties of Sets - Theorems
:: by Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002-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;
constructors TARSKI, XBOOLE_0;
registrations XBOOLE_0;
requirements BOOLE;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0;
begin
reserve x,A,B,X,X9,Y,Y9,Z,V for set;
::$N Modus Barbara
theorem
X c= Y & Y c= Z implies X c= Z;
theorem
{} c= X;
theorem Th3:
X c= {} implies X = {}
proof
assume X c= {};
hence X c= {} & {} c= X;
end;
theorem Th4:
(X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
thus (X \/ Y) \/ Z c= X \/ (Y \/ Z)
proof
let x be object;
assume x in (X \/ Y) \/ Z;
then x in X \/ Y or x in Z by XBOOLE_0:def 3;
then x in X or x in Y or x in Z by XBOOLE_0:def 3;
then x in X or x in Y \/ Z by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in X \/ (Y \/ Z);
then x in X or x in Y \/ Z by XBOOLE_0:def 3;
then x in X or x in Y or x in Z by XBOOLE_0:def 3;
then x in X \/ Y or x in Z by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proof
(X \/ Y) \/ Z = X \/ ((Z \/ Z) \/ Y) by Th4
.= X \/ (Z \/ (Z \/ Y)) by Th4
.= (X \/ Z) \/ (Y \/ Z) by Th4;
hence thesis;
end;
theorem
X \/ (X \/ Y) = X \/ Y
proof
X \/ (X \/ Y) = (X \/ X) \/ Y by Th4
.= X \/ Y;
hence thesis;
end;
theorem Th7:
X c= X \/ Y
by XBOOLE_0:def 3;
theorem Th8:
X c= Z & Y c= Z implies X \/ Y c= Z
proof
assume
A1: X c= Z & Y c= Z;
let x be object;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
X c= Y implies X \/ Z c= Y \/ Z
proof
assume
A1: X c= Y;
let x be object;
assume x in X \/ Z;
then x in X or x in Z by XBOOLE_0:def 3;
then x in Y or x in Z by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem
X c= Y implies X c= Z \/ Y
proof
Y c= Z \/ Y by Th7;
hence thesis;
end;
theorem
X \/ Y c= Z implies X c= Z
proof
X c= X \/ Y by Th7;
hence thesis;
end;
theorem Th12:
X c= Y implies X \/ Y = Y
proof
assume
A1: X c= Y;
thus X \/ Y c= Y
proof
let x be object;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis by A1;
end;
let x be object;
thus thesis by XBOOLE_0:def 3;
end;
theorem
X c= Y & Z c= V implies X \/ Z c= Y \/ V
proof
assume
A1: X c= Y;
assume
A2: Z c= V;
let x be object;
assume x in X \/ Z;
then x in X or x in Z by XBOOLE_0:def 3;
then x in Y or x in V by A1,A2;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = Y \/ Z
proof
assume that
A1: Y c= X & Z c= X and
A2: Y c= V & Z c= V implies X c= V;
Y c= Y \/ Z & Z c= Y \/ Z by Th7;
hence X c= Y \/ Z by A2;
thus thesis by A1,Th8;
end;
theorem
X \/ Y = {} implies X = {};
theorem Th16:
(X /\ Y) /\ Z = X /\ (Y /\ Z)
proof
thus (X /\ Y) /\ Z c= X /\ (Y /\ Z)
proof
let x be object;
assume
A1: x in (X /\ Y) /\ Z;
then
A2: x in Z by XBOOLE_0:def 4;
A3: x in X /\ Y by A1,XBOOLE_0:def 4;
then
A4: x in X by XBOOLE_0:def 4;
x in Y by A3,XBOOLE_0:def 4;
then x in Y /\ Z by A2,XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in X /\ (Y /\ Z);
then
A6: x in Y /\ Z by XBOOLE_0:def 4;
then
A7: x in Y by XBOOLE_0:def 4;
A8: x in Z by A6,XBOOLE_0:def 4;
x in X by A5,XBOOLE_0:def 4;
then x in X /\ Y by A7,XBOOLE_0:def 4;
hence thesis by A8,XBOOLE_0:def 4;
end;
theorem Th17:
X /\ Y c= X
by XBOOLE_0:def 4;
theorem
X c= Y /\ Z implies X c= Y
proof
Y /\ Z c= Y by Th17;
hence thesis;
end;
theorem Th19:
Z c= X & Z c= Y implies Z c= X /\ Y
proof
assume
A1: Z c= X & Z c= Y;
let x be object;
assume x in Z;
then x in X & x in Y by A1;
hence thesis by XBOOLE_0:def 4;
end;
theorem
(X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = Y /\ Z
proof
assume that
A1: X c= Y & X c= Z and
A2: V c= Y & V c= Z implies V c= X;
thus X c= Y /\ Z by A1,Th19;
Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X by A2;
hence thesis by Th17;
end;
theorem
X /\ (X \/ Y) = X
proof
thus X /\ (X \/ Y) c= X
by XBOOLE_0:def 4;
let x be object;
assume
A1: x in X;
then x in X \/ Y by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th22:
X \/ (X /\ Y) = X
proof
thus X \/ (X /\ Y) c= X
proof
let x be object;
assume x in X \/ (X /\ Y);
then x in X or x in X /\ Y by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 4;
end;
let x be object;
thus thesis by XBOOLE_0:def 3;
end;
theorem Th23:
X /\ (Y \/ Z) = X /\ Y \/ X /\ Z
proof
thus X /\ (Y \/ Z) c= X /\ Y \/ X /\ Z
proof
let x be object;
assume
A1: x in X /\ (Y \/ Z);
then x in Y \/ Z by XBOOLE_0:def 4;
then
A2: x in Y or x in Z by XBOOLE_0:def 3;
x in X by A1,XBOOLE_0:def 4;
then x in X /\ Y or x in X /\ Z by A2,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in X /\ Y \/ X /\ Z;
then x in X /\ Y or x in X /\ Z by XBOOLE_0:def 3;
then
A3: x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;
then x in Y \/ Z by XBOOLE_0:def 3;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem Th24:
X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z)
proof
thus X \/ Y /\ Z c= (X \/ Y) /\ (X \/ Z)
proof
let x be object;
assume x in X \/ Y /\ Z;
then x in X or x in Y /\ Z by XBOOLE_0:def 3;
then x in X or x in Y & x in Z by XBOOLE_0:def 4;
then x in X \/ Y & x in X \/ Z by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 4;
end;
let x be object;
assume
A1: x in (X \/ Y) /\ (X \/ Z);
then x in X \/ Z by XBOOLE_0:def 4;
then
A2: x in X or x in Z by XBOOLE_0:def 3;
x in X \/ Y by A1,XBOOLE_0:def 4;
then x in X or x in Y by XBOOLE_0:def 3;
then x in X or x in Y /\ Z by A2,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X)
proof
thus X /\ Y \/ Y /\ Z \/ Z /\ X = (X /\ Y \/ Y /\ Z \/ Z) /\ (X /\ Y \/ Y /\
Z \/ X) by Th24
.= (X /\ Y \/ (Y /\ Z \/ Z)) /\ (X /\ Y \/ Y /\ Z \/ X) by Th4
.= (X /\ Y \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by Th22
.= (X /\ Y \/ Z) /\ (X /\ Y \/ X \/ Y /\ Z) by Th4
.= (X /\ Y \/ Z) /\ (X \/ Y /\ Z) by Th22
.= (X \/ Z) /\ (Y \/ Z) /\ (X \/ Y /\ Z) by Th24
.= (X \/ Z) /\ (Y \/ Z) /\ ((X \/ Y) /\ (X \/ Z)) by Th24
.= (X \/ Y) /\ ((Y \/ Z) /\ (X \/ Z) /\ (X \/ Z)) by Th16
.= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th16
.= (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X) by Th16;
end;
theorem Th26:
X c= Y implies X /\ Z c= Y /\ Z
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in X /\ Z;
then x in X by XBOOLE_0:def 4;
then
A3: x in Y by A1;
x in Z by A2,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
X c= Y & Z c= V implies X /\ Z c= Y /\ V
proof
assume that
A1: X c= Y and
A2: Z c= V;
let x be object;
assume
A3: x in X /\ Z;
then x in Z by XBOOLE_0:def 4;
then
A4: x in V by A2;
x in X by A3,XBOOLE_0:def 4;
then x in Y by A1;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem Th28:
X c= Y implies X /\ Y = X
proof
assume
A1: X c= Y;
thus X /\ Y c= X by Th17;
let x be object;
assume
A2: x in X;
then x in Y by A1;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem
X /\ Y c= X \/ Z
proof
X /\ Y c= X & X c= X \/ Z by Th7,Th17;
hence thesis;
end;
theorem
X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z
proof
assume
A1: X c= Z;
thus X \/ Y /\ Z c= (X \/ Y) /\ Z
proof
let x be object;
assume x in X \/ Y /\ Z;
then
A2: x in X or x in Y /\ Z by XBOOLE_0:def 3;
then x in X or x in Y & x in Z by XBOOLE_0:def 4;
then
A3: x in (X \/ Y) by XBOOLE_0:def 3;
x in Z by A1,A2,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (X \/ Y) /\ Z;
then x in X \/ Y by XBOOLE_0:def 4;
then
A5: x in X or x in Y by XBOOLE_0:def 3;
x in Z by A4,XBOOLE_0:def 4;
then x in X & x in Z or x in Y /\ Z by A5,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(X /\ Y) \/ (X /\ Z) c= Y \/ Z
proof
now
let x be object;
assume x in (X /\ Y) \/ (X /\ Z);
then x in (X /\ Y) or x in (X /\ Z) by XBOOLE_0:def 3;
then x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;
hence x in Y \/ Z by XBOOLE_0:def 3;
end;
hence thesis;
end;
Lm1: X \ Y = {} iff X c= Y
proof
thus X \ Y = {} implies X c= Y
by XBOOLE_0:def 5;
assume
A1: X c= Y;
now
let x be object;
x in X & not x in Y iff contradiction by A1;
hence x in X \ Y iff x in {} by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem
X \ Y = Y \ X implies X = Y
proof
assume
A1: X \ Y = Y \ X;
now
let x be object;
x in X & not x in Y iff x in Y \ X by A1,XBOOLE_0:def 5;
hence x in X iff x in Y by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th33:
X c= Y implies X \ Z c= Y \ Z
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in X \ Z;
then x in X by XBOOLE_0:def 5;
then
A3: x in Y by A1;
not x in Z by A2,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem Th34:
X c= Y implies Z \ Y c= Z \ X
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in Z \ Y;
then not x in Y by XBOOLE_0:def 5;
then
A3: not x in X by A1;
x in Z by A2,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 5;
end;
Lm2: X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof
thus X \ (Y /\ Z) c= (X \ Y) \/ (X \ Z)
proof
let x be object;
assume
A1: x in X \ (Y /\ Z);
then not x in (Y /\ Z) by XBOOLE_0:def 5;
then
A2: not x in Y or not x in Z by XBOOLE_0:def 4;
x in X by A1,XBOOLE_0:def 5;
then x in (X \ Y) or x in (X \ Z) by A2,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
(X \ Y) c= X \ (Y /\ Z) & X \ Z c= X \ (Y /\ Z) by Th17,Th34;
hence thesis by Th8;
end;
theorem
X c= Y & Z c= V implies X \ V c= Y \ Z
proof
assume X c= Y & Z c= V;
then X \ V c= Y \ V & Y \ V c= Y \ Z by Th33,Th34;
hence thesis;
end;
theorem Th36:
X \ Y c= X
by XBOOLE_0:def 5;
theorem
X \ Y = {} iff X c= Y by Lm1;
theorem
X c= Y \ X implies X = {}
proof
assume
A1: X c= Y \ X;
thus X c= {}
proof
let x be object;
assume
A2: x in X;
then x in Y \ X by A1;
hence thesis by A2,XBOOLE_0:def 5;
end;
thus thesis;
end;
theorem Th39:
X \/ (Y \ X) = X \/ Y
proof
thus X \/ (Y \ X) c= X \/ Y
proof
let x be object;
assume x in X \/ (Y \ X);
then x in X or x in Y \ X by XBOOLE_0:def 3;
then x in X or x in Y by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in X \/ Y;
then x in X or x in Y & not x in X by XBOOLE_0:def 3;
then x in X or x in Y \ X by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(X \/ Y) \ Y = X \ Y
proof
thus for x being object holds x in (X \/ Y) \ Y implies x in X \ Y
proof let x be object;
assume
A1: x in (X \/ Y) \ Y;
then x in (X \/ Y) by XBOOLE_0:def 5;
then
A2: x in X or x in Y by XBOOLE_0:def 3;
not x in Y by A1,XBOOLE_0:def 5;
hence thesis by A2,XBOOLE_0:def 5;
end;
thus for x being object holds x in X \ Y implies x in (X \/ Y) \ Y
proof let x be object;
assume
A3: x in X \ Y;
then x in X or x in Y by XBOOLE_0:def 5;
then
A4: x in (X \/ Y) by XBOOLE_0:def 3;
not x in Y by A3,XBOOLE_0:def 5;
hence thesis by A4,XBOOLE_0:def 5;
end;
end;
theorem Th41:
(X \ Y) \ Z = X \ (Y \/ Z)
proof
thus for x being object holds x in (X \ Y) \ Z implies x in X \ (Y \/ Z)
proof let x be object;
assume
A1: x in (X \ Y) \ Z;
then
A2: not x in Z by XBOOLE_0:def 5;
A3: x in (X \ Y) by A1,XBOOLE_0:def 5;
then
A4: x in X by XBOOLE_0:def 5;
not x in Y by A3,XBOOLE_0:def 5;
then not x in (Y \/ Z) by A2,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 5;
end;
thus for x being object holds x in X \ (Y \/ Z) implies x in (X \ Y) \ Z
proof let x be object;
assume
A5: x in X \ (Y \/ Z);
then
A6: not x in (Y \/ Z) by XBOOLE_0:def 5;
then
A7: not x in Y by XBOOLE_0:def 3;
A8: not x in Z by A6,XBOOLE_0:def 3;
x in X by A5,XBOOLE_0:def 5;
then x in (X \ Y) by A7,XBOOLE_0:def 5;
hence thesis by A8,XBOOLE_0:def 5;
end;
end;
theorem Th42:
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proof
thus (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z)
proof
let x be object;
assume
A1: x in (X \/ Y) \ Z;
then x in (X \/ Y) by XBOOLE_0:def 5;
then x in X & not x in Z or x in Y & not x in Z by A1,XBOOLE_0:def 3,def 5;
then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (( X \ Z) \/ (Y \ Z));
then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 3;
then
A2: x in X & not x in Z or x in Y & not x in Z by XBOOLE_0:def 5;
then x in (X \/ Y) by XBOOLE_0:def 3;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem
X c= Y \/ Z implies X \ Y c= Z
proof
assume
A1: X c= Y \/ Z;
let x be object;
assume
A2: x in X \ Y;
then x in X by XBOOLE_0:def 5;
then
A3: x in Y \/ Z by A1;
not x in Y by A2,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 3;
end;
theorem
X \ Y c= Z implies X c= Y \/ Z
proof
assume
A1: for x being object holds x in X \ Y implies x in Z;
let x be object;
assume x in X;
then x in X \ Y or x in Y by XBOOLE_0:def 5;
then x in Z or x in Y by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem
X c= Y implies Y = X \/ (Y \ X)
proof
assume
A1: X c= Y;
now
let x be object;
x in Y iff x in X or x in (Y \ X) by A1,XBOOLE_0:def 5;
hence x in Y iff x in X \/ (Y \ X) by XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem
X \ (X \/ Y) = {} by Th7,Lm1;
theorem Th47:
X \ X /\ Y = X \ Y
proof
now
let x be object;
x in X & not x in X /\ Y iff x in X & not x in Y by XBOOLE_0:def 4;
hence x in X \ X /\ Y iff x in X \ Y by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem
X \ (X \ Y) = X /\ Y
proof
thus for x being object holds x in X \ (X \ Y) implies x in X /\ Y
proof let x be object;
assume
A1: x in X \ (X \ Y);
then not x in (X \ Y) by XBOOLE_0:def 5;
then
A2: not x in X or x in Y by XBOOLE_0:def 5;
x in X by A1,XBOOLE_0:def 5;
hence thesis by A2,XBOOLE_0:def 4;
end;
thus for x being object holds x in X /\ Y implies x in X \ (X \ Y)
proof let x be object;
assume
A3: x in X /\ Y;
then not x in X or x in Y by XBOOLE_0:def 4;
then
A4: not x in (X \ Y) by XBOOLE_0:def 5;
x in X by A3,XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 5;
end;
end;
theorem Th49:
X /\ (Y \ Z) = (X /\ Y) \ Z
proof
now
let x be object;
x in X & x in Y & not x in Z iff x in X & x in Y & not x in Z;
then x in X & x in (Y \ Z) iff x in (X /\ Y) & not x in Z by XBOOLE_0:def 4
,def 5;
hence x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z by XBOOLE_0:def 4,def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th50:
X /\ (Y \ Z) = X /\ Y \ X /\ Z
proof
A1: X /\ Y c= X by Th17;
X /\ Y \ X /\ Z = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Lm2
.= {} \/ ((X /\ Y) \ Z) by A1,Lm1
.= (X /\ Y) \ Z;
hence thesis by Th49;
end;
theorem Th51:
X /\ Y \/ (X \ Y) = X
proof
thus X /\ Y \/ (X \ Y) c= X
proof
let x be object;
assume x in X /\ Y \/ (X \ Y);
then x in X /\ Y or x in (X \ Y) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 4,def 5;
end;
let x be object;
assume x in X;
then x in X & x in Y or x in (X\Y) by XBOOLE_0:def 5;
then x in X /\ Y or x in (X \ Y) by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th52:
X \ (Y \ Z) = (X \ Y) \/ X /\ Z
proof
thus for x being object
holds x in X \ (Y \ Z) implies x in (X \ Y) \/ X /\ Z
proof let x be object;
assume
A1: x in X \ (Y \ Z);
then not x in (Y \ Z) by XBOOLE_0:def 5;
then x in X & not x in Y or x in X & x in Z by A1,XBOOLE_0:def 5;
then x in (X \ Y) or x in X /\ Z by XBOOLE_0:def 4,def 5;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (X \ Y) \/ X /\ Z;
then x in (X \ Y) or x in X /\ Z by XBOOLE_0:def 3;
then
A2: x in X & not x in Y or x in X & x in Z by XBOOLE_0:def 4,def 5;
then not x in (Y \ Z) by XBOOLE_0:def 5;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proof
X \(Y \/ Z) c= X \ Y & X \ (Y \/ Z) c= X \ Z by Th7,Th34;
hence X \ (Y \/ Z) c= (X \ Y) /\ (X \ Z) by Th19;
let x be object;
assume
A1: x in (X \ Y) /\ (X \ Z);
then
A2: x in (X \ Y) by XBOOLE_0:def 4;
then
A3: x in X by XBOOLE_0:def 5;
x in (X \ Z) by A1,XBOOLE_0:def 4;
then
A4: not x in Z by XBOOLE_0:def 5;
not x in Y by A2,XBOOLE_0:def 5;
then not x in (Y \/ Z) by A4,XBOOLE_0:def 3;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem
X \ (Y /\ Z) = (X \ Y) \/ (X \ Z) by Lm2;
theorem Th55:
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proof
for x being object holds
x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X)
proof let x be object;
thus x in (X \/ Y) \ (X /\ Y) implies x in (X \ Y) \/ (Y \ X)
proof
assume
A1: x in (X \/ Y) \ (X /\ Y);
then not x in (X /\ Y) by XBOOLE_0:def 5;
then
A2: not x in X or not x in Y by XBOOLE_0:def 4;
x in (X \/ Y) by A1,XBOOLE_0:def 5;
then x in X or x in Y by XBOOLE_0:def 3;
then x in (X \ Y) or x in( Y \ X) by A2,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
assume x in (X \ Y) \/ (Y \ X);
then x in (X \ Y) or x in (Y \ X) by XBOOLE_0:def 3;
then x in X & not x in Y or x in Y & not x in X by XBOOLE_0:def 5;
then ( not x in (X /\ Y))& x in (X \/ Y) by XBOOLE_0:def 3,def 4;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
Lm3: X c= Y & Y c< Z implies X c< Z
proof
assume that
A1: X c= Y and
A2: Y c< Z;
Y c= Z by A2;
hence X c= Z & X <> Z by A1,A2,XBOOLE_0:def 10;
end;
theorem
X c< Y & Y c< Z implies X c< Z
by Lm3;
theorem
not (X c< Y & Y c< X);
theorem
X c< Y & Y c= Z implies X c< Z
proof
assume that
A1: X c< Y and
A2: Y c= Z;
X c= Y by A1;
hence X c= Z & X <> Z by A1,A2,XBOOLE_0:def 10;
end;
theorem
X c= Y & Y c< Z implies X c< Z by Lm3;
theorem Th60:
X c= Y implies not Y c< X
proof
assume X c= Y & Y c= X & X <> Y;
hence contradiction;
end;
theorem
X <> {} implies {} c< X
proof
assume
A1: X <> {};
thus {} c= X;
thus thesis by A1;
end;
theorem
not X c< {} by Th3;
::$N Modus Celarent
::$N Modus Darii
theorem Th63:
X c= Y & Y misses Z implies X misses Z
by Th3,Th26;
theorem
A c= X & B c= Y & X misses Y implies A misses B
proof
assume that
A1: A c= X and
A2: B c= Y and
A3: X misses Y;
A misses Y by A1,A3,Th63;
hence thesis by A2,Th63;
end;
theorem
X misses {};
theorem
X meets X iff X <> {};
theorem
X c= Y & X c= Z & Y misses Z implies X = {}
by Th3,Th19;
::$N Modus Darapti
theorem Th68:
for A being non empty set st A c= Y & A c= Z holds Y meets Z
proof
let A be non empty set;
consider x being object such that
A1: x in A by XBOOLE_0:def 1;
assume A c= Y & A c= Z;
then x in Y & x in Z by A1;
hence thesis by XBOOLE_0:3;
end;
theorem
for A being non empty set st A c= Y holds A meets Y by Th68;
theorem Th70:
X meets Y \/ Z iff X meets Y or X meets Z
proof
thus X meets Y \/ Z implies X meets Y or X meets Z
proof
assume X meets Y \/ Z;
then consider x being object such that
A1: x in X & x in Y \/ Z by XBOOLE_0:3;
x in X & x in Y or x in X & x in Z by A1,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:3;
end;
A2: X meets Z implies X meets Y \/ Z
proof
assume X meets Z;
then consider x being object such that
A3: x in X and
A4: x in Z by XBOOLE_0:3;
x in Y \/ Z by A4,XBOOLE_0:def 3;
hence thesis by A3,XBOOLE_0:3;
end;
X meets Y implies X meets Y \/ Z
proof
assume X meets Y;
then consider x being object such that
A5: x in X and
A6: x in Y by XBOOLE_0:3;
x in Y \/ Z by A6,XBOOLE_0:def 3;
hence thesis by A5,XBOOLE_0:3;
end;
hence thesis by A2;
end;
theorem
X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z
proof
assume that
A1: X \/ Y = Z \/ Y and
A2: X /\ Y = {} and
A3: Z /\ Y = {};
thus X c= Z
proof
let x be object such that
A4: x in X;
X c= Z \/ Y by A1,Th7;
then
A5: x in Z \/ Y by A4;
not x in Y by A2,A4,XBOOLE_0:def 4;
hence thesis by A5,XBOOLE_0:def 3;
end;
let x be object such that
A6: x in Z;
Z c= X \/ Y by A1,Th7;
then
A7: x in X \/ Y by A6;
not x in Y by A3,A6,XBOOLE_0:def 4;
hence thesis by A7,XBOOLE_0:def 3;
end;
theorem
X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9
proof
assume
A1: X9 \/ Y9 = X \/ Y;
assume X misses X9 & Y misses Y9;
then
A2: X /\ X9 = {} & Y /\ Y9 = {};
thus X = X /\ (X9 \/ Y9) by A1,Th7,Th28
.= X /\ X9 \/ X /\ Y9 by Th23
.= (X \/ Y) /\ Y9 by A2,Th23
.= Y9 by A1,Th7,Th28;
end;
theorem
X c= Y \/ Z & X misses Z implies X c= Y
proof
assume that
A1: X c= Y \/ Z and
A2: X /\ Z = {};
X /\ (Y \/ Z)= X by A1,Th28;
then Y /\ X \/ {} = X by A2,Th23;
hence thesis by Th17;
end;
theorem Th74:
X meets Y /\ Z implies X meets Y
proof
assume X meets Y /\ Z;
then consider x being object such that
A1: x in X and
A2: x in Y /\ Z by XBOOLE_0:3;
x in Y by A2,XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:3;
end;
theorem
X meets Y implies X /\ Y meets Y
proof
assume X meets Y;
then consider x being object such that
A1: x in X and
A2: x in Y by XBOOLE_0:3;
x in X /\ Y by A1,A2,XBOOLE_0:def 4;
hence thesis by A2,XBOOLE_0:3;
end;
theorem
Y misses Z implies X /\ Y misses X /\ Z
proof
assume Y misses Z;
then (X /\ Z) misses Y by Th74;
hence thesis by Th74;
end;
theorem
X meets Y & X c= Z implies X meets Y /\ Z
proof
assume that
A1: X meets Y and
A2: X c= Z;
now
assume
A3: X /\ (Y /\ Z) = {};
X /\ Y = (X /\ Z) /\ Y by A2,Th28
.= {} by A3,Th16;
hence contradiction by A1;
end;
hence thesis;
end;
theorem
X misses Y implies X /\ (Y \/ Z) = X /\ Z
proof
assume X misses Y;
then X /\ Y = {};
hence X /\ (Y \/ Z) = {} \/ X /\ Z by Th23
.= X /\ Z;
end;
theorem Th79:
X \ Y misses Y
proof
not ex x being object st x in (X \ Y) /\ Y
proof
given x being object such that
A1: x in (X \ Y) /\ Y;
x in X \ Y & x in Y by A1,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5;
end;
hence (X \ Y) /\ Y = {} by XBOOLE_0:def 1;
end;
theorem
X misses Y implies X misses Y \ Z
proof
assume
A1: X misses Y;
assume X meets Y \ Z;
then consider x being object such that
A2: x in X and
A3: x in Y \ Z by XBOOLE_0:3;
x in Y by A3,XBOOLE_0:def 5;
hence thesis by A1,A2,XBOOLE_0:3;
end;
theorem
X misses Y \ Z implies Y misses X \ Z
proof
X /\ (Y \ Z) = Y /\ X \ Z by Th49
.= Y /\ (X \ Z) by Th49;
hence thesis;
end;
theorem
X \ Y misses Y \ X
proof
assume X \ Y meets Y \ X;
then consider x being object such that
A1: x in X \ Y and
A2: x in Y \ X by XBOOLE_0:3;
x in X by A1,XBOOLE_0:def 5;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem Th83:
X misses Y iff X \ Y = X
proof
thus X misses Y implies X \ Y = X
proof
assume
A1: X /\ Y = {};
thus for x being object holds x in X \ Y implies x in X by XBOOLE_0:def 5;
let x be object;
not x in X /\ Y implies not x in X or not x in Y by XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:def 5;
end;
assume
A2: X \ Y = X;
not ex x being object st x in X /\ Y
proof
given x being object such that
A3: x in X /\ Y;
x in X & x in Y by A3,XBOOLE_0:def 4;
hence contradiction by A2,XBOOLE_0:def 5;
end;
hence thesis by XBOOLE_0:4;
end;
theorem
X meets Y & X misses Z implies X meets Y \ Z
proof
assume that
A1: X meets Y and
A2: X misses Z;
X /\ (Y \ Z) = X /\ Y \ X /\ Z by Th50
.= X /\ Y \ {} by A2;
hence X /\ (Y \ Z) <> {} by A1;
end;
theorem
X c= Y implies X misses Z \ Y
proof
assume
A1: X c= Y;
thus X /\ (Z \ Y) = Z /\ X \ Y by Th49
.= Z /\ (X \ Y) by Th49
.= Z /\ {} by A1,Lm1
.= {};
end;
theorem Th86:
X c= Y & X misses Z implies X c= Y \ Z
proof
assume
A1: X c= Y & X /\ Z = {};
let x be object;
assume x in X;
then x in Y & not x in Z by A1,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
theorem
Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y
proof
assume
A1: Y misses Z;
thus (X \/ Z) \ Y = (X \ Y) \/ (Z \ Y) by Th42
.= (X \ Y) \/ Z by A1,Th83;
end;
theorem Th88:
X misses Y implies (X \/ Y) \ Y = X
proof
assume
A1: X misses Y;
thus (X \/ Y) \ Y = (X \ Y) \/ (Y \ Y) by Th42
.= (X \ Y) \/ {} by Lm1
.= X by A1,Th83;
end;
theorem Th89:
X /\ Y misses X \ Y
proof
now
let x be object;
not (x in X & x in Y & not x in Y);
hence not (x in X /\ Y & x in X \ Y) by XBOOLE_0:def 4,def 5;
end;
hence thesis by XBOOLE_0:3;
end;
theorem
X \ (X /\ Y) misses Y
proof
X \ (X /\ Y) = X \ Y by Th47;
hence thesis by Th79;
end;
theorem
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
set S1 = X \ (Y \/ Z), S2 = Y \ (X \/ Z), S3 = Z \ (X \/ Y), S4 = X /\ Y /\
Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/
(Y \ X))) by Th42
.= (S1 \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= (S1 \/ S2) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= (S1 \/ S2) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th55
.= (S1 \/ S2) \/ (S4 \/ S3) by Th52
.= (S1 \/ S2 \/ S4) \/ S3 by Th4
.= (S1 \/ S4 \/ S2) \/ S3 by Th4
.= (S1 \/ S4) \/ (S2 \/ S3) by Th4
.= (S1 \/ X /\ (Y /\ Z)) \/ (S2 \/ S3) by Th16
.= X \ ((Y \/ Z) \ (Y /\ Z)) \/ (S2 \/ S3) by Th52
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ (S2 \/ (Z \ (Y \/ X))) by Th55
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ (Z \/ X)) \/ (Z \ Y \ X)) by Th41
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ Z \ X) \/ (Z \ Y \ X)) by Th41
.= X \+\ (Y \+\ Z) by Th42;
end;
theorem
X \+\ X = {} by Lm1;
theorem Th93:
X \/ Y = (X \+\ Y) \/ X /\ Y
proof
thus X \/ Y = ((X \ Y) \/ X /\ Y) \/ Y by Th51
.= (X \ Y) \/ (X /\ Y \/ Y) by Th4
.= (X \ Y) \/ Y by Th22
.= (X \ Y) \/ ((Y \ X) \/ (Y /\ X)) by Th51
.= (X \+\ Y) \/ X /\ Y by Th4;
end;
Lm4: X /\ Y misses X \+\ Y
proof
X /\ Y misses X \ Y & X /\ Y misses Y \ X by Th89;
hence thesis by Th70;
end;
Lm5: X \+\ Y = (X \/ Y) \ X /\ Y
proof
thus X \+\ Y = (X \ X /\ Y) \/ (Y \ X) by Th47
.= (X \ X /\ Y) \/ (Y \ X /\ Y) by Th47
.= (X \/ Y) \ X /\ Y by Th42;
end;
theorem
X \/ Y = X \+\ Y \+\ X /\ Y
proof
X /\ Y misses X \+\ Y by Lm4;
then (X \+\ Y) \ X /\ Y = X \+\ Y & X /\ Y \ (X \+\ Y) = X /\ Y by Th83;
hence thesis by Th93;
end;
theorem
X /\ Y = X \+\ Y \+\ (X \/ Y)
proof
X \+\ Y = (X \/ Y) \ X /\ Y by Lm5;
then X \+\ Y c= X \/ Y by Th36;
then
A1: (X \+\ Y) \ (X \/ Y) = {} by Lm1;
X \/ Y = (X \+\ Y) \/ X /\ Y by Th93;
hence thesis by A1,Lm4,Th88;
end;
theorem
X \ Y c= X \+\ Y by Th7;
theorem
X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z by Th8;
theorem
X \/ Y = X \+\ (Y \ X)
proof
A1: Y \ X \ X = Y \ (X \/ X) by Th41
.= Y \ X;
X \ (Y \ X) = (X \ Y) \/ X /\ X by Th52
.= X by Th12,Th36;
hence thesis by A1,Th39;
end;
theorem
(X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proof
thus (X \+\ Y) \ Z = (X \ Y \ Z) \/ (Y \ X \ Z) by Th42
.= (X \ (Y \/ Z)) \/ (Y \ X \ Z) by Th41
.= (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)) by Th41;
end;
theorem
X \ Y = X \+\ (X /\ Y)
proof
X /\ Y c= X by Th17;
then X /\ Y \ X = {} by Lm1;
hence thesis by Th47;
end;
theorem
X \+\ Y = (X \/ Y) \ X /\ Y by Lm5;
theorem
X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z
proof
thus X \ (Y \+\ Z) = X \ ((Y \/ Z) \ Y /\ Z) by Lm5
.= X \ (Y \/ Z) \/ X /\ (Y /\ Z) by Th52
.= X \ (Y \/ Z) \/ X /\ Y /\ Z by Th16;
end;
theorem
X /\ Y misses X \+\ Y by Lm4;
theorem
X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable;
begin :: Addenda
theorem
for X, Y being set st X c< Y holds Y \ X <> {} by Th60,Lm1;
theorem Th106:
X c= A \ B implies X c= A & X misses B
proof
assume
A1: X c= A \ B;
A \ B c= A by Th36;
hence X c= A by A1;
now
let x be object;
assume x in X;
then x in A \ B by A1;
hence not x in B by XBOOLE_0:def 5;
end;
hence thesis by XBOOLE_0:3;
end;
theorem
X c= A \+\ B iff X c= A \/ B & X misses A /\ B
proof
A \+\ B = (A \/ B) \ A /\ B by Lm5;
hence thesis by Th86,Th106;
end;
theorem
X c= A implies X /\ Y c= A
proof
X /\ Y c= X by Th17;
hence thesis;
end;
theorem Th109:
X c= A implies X \ Y c= A
proof
X \ Y c= X by Th36;
hence thesis;
end;
theorem
X c= A & Y c= A implies X \+\ Y c= A
proof
assume X c= A & Y c= A;
then X \ Y c= A & Y \ X c= A by Th109;
hence thesis by Th8;
end;
theorem Th111:
(X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
proof
thus (X /\ Z) \ (Y /\ Z) = ((X /\ Z) \ Y) \/ ((X /\ Z) \ Z) by Lm2
.= ((X /\ Z) \ Y) \/ (X /\ (Z \ Z)) by Th49
.= ((X /\ Z) \ Y) \/ (X /\ {}) by Lm1
.= (X \ Y) /\ Z by Th49;
end;
theorem
(X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
proof
thus (X /\ Z) \+\ (Y /\ Z) = ((X \ Y) /\ Z) \/ ((Y /\ Z) \ (X /\ Z)) by Th111
.= ((X \ Y) /\ Z) \/ ((Y \ X) /\ Z) by Th111
.= (X \+\ Y) /\ Z by Th23;
end;
theorem
X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V)
proof
X \/ Y \/ Z \/ V = X \/ Y \/ (Z \/ V) by Th4
.= X \/ (Y \/ (Z \/ V)) by Th4
.= X \/ (Y \/ Z \/ V) by Th4;
hence thesis;
end;
theorem
for A,B,C,D being set st A misses D & B misses D & C misses D holds A
\/ B \/ C misses D
proof
let A,B,C,D be set;
assume A misses D & B misses D;
then
A1: A \/ B misses D by Th70;
assume C misses D;
hence thesis by A1,Th70;
end;
::$CT
theorem
X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
proof
thus X /\ (Y /\ Z) = X /\ X /\ Y /\ Z by Th16
.= X /\ (X /\ Y) /\ Z by Th16
.= (X /\ Y) /\ (X /\ Z) by Th16;
end;
theorem
for P,G,C being set st C c= G holds P \ C = (P \ G) \/ (P /\ (G \ C))
proof
let P,G,C be set;
assume C c= G;
then
A1: P \ G c= P \ C by Th34;
thus P \ C c= (P \ G) \/ (P /\ (G \ C))
proof
let x be object;
assume x in P \ C;
then x in P & not x in G or x in P & x in G & not x in C by XBOOLE_0:def 5;
then x in P \ G or x in P & x in G \ C by XBOOLE_0:def 5;
then x in P \ G or x in P /\ (G \ C) by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
P /\ (G \ C) = (P /\ G) \ C & (P /\ G) \ C c= P \ C by Th17,Th33,Th49;
hence thesis by A1,Th8;
end;