:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990-2017 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 XBOOLE_0, TARSKI, ZFMISC_1;
notations TARSKI, XBOOLE_0, ENUMSET1;
constructors TARSKI, XBOOLE_0, ENUMSET1;
registrations XBOOLE_0;
requirements BOOLE;
definitions TARSKI, XBOOLE_0;
equalities TARSKI, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, ENUMSET1, XBOOLE_1, XTUPLE_0, XREGULAR, TARSKI_A;
schemes XBOOLE_0, XFAMILY;
begin
reserve u,v,x,x1,x2,y,y1,y2,z,p,a for object,
A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;
Lm1: {x} c= X iff x in X
proof
x in {x} by TARSKI:def 1;
hence {x} c= X implies x in X;
assume
A1: x in X;
let y;
thus thesis by A1,TARSKI:def 1;
end;
Lm2: Y c= X & not x in Y implies Y c= X \ { x }
proof
assume
A1: Y c= X & not x in Y;
let y;
assume y in Y;
then y in X & not y in { x } by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
Lm3:
Y c= { x } iff Y = {} or Y = { x }
proof
thus Y c= { x } implies Y = {} or Y = { x }
proof
assume
A1: Y c= { x };
x in Y or not x in Y;
then { x } c= Y or Y c= { x } \ { x } by A1,Lm1,Lm2;
then { x } = Y or Y c= {} by A1,XBOOLE_1:37;
hence thesis by XBOOLE_1:3;
end;
thus thesis;
end;
definition
let X;
defpred IT[set] means $1 c= X;
func bool X -> set means
:Def1:
Z in it iff Z c= X;
existence
proof
consider M such that
A1: X in M & for X,Y holds X in M & Y c= X implies Y in M and
for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
for X holds X c= M implies X,M are_equipotent or X in M by TARSKI_A:1;
consider IT being set such that
A2: Y in IT iff Y in M & IT[Y] from XFAMILY:sch 1;
take IT;
thus thesis by A2,A1;
end;
uniqueness
proof
thus for X1,X2 being set st (for x being set holds x in X1 iff IT[x]) & (
for x being set holds x in X2 iff IT[x]) holds X1 = X2 from XFAMILY:sch 3;
end;
end;
definition
let X1,X2;
defpred X[object] means
ex x,y st x in X1 & y in X2 & $1 = [x,y];
func [: X1,X2 :] -> set means
:Def2:
z in it iff ex x,y st x in X1 & y in X2 & z = [x,y];
existence
proof
A1: X1 c= X1 \/ X2 by XBOOLE_1:7;
consider X such that
A2: for z holds z in X iff z in bool(bool(X1 \/ X2)) & X[z] from
XBOOLE_0:sch 1;
take X;
let z;
thus z in X implies
ex x,y st x in X1 & y in X2 & z = [x,y] by A2;
given x,y such that
A3: x in X1 and
A4: y in X2 and
A5: z = [x,y];
{x,y} c= X1 \/ X2
proof
let z;
assume z in {x,y};
then z = x or z = y by TARSKI:def 2;
hence thesis by A3,A4,XBOOLE_0:def 3;
end;
then
A6: {x,y} in bool(X1 \/ X2) by Def1;
{x} c= X1 \/ X2 by A1,A3,Lm1;
then
A7: {x} in bool(X1 \/ X2) by Def1;
{{x,y},{x}} c= bool(X1 \/ X2)
by A7,A6,TARSKI:def 2;
then {{x,y},{x}} in bool(bool(X1 \/ X2)) by Def1;
hence thesis by A2,A3,A4,A5;
end;
uniqueness
proof
thus for X1,X2 being set
st (for x holds x in X1 iff X[x]) & (for x holds x in X2 iff X[x])
holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
definition
let X1,X2,X3;
func [: X1,X2,X3 :] -> set equals
[:[:X1,X2:],X3:];
coherence;
end;
definition
let X1,X2,X3,X4;
func [: X1,X2,X3,X4 :] -> set equals
[:[:X1,X2,X3:],X4:];
coherence;
end;
begin
::
:: Empty set.
::
theorem
bool {} = { {} }
proof
now
let x;
reconsider xx = x as set by TARSKI:1;
xx c= {} iff x = {} by XBOOLE_1:3;
hence x in bool {} iff x in { {} } by Def1,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem
union {} = {}
proof
now
given x such that
A1: x in union {};
ex X being set st x in X & X in {} by A1,TARSKI:def 4;
hence contradiction;
end;
hence thesis by XBOOLE_0:7;
end;
::
:: Singleton and unordered pairs.
::
theorem Th3:
{x} c= {y} implies x = y
proof
x in { x } by TARSKI:def 1;
then {x} = {y} implies x = y by TARSKI:def 1;
hence thesis by Lm3;
end;
theorem Th4:
{x} = {y1,y2} implies x = y1
proof
assume { x } = { y1,y2 };
then y1 in { x } by TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
theorem
{x} = {y1,y2} implies y1 = y2
proof
assume
A1: { x } = { y1,y2 };
then x = y1 by Th4;
hence thesis by A1,Th4;
end;
theorem Th6:
{ x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2
proof
x1 in { x1,x2 } by TARSKI:def 2;
hence thesis by TARSKI:def 2;
end;
theorem Th7:
{x} c= {x,y}
proof
let z;
assume z in {x};
then z=x by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
Lm4: {x} \/ X c= X implies x in X
proof
assume
A1: {x} \/ X c= X;
assume not x in X;
then not x in {x} \/ X by A1;
then not x in {x} by XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
theorem
{x} \/ {y} = {x} implies x = y
proof
assume {x} \/ {y} = {x};
then y in {x} or x in {y} by Lm4;
hence thesis by TARSKI:def 1;
end;
theorem
{x} \/ {x,y} = {x,y}
proof
x in {x,y} by TARSKI:def 2;
hence thesis by Lm1,XBOOLE_1:12;
end;
Lm5: {x} misses X implies not x in X
proof
A1: x in {x} by TARSKI:def 1;
assume {x} /\ X = {} & x in X;
hence contradiction by A1,XBOOLE_0:def 4;
end;
theorem
{x} misses {y} implies x <> y;
Lm6: not x in X implies {x} misses X
proof
assume
A1: not x in X;
thus {x} /\ X c= {}
proof
let y;
assume y in {x} /\ X;
then y in {x} & y in X by XBOOLE_0:def 4;
hence thesis by A1,TARSKI:def 1;
end;
thus thesis;
end;
theorem Th11:
x <> y implies {x} misses {y}
proof
assume x <> y;
then not x in {y} by TARSKI:def 1;
hence thesis by Lm6;
end;
Lm7: X /\ {x} = {x} implies x in X
proof
assume X /\ {x} = {x};
then x in X /\ {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 4;
end;
theorem
{x} /\ {y} = {x} implies x = y
proof
assume {x} /\ {y} = {x};
then x in {y} or y in {x} by Lm7;
hence thesis by TARSKI:def 1;
end;
Lm8: x in X implies X /\ {x} = {x} by Lm1,XBOOLE_1:28;
theorem
{x} /\ {x,y} = {x}
proof
x in {x,y} by TARSKI:def 2;
hence thesis by Lm1,XBOOLE_1:28;
end;
Lm9: {x} \ X = {x} iff not x in X by Lm5,Lm6,XBOOLE_1:83;
theorem
{x} \ {y} = {x} iff x <> y
proof
{x} \ {y} = {x} iff not x in {y} by Lm5,Lm6,XBOOLE_1:83;
hence thesis by TARSKI:def 1;
end;
Lm10: {x} \ X = {} iff x in X by Lm1,XBOOLE_1:37;
theorem
{x} \ {y} = {} implies x = y
proof
assume {x} \ {y} = {};
then x in {y} by Lm1,XBOOLE_1:37;
hence thesis by TARSKI:def 1;
end;
theorem
{x} \ {x,y} = {}
proof
x in {x,y} by TARSKI:def 2;
hence thesis by Lm1,XBOOLE_1:37;
end;
Lm11: {x,y} \ X = {x} iff not x in X & (y in X or x = y)
proof
thus {x,y} \ X = {x} implies not x in X & (y in X or x = y)
proof
assume
A1: {x,y} \ X = {x};
then x in {x,y} \ X by TARSKI:def 1;
hence not x in X by XBOOLE_0:def 5;
A2: y in {x,y} by TARSKI:def 2;
assume not y in X;
then y in {x} by A1,A2,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
assume
A3: ( not x in X)&( y in X or x=y);
for z holds z in {x,y} \ X iff z=x
proof
let z;
z in {x,y} \ X iff z in {x,y} & not z in X by XBOOLE_0:def 5;
hence thesis by A3,TARSKI:def 2;
end;
hence thesis by TARSKI:def 1;
end;
theorem
x <> y implies { x,y } \ { y } = { x }
proof
assume x <> y;
then
A1: not x in {y} by TARSKI:def 1;
y in {y} by TARSKI:def 1;
hence thesis by A1,Lm11;
end;
theorem
{x} c= {y} implies x = y by Th3;
theorem
{z} c= {x,y} implies z = x or z = y
proof
A1: z in {z} by TARSKI:def 1;
assume {z} c= {x,y};
then z in {x,y} by A1;
hence thesis by TARSKI:def 2;
end;
theorem Th20:
{x,y} c= {z} implies x = z
proof
A1: x in {x,y} by TARSKI:def 2;
assume {x,y} c= {z};
then x in {z} by A1;
hence thesis by TARSKI:def 1;
end;
theorem
{x,y} c= {z} implies {x,y} = {z}
proof
assume {x,y} c= {z};
then x=z & y=z by Th20;
hence thesis by ENUMSET1:29;
end;
Lm12: X <> {x} & X <> {} implies ex y st y in X & y <> x
proof
assume that
A1: X <> {x} and
A2: X <> {};
per cases;
suppose
A3: not x in X;
consider y such that
A4: y in X by A2,XBOOLE_0:7;
take y;
thus thesis by A3,A4;
end;
suppose
A5: x in X;
consider y such that
A6: y in X & not y in {x} or y in {x} & not y in X by A1,TARSKI:2;
take y;
thus thesis by A5,A6,TARSKI:def 1;
end;
end;
Lm13: Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2}
proof
thus Z c= {x1,x2} implies Z={} or Z={x1} or Z={x2} or Z={x1,x2}
proof
assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2};
now
let z;
thus z in Z implies z in {x1,x2} by A1;
A5: now
assume
A6: not x1 in Z;
consider y such that
A7: y in Z and
A8: y<>x2 by A2,A4,Lm12;
y in {x1,x2} by A1,A7;
hence contradiction by A6,A7,A8,TARSKI:def 2;
end;
A9: now
assume
A10: not x2 in Z;
consider y such that
A11: y in Z and
A12: y<>x1 by A2,A3,Lm12;
y in {x1,x2} by A1,A11;
hence contradiction by A10,A11,A12,TARSKI:def 2;
end;
assume z in {x1,x2};
hence z in Z by A5,A9,TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
thus thesis by Th7;
end;
theorem
{x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2
proof
assume {x1,x2} c= {y1,y2};
then {x1,x2}={} or {x1,x2}={y1} or {x1,x2}={y2} or {x1,x2}={y1,y2} by Lm13;
hence thesis by Th4,Th6;
end;
theorem
x <> y implies { x } \+\ { y } = { x,y }
proof
assume
A1: x <> y;
for z holds z in { x } \+\ { y } iff z=x or z=y
proof
let z;
A2: z in {y} iff z=y by TARSKI:def 1;
z in {x} iff z=x by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:1;
end;
hence thesis by TARSKI:def 2;
end;
theorem
bool { x } = { {} , { x }}
proof
now
let y;
reconsider yy = y as set by TARSKI:1;
yy c= { x } iff y = {} or y = { x } by Lm3;
hence y in bool { x } iff y in { {}, { x }} by Def1,TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
Lm14: X in A implies X c= union A
by TARSKI:def 4;
registration let x be object;
reduce union { x } to x;
reducibility
proof
reconsider X = x as set by TARSKI:1;
A1: union { X } c= X
proof
let y;
assume y in union { X };
then ex Y being set st y in Y & Y in { X } by TARSKI:def 4;
hence thesis by TARSKI:def 1;
end;
X in { X } by TARSKI:def 1;
then X c= union { X } by Lm14;
hence thesis by A1,XBOOLE_0:def 10;
end;
end;
theorem
union { x } = x;
Lm15: union { X,Y } = X \/ Y
proof
x in union {X,Y} iff x in X or x in Y
proof
thus x in union {X,Y} implies x in X or x in Y
proof
assume x in union {X,Y};
then ex Z st x in Z & Z in {X,Y} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
X in {X,Y} & Y in {X,Y} by TARSKI:def 2;
hence thesis by TARSKI:def 4;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem
union {{x},{y}} = {x,y}
proof
thus union {{x},{y}} = {x} \/ {y} by Lm15
.= {x,y} by ENUMSET1:1;
end;
::
:: Ordered pairs.
::
Lm16: [x,y] in [:X,Y:] iff x in X & y in Y
proof
thus [x,y] in [:X,Y:] implies x in X & y in Y
proof
assume [x,y] in [:X,Y:];
then ex x1,y1 st x1 in X & y1 in Y & [x,y]=[x1,y1] by Def2;
hence thesis by XTUPLE_0:1;
end;
thus thesis by Def2;
end;
::$CT
theorem
[x,y] in [:{x1},{y1}:] iff x = x1 & y = y1
proof
x=x1 & y=y1 iff x in {x1} & y in {y1} by TARSKI:def 1;
hence thesis by Lm16;
end;
theorem Th28:
[:{x},{y}:] = {[x,y]}
proof
now
let z;
thus z in [:{x},{y}:] implies z in {[x,y]}
proof
assume z in [:{x},{y}:];
then consider x1,y1 such that
A1: x1 in {x} & y1 in {y} and
A2: z=[x1,y1] by Def2;
x1=x & y1=y by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
assume z in {[x,y]};
then
A3: z=[x,y] by TARSKI:def 1;
x in {x} & y in {y} by TARSKI:def 1;
hence z in [:{x},{y}:] by A3,Lm16;
end;
hence thesis by TARSKI:2;
end;
theorem Th29:
[:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]}
proof
now
let v;
A1: z in{y,z} by TARSKI:def 2;
thus v in [:{x},{y,z}:] implies v in {[x,y],[x,z]}
proof
assume v in [:{x},{y,z}:];
then consider x1,y1 such that
A2: x1 in {x} and
A3: y1 in {y,z} and
A4: v=[x1,y1] by Def2;
A5: y1=y or y1=z by A3,TARSKI:def 2;
x1=x by A2,TARSKI:def 1;
hence thesis by A4,A5,TARSKI:def 2;
end;
assume v in {[x,y],[x,z]};
then
A6: v=[x,y] or v=[x,z] by TARSKI:def 2;
x in{x} & y in{y,z} by TARSKI:def 1,def 2;
hence v in [:{x},{y,z}:] by A6,A1,Lm16;
end;
hence [:{x},{y,z}:] = {[x,y],[x,z]} by TARSKI:2;
now
let v;
A7: z in{z} by TARSKI:def 1;
thus v in [:{x,y},{z}:] implies v in {[x,z],[y,z]}
proof
assume v in [:{x,y},{z}:];
then consider x1,y1 such that
A8: x1 in {x,y} and
A9: y1 in {z} and
A10: v=[x1,y1] by Def2;
A11: x1=x or x1=y by A8,TARSKI:def 2;
y1=z by A9,TARSKI:def 1;
hence thesis by A10,A11,TARSKI:def 2;
end;
assume v in {[x,z],[y,z]};
then
A12: v=[x,z] or v=[y,z] by TARSKI:def 2;
x in{x,y} & y in{x,y} by TARSKI:def 2;
hence v in [:{x,y},{z}:] by A12,A7,Lm16;
end;
hence thesis by TARSKI:2;
end;
::
:: Singleton and unordered pairs included in a set.
::
theorem
{x} c= X iff x in X by Lm1;
theorem Th31:
{x1,x2} c= Z iff x1 in Z & x2 in Z
proof
x1 in {x1,x2} & x2 in {x1,x2} by TARSKI:def 2;
hence {x1,x2} c= Z implies x1 in Z & x2 in Z;
assume
A1: x1 in Z & x2 in Z;
let z;
assume z in {x1,x2};
hence thesis by A1,TARSKI:def 2;
end;
::
:: Set included in a singleton (or unordered pair).
::
theorem
Y c= { x } iff Y = {} or Y = { x } by Lm3;
theorem
Y c= X & not x in Y implies Y c= X \ { x } by Lm2;
theorem
X <> {x} & X <> {} implies ex y st y in X & y <> x by Lm12;
theorem
Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} by Lm13;
::
:: Sum of an unordered pair (or a singleton) and a set.
::
theorem Th36:
{z} = X \/ Y implies X = {z} & Y = {z} or X = {} & Y = {z} or X
= {z} & Y = {}
proof
assume
A1: {z} = X \/ Y;
X <> {} or Y <> {} by A1;
hence thesis by A1,Lm3,XBOOLE_1:7;
end;
theorem
{z} = X \/ Y & X <> Y implies X = {} or Y = {}
proof
assume {z} = X \/ Y;
then X={z} & Y={z} or X={} & Y={z} or X={z} & Y={} by Th36;
hence thesis;
end;
theorem
{x} \/ X c= X implies x in X by Lm4;
theorem
x in X implies {x} \/ X = X by Lm1,XBOOLE_1:12;
theorem
{x,y} \/ Z c= Z implies x in Z
proof
assume
A1: {x,y} \/ Z c= Z;
assume not x in Z;
then not x in {x,y} \/ Z by A1;
then not x in {x,y} by XBOOLE_0:def 3;
hence thesis by TARSKI:def 2;
end;
theorem
x in Z & y in Z implies {x,y} \/ Z = Z by Th31,XBOOLE_1:12;
theorem
{x} \/ X <> {};
theorem
{x,y} \/ X <> {};
::
:: Intersection of an unordered pair (or a singleton) and a set.
::
theorem
X /\ {x} = {x} implies x in X by Lm7;
theorem
x in X implies X /\ {x} = {x} by Lm1,XBOOLE_1:28;
theorem
x in Z & y in Z implies {x,y} /\ Z = {x,y} by Th31,XBOOLE_1:28;
theorem
{x} misses X implies not x in X by Lm5;
theorem Th48:
{x,y} misses Z implies not x in Z
proof
A1: x in {x,y} by TARSKI:def 2;
assume {x,y} /\ Z = {} & x in Z;
hence contradiction by A1,XBOOLE_0:def 4;
end;
theorem
not x in X implies {x} misses X by Lm6;
theorem Th50:
not x in Z & not y in Z implies {x,y} misses Z
proof
assume
A1: ( not x in Z)& not y in Z;
assume {x,y} meets Z;
then consider z such that
A2: z in {x,y} /\ Z by XBOOLE_0:4;
z in {x,y} & z in Z by A2,XBOOLE_0:def 4;
hence contradiction by A1,TARSKI:def 2;
end;
theorem
{x} misses X or {x} /\ X = {x} by Lm6,Lm8;
theorem
{x,y} /\ X = {x} implies not y in X or x = y
proof
A1: y in {x,y} by TARSKI:def 2;
assume {x,y} /\ X = {x} & y in X;
then y in {x} by A1,XBOOLE_0:def 4;
hence thesis by TARSKI:def 1;
end;
theorem
x in X & (not y in X or x = y) implies {x,y} /\ X = {x}
proof
assume
A1: x in X &( not y in X or x=y);
for z holds z in {x,y} /\ X iff z=x
proof
let z be object;
z in {x,y} /\ X iff z in {x,y} & z in X by XBOOLE_0:def 4;
hence thesis by A1,TARSKI:def 2;
end;
hence thesis by TARSKI:def 1;
end;
theorem
{x,y} /\ X = {x,y} implies x in X
proof
assume {x,y} /\ X = {x,y};
then x in {x,y} /\ X & y in {x,y} /\ X or x in X /\ {x,y} & y in X /\ {x,y}
by TARSKI:def 2;
hence thesis by XBOOLE_0:def 4;
end;
::
:: Difference of an unordered pair (or a singleton) and a set.
::
theorem Th55:
z in X \ {x} iff z in X & z <> x
proof
z in X \ {x} iff z in X & not z in {x} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
theorem Th56:
X \ {x} = X iff not x in X
proof
X \ {x} = X iff X misses {x} by XBOOLE_1:83;
hence thesis by Lm5,Lm6;
end;
theorem
X \ {x} = {} implies X = {} or X = {x}
proof
assume X \ {x} = {};
then X c= {x} by XBOOLE_1:37;
hence thesis by Lm3;
end;
theorem
{x} \ X = {x} iff not x in X by Lm5,Lm6,XBOOLE_1:83;
theorem
{x} \ X = {} iff x in X by Lm1,XBOOLE_1:37;
theorem
{x} \ X = {} or {x} \ X = {x} by Lm9,Lm10;
theorem
{x,y} \ X = {x} iff not x in X & (y in X or x = y) by Lm11;
theorem
{x,y} \ X = {x,y} iff not x in X & not y in X by Th48,Th50,XBOOLE_1:83;
theorem Th63:
{x,y} \ X = {} iff x in X & y in X
proof
{x,y} \ X = {} iff {x,y} c= X by XBOOLE_1:37;
hence thesis by Th31;
end;
theorem
{x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x ,y}
proof
assume that
A1: {x,y} \ X <> {} and
A2: {x,y} \ X <> {x} and
A3: {x,y} \ X <> {y};
A4: not x in X & x<>y or y in X by A3,Lm11;
x in X or not y in X & x<>y by A2,Lm11;
hence thesis by A1,A4,Th50,Th63,XBOOLE_1:83;
end;
theorem
X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y}
proof
X \ {x,y} = {} iff X c= {x,y} by XBOOLE_1:37;
hence thesis by Lm13;
end;
::
:: Power Set.
::
theorem
A c= B implies bool A c= bool B
proof
assume
A1: A c= B;
let x;
reconsider xx=x as set by TARSKI:1;
assume x in bool A;
then xx c= A by Def1;
then xx c= B by A1;
hence thesis by Def1;
end;
theorem
{ A } c= bool A
proof
A in bool A by Def1;
hence thesis by Lm1;
end;
theorem
bool A \/ bool B c= bool (A \/ B)
proof
let x;
reconsider xx=x as set by TARSKI:1;
assume x in bool A \/ bool B;
then x in bool A or x in bool B by XBOOLE_0:def 3;
then
A1: xx c= A or xx c= B by Def1;
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then xx c= A \/ B by A1;
hence thesis by Def1;
end;
theorem
bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable
proof
assume
A1: bool A \/ bool B = bool (A \/ B);
A \/ B in bool (A \/ B) by Def1;
then A \/ B in bool A or A \/ B in bool B by A1,XBOOLE_0:def 3;
then
A2: A \/ B c= A or A \/ B c= B by Def1;
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
hence A c= B or B c= A by A2;
end;
theorem
bool (A /\ B) = bool A /\ bool B
proof
now
let x;
reconsider xx=x as set by TARSKI:1;
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then xx c= A & xx c= B iff xx c= A /\ B by XBOOLE_1:19;
then x in bool A & x in bool B iff x in bool (A /\ B) by Def1;
hence x in bool (A /\ B) iff x in bool A /\ bool B by XBOOLE_0:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
bool (A \ B) c= { {} } \/ (bool A \ bool B)
proof
let x;
reconsider xx=x as set by TARSKI:1;
assume x in bool (A \ B);
then
A1: xx c= A \ B by Def1;
then xx misses B by XBOOLE_1:63,79;
then A \ B c= A & xx /\ B = {} by XBOOLE_1:36;
then x = {} or xx c= A & not xx c= B by A1,XBOOLE_1:28;
then x in { {} } or x in bool A & not x in bool B by Def1,TARSKI:def 1;
then x in { {} } or x in bool A \ bool B by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
theorem
bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B)
proof
let x;
reconsider xx=x as set by TARSKI:1;
assume x in bool (A \ B) \/ bool (B \ A);
then x in bool (A \ B) or x in bool (B \ A) by XBOOLE_0:def 3;
then
A1: xx c= A \ B or xx c= B \ A by Def1;
xx c= (A \ B) \/ (B \ A)
proof
let z;
assume z in xx;
then z in A \ B or z in B \ A by A1;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by Def1;
end;
::
:: Union of a set.
::
theorem
X in A implies X c= union A by Lm14;
theorem
union { X,Y } = X \/ Y by Lm15;
theorem
(for X st X in A holds X c= Z) implies union A c= Z
proof
assume
A1: for X st X in A holds X c= Z;
let y;
assume y in union A;
then consider Y such that
A2: y in Y and
A3: Y in A by TARSKI:def 4;
Y c= Z by A1,A3;
hence thesis by A2;
end;
theorem Th76:
A c= B implies union A c= union B
proof
assume
A1: A c= B;
let x;
assume x in union A;
then consider Y such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
Y in B by A1,A3;
hence thesis by A2,TARSKI:def 4;
end;
theorem
union (A \/ B) = union A \/ union B
proof
A1: union (A \/ B) c= union A \/ union B
proof
let x;
assume x in union (A \/ B);
then consider Y such that
A2: x in Y and
A3: Y in A \/ B by TARSKI:def 4;
Y in A or Y in B by A3,XBOOLE_0:def 3;
then x in union A or x in union B by A2,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
union A c= union (A \/ B) & union B c= union (A \/ B) by Th76,XBOOLE_1:7;
hence thesis by A1,XBOOLE_1:8;
end;
theorem Th78:
union (A /\ B) c= union A /\ union B
proof
let x;
assume x in union (A /\ B);
then consider Y such that
A1: x in Y and
A2: Y in A /\ B by TARSKI:def 4;
Y in B by A2,XBOOLE_0:def 4;
then
A3: x in union B by A1,TARSKI:def 4;
Y in A by A2,XBOOLE_0:def 4;
then x in union A by A1,TARSKI:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem Th79:
(for X st X in A holds X misses B) implies union A misses B
proof
assume
A1: for X st X in A holds X misses B;
assume union(A) meets B;
then consider z such that
A2: z in union(A) /\ B by XBOOLE_0:4;
z in union(A) by A2,XBOOLE_0:def 4;
then consider X such that
A3: z in X and
A4: X in A by TARSKI:def 4;
z in B by A2,XBOOLE_0:def 4;
then z in X /\ B by A3,XBOOLE_0:def 4;
hence contradiction by A1,A4,XBOOLE_0:4;
end;
theorem
union bool A = A
proof
now
let x;
thus x in union bool A implies x in A
proof
assume x in union bool A;
then consider X such that
A1: x in X and
A2: X in bool A by TARSKI:def 4;
X c= A by A2,Def1;
hence thesis by A1;
end;
assume x in A;
then { x } c= A by Lm1;
then
A3: { x } in bool A by Def1;
x in { x } by TARSKI:def 1;
hence x in union bool A by A3,TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
A c= bool union A
proof
let x;
reconsider xx=x as set by TARSKI:1;
assume x in A;
then xx c= union A by Lm14;
hence thesis by Def1;
end;
theorem
(for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y) implies
union(A /\ B) = union A /\ union B
proof
assume
A1: for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y;
union A /\ union B c= union (A /\ B)
proof
let x;
assume
A2: x in union A /\ union B;
then x in union A by XBOOLE_0:def 4;
then consider X such that
A3: x in X and
A4: X in A by TARSKI:def 4;
x in union B by A2,XBOOLE_0:def 4;
then consider Y such that
A5: x in Y and
A6: Y in B by TARSKI:def 4;
now
A7: x in X /\ Y by A3,A5,XBOOLE_0:def 4;
assume
A8: X<>Y;
X in A \/ B & Y in A \/ B by A4,A6,XBOOLE_0:def 3;
hence contradiction by A1,A8,A7,XBOOLE_0:4;
end;
then Y in A /\ B by A4,A6,XBOOLE_0:def 4;
hence thesis by A5,TARSKI:def 4;
end;
hence thesis by Th78;
end;
::
:: Cartesian product.
::
theorem Th83:
A c= [:X,Y:] & z in A implies
ex x,y st x in X & y in Y & z = [ x,y]
proof
assume A c= [:X,Y:] & z in A;
then z in [:X,Y:];
hence thesis by Def2;
end;
theorem Th84:
z in [:X1, Y1:] /\ [:X2, Y2:] implies ex x,y st z = [x,y] & x
in X1 /\ X2 & y in Y1 /\ Y2
proof
assume
A1: z in [:X1, Y1:] /\ [:X2, Y2:];
then z in [:X1, Y1:] by XBOOLE_0:def 4;
then consider x1,y1 such that
A2: x1 in X1 and
A3: y1 in Y1 and
A4: z=[x1,y1] by Def2;
z in [:X2, Y2:] by A1,XBOOLE_0:def 4;
then consider x2,y2 such that
A5: x2 in X2 and
A6: y2 in Y2 and
A7: z=[x2,y2] by Def2;
y1=y2 by A4,A7,XTUPLE_0:1;
then
A8: y1 in Y1 /\ Y2 by A3,A6,XBOOLE_0:def 4;
x1=x2 by A4,A7,XTUPLE_0:1;
then x1 in X1 /\ X2 by A2,A5,XBOOLE_0:def 4;
hence thesis by A4,A8;
end;
theorem
[:X,Y:] c= bool bool (X \/ Y)
proof
let z;
reconsider zz=z as set by TARSKI:1;
assume z in [:X,Y:];
then consider x,y such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by Def2;
zz c= bool (X \/ Y)
proof
let u;
assume u in zz;
then
A4: u = {x,y} or u = {x} by A3,TARSKI:def 2;
X c= X \/ Y & {x} c= X by A1,Lm1,XBOOLE_1:7;
then
A5: {x} c= X \/ Y;
x in X \/ Y & y in X \/ Y by A1,A2,XBOOLE_0:def 3;
then {x,y} c= X \/ Y by Th31;
hence thesis by A5,A4,Def1;
end;
hence thesis by Def1;
end;
theorem
for x,y being object holds [x,y] in [:X,Y:] iff x in X & y in Y by Lm16;
theorem Th87:
[x,y] in [:X,Y:] implies [y,x] in [:Y,X:]
proof
[x,y] in [:X,Y:] implies x in X & y in Y by Lm16;
hence thesis by Lm16;
end;
theorem
(for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:]) implies [:X1
,Y1:]=[:X2,Y2:]
proof
assume
A1: for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:];
now
let z;
thus z in [:X1,Y1:] implies z in [:X2,Y2:]
proof
assume
A2: z in [:X1,Y1:];
then ex x,y st x in X1 & y in Y1 & [x,y]=z by Def2;
hence thesis by A1,A2;
end;
assume
A3: z in [:X2,Y2:];
then ex x,y st x in X2 & y in Y2 & [x,y]=z by Def2;
hence z in [:X1,Y1:] by A1,A3;
end;
hence thesis by TARSKI:2;
end;
Lm17: A c= [:X1,Y1:] & B c= [:X2,Y2:] & (for x,y holds [x,y] in A iff [x,y] in
B) implies A = B
proof
assume that
A1: A c= [:X1,Y1:] and
A2: B c= [:X2,Y2:] and
A3: for x,y holds [x,y] in A iff [x,y] in B;
now
let z;
A4: z in B implies ex x,y st x in X2 & y in Y2 & z=[x,y] by A2,Th83;
z in A implies ex x,y st x in X1 & y in Y1 & z=[x,y] by A1,Th83;
hence z in A iff z in B by A3,A4;
end;
hence thesis by TARSKI:2;
end;
Lm18: ( for z st z in A ex x,y st z = [x,y]) & (for z st z in B ex x,y st z=[x
,y]) & (for x,y holds [x,y] in A iff [x,y] in B) implies A = B
proof
assume that
A1: for z st z in A ex x,y st z=[x,y] and
A2: for z st z in B ex x,y st z=[x,y] and
A3: for x,y holds [x,y] in A iff [x,y] in B;
now
let z;
A4: z in B implies ex x,y st z=[x, y ] by A2;
z in A implies ex x,y st z=[x,y] by A1;
hence z in A iff z in B by A3,A4;
end;
hence thesis by TARSKI:2;
end;
theorem Th89:
[:X,Y:] = {} iff X = {} or Y = {}
proof
thus [:X,Y:] = {} implies X={} or Y={}
proof
assume
A1: [:X,Y:] = {};
assume X<>{};
then consider x such that
A2: x in X by XBOOLE_0:7;
assume Y<>{};
then consider y such that
A3: y in Y by XBOOLE_0:7;
[x,y] in [:X,Y:] by A2,A3,Def2;
hence contradiction by A1;
end;
assume
A4: not thesis;
then consider z such that
A5: z in [:X,Y:] by XBOOLE_0:7;
ex x,y st x in X & y in Y & [x,y]=z by A5,Def2;
hence contradiction by A4;
end;
theorem
X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y
proof
assume X<>{};
then consider x such that
A1: x in X by XBOOLE_0:7;
assume Y<>{};
then consider y such that
A2: y in Y by XBOOLE_0:7;
assume
A3: [:X,Y:]=[:Y,X:];
for z holds z in X iff z in Y
proof let z;
thus z in X implies z in Y
proof
assume z in X;
then [z,y] in [:Y,X:] by A2,A3,Lm16;
hence thesis by Lm16;
end;
assume z in Y;
then [z,x] in [:X,Y:] by A1,A3,Lm16;
hence thesis by Lm16;
end;
hence thesis by TARSKI:2;
end;
theorem
[:X,X:] = [:Y,Y:] implies X = Y
proof
assume
A1: [:X,X:] = [:Y,Y:];
for x holds x in X iff x in Y
proof let x;
x in X iff [x,x] in [:X,X:] by Lm16;
hence thesis by A1,Lm16;
end;
hence thesis by TARSKI:2;
end;
Lm19: z in [:X,Y:] implies ex x,y st [x,y] = z
proof
assume z in [:X,Y:];
then ex x,y st x in X & y in Y & [x,y]=z by Def2;
hence thesis;
end;
theorem
X c= [:X,Y:] implies X = {}
proof
assume
A1: X c= [:X,Y:];
assume X <> {};
then consider z such that
A2: z in X by XBOOLE_0:7;
consider M such that
A3: M in X \/ union X and
A4: X \/ union X misses M by A2,XREGULAR:1;
now
assume
A5: M in X;
then consider x,y such that
A6: M = [x,y] by Lm19,A1;
A7: {x} in M by A6,TARSKI:def 2;
M c= union X by A5,Lm14;
then {x} in union X by A7;
then {x} in X \/ union X by XBOOLE_0:def 3;
hence contradiction by A4,A7,XBOOLE_0:3;
end;
then M in union X by A3,XBOOLE_0:def 3;
then consider Z such that
A8: M in Z and
A9: Z in X by TARSKI:def 4;
Z in [:X,Y:] by A1,A9;
then consider x,y such that
A10: x in X and y in Y and
A11: Z = [x,y] by Def2;
M={x} or M={x,y} by A8,A11,TARSKI:def 2;
then
A12: x in M by TARSKI:def 1,def 2;
x in X \/ union X by A10,XBOOLE_0:def 3;
hence contradiction by A4,A12,XBOOLE_0:3;
end;
theorem
Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y
proof
assume Z<>{};
then consider z such that
A1: z in Z by XBOOLE_0:7;
assume
A2: [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:];
let x;
assume x in X;
then [x,z] in [:X,Z:] & [z,x] in [:Z,X:] by A1,Def2;
then [x,z] in [:Y,Z:] or [z,x] in [:Z,Y:] by A2;
hence thesis by Lm16;
end;
theorem Th94:
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 z;
assume z in [:X,Z:];
then consider x,y such that
A2: x in X and
A3: y in Z & z=[x,y] by Def2;
x in Y by A1,A2;
hence thesis by A3,Def2;
end;
let z;
assume z in [:Z,X:];
then consider y,x such that
A4: y in Z and
A5: x in X and
A6: z=[y,x] by Def2;
x in Y by A1,A5;
hence thesis by A4,A6,Def2;
end;
theorem Th95:
X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:]
proof
assume X1 c= Y1 & X2 c= Y2;
then [:X1,X2:] c= [:Y1,X2:] & [:Y1,X2:] c= [:Y1,Y2:] by Th94;
hence thesis;
end;
theorem Th96:
[:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:]
proof
A1: for z st z in [:X \/ Y, Z:] ex x,y st z=[x,y] by Lm19;
A2: for x,y holds [x,y] in [:X \/ Y, Z:] iff [x,y] in [:X, Z:] \/ [:Y, Z:]
proof
let x,y;
thus [x,y] in [:X \/ Y, Z:] implies [x,y] in [:X, Z:] \/ [:Y, Z:]
proof
assume
A3: [x,y] in [:X \/ Y, Z:];
then x in X \/ Y by Lm16;
then
A4: x in X or x in Y by XBOOLE_0:def 3;
y in Z by A3,Lm16;
then [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] by A4,Lm16;
hence thesis by XBOOLE_0:def 3;
end;
assume [x,y] in [:X, Z:] \/ [:Y, Z:];
then [x,y] in [:X, Z:] or [x,y] in [:Y, Z:] by XBOOLE_0:def 3;
then
A5: x in X & y in Z or x in Y & y in Z by Lm16;
then x in X \/ Y by XBOOLE_0:def 3;
hence thesis by A5,Lm16;
end;
A6: z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x,y st z=[x,y]
proof
assume z in [:X1,X2:] \/ [:Y1,Y2:];
then z in [:X1,X2:] or z in [:Y1,Y2:] by XBOOLE_0:def 3;
hence thesis by Lm19;
end;
then for z st z in [:X,Z:] \/ [:Y,Z:] ex x,y st z=[x,y];
hence
A7: [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] by A1,A2,Lm18;
A8: for y,x holds [y,x] in [:Z, X \/ Y:] iff [y,x] in [:Z, X:] \/ [:Z, Y:]
proof
let y,x;
A9: [x,y]in[:X, Z:] or [x,y]in[:Y,Z:] iff [y,x]in[:Z,X:] or [y,x]in[:Z,Y
:] by Th87;
[y,x] in [:Z, X \/ Y:] iff [x,y] in [:X \/ Y, Z:] by Th87;
hence thesis by A7,A9,XBOOLE_0:def 3;
end;
A10: for z st z in [:Z,X \/ Y:] ex x,y st z=[x,y] by Lm19;
for z st z in [:Z,X:] \/ [:Z,Y:] ex x,y st z=[x,y] by A6;
hence thesis by A10,A8,Lm18;
end;
theorem
[:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2, Y2:]
proof
thus [:X1 \/ X2, Y1 \/ Y2:] = [:X1, Y1 \/ Y2:] \/ [:X2, Y1 \/ Y2:] by Th96
.= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1 \/ Y2:] by Th96
.= [:X1,Y1:] \/ [:X1,Y2:] \/ ([:X2,Y1:] \/ [:X2,Y2:]) by Th96
.= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:] by XBOOLE_1:4;
end;
theorem
[:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z , Y :]
proof
A1: for x,y holds [x,y] in [:X /\ Y, Z:] iff [x,y] in [:X, Z:] /\ [:Y, Z :]
proof
let x,y;
thus [x,y] in [:X /\ Y, Z:] implies [x,y] in [:X, Z:] /\ [:Y, Z:]
proof
assume
A2: [x,y] in [:X /\ Y, Z:];
then
A3: x in X /\ Y by Lm16;
A4: y in Z by A2,Lm16;
x in Y by A3,XBOOLE_0:def 4;
then
A5: [x,y] in [:Y,Z:] by A4,Lm16;
x in X by A3,XBOOLE_0:def 4;
then [x,y] in [:X,Z:] by A4,Lm16;
hence thesis by A5,XBOOLE_0:def 4;
end;
assume
A6: [x,y] in [:X, Z:] /\ [:Y, Z:];
then [x,y] in [:Y, Z:] by XBOOLE_0:def 4;
then
A7: x in Y by Lm16;
A8: [x,y] in [:X, Z:] by A6,XBOOLE_0:def 4;
then x in X by Lm16;
then
A9: x in X /\ Y by A7,XBOOLE_0:def 4;
y in Z by A8,Lm16;
hence thesis by A9,Lm16;
end;
[:X, Z:] /\ [:Y, Z:] c= [:X, Z:] by XBOOLE_1:17;
hence
A10: [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] by A1,Lm17;
A11: for y,x holds [y,x] in [:Z, X /\ Y:] iff [y,x] in [:Z, X:] /\ [:Z, Y:]
proof
let y,x;
A12: [x,y]in[:X, Z:] & [x,y]in[:Y,Z:] iff [y,x]in[:Z,X:] & [y,x]in[:Z,Y:]
by Th87;
[y,x] in [:Z, X /\ Y:] iff [x,y] in [:X /\ Y, Z:] by Th87;
hence thesis by A10,A12,XBOOLE_0:def 4;
end;
[:Z, X:] /\ [:Z, Y:] c= [:Z, X:] by XBOOLE_1:17;
hence thesis by A11,Lm17;
end;
theorem Th99:
[:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:]
proof
Y1 /\ Y2 c= Y2 & X1 /\ X2 c= X2 by XBOOLE_1:17;
then
A1: [:X1 /\ X2, Y1 /\ Y2:] c= [:X2, Y2:] by Th95;
A2: [:X1, Y1:] /\ [:X2, Y2:] c= [:X1 /\ X2, Y1 /\ Y2:]
proof
let z;
assume z in [:X1, Y1:] /\ [:X2, Y2:];
then ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by Th84;
hence thesis by Def2;
end;
Y1 /\ Y2 c= Y1 & X1 /\ X2 c= X1 by XBOOLE_1:17;
then [:X1 /\ X2, Y1 /\ Y2:] c= [:X1, Y1:] by Th95;
hence thesis by A2,A1,XBOOLE_1:19;
end;
theorem
A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:]
proof
assume that
A1: A c= X and
A2: B c= Y;
A3: [:A,Y:] /\ [:X,B:] = [:A /\ X, Y /\ B:] by Th99;
A /\ X = A by A1,XBOOLE_1:28;
hence thesis by A2,A3,XBOOLE_1:28;
end;
theorem Th101:
[:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:]
proof
A1: for x,y holds [x,y] in [:X \ Y, Z:] iff [x,y] in [:X, Z:] \ [:Y, Z:]
proof
let x,y;
thus [x,y] in [:X \ Y, Z:] implies [x,y] in [:X, Z:] \ [:Y, Z:]
proof
assume
A2: [x,y] in [:X \ Y, Z:];
then
A3: x in X \ Y by Lm16;
then
A4: x in X by XBOOLE_0:def 5;
not x in Y by A3,XBOOLE_0:def 5;
then
A5: not [x,y] in [:Y,Z:] by Lm16;
y in Z by A2,Lm16;
then [x,y] in [:X,Z:] by A4,Lm16;
hence thesis by A5,XBOOLE_0:def 5;
end;
assume
A6: [x,y] in [:X, Z:] \ [:Y, Z:];
then
A7: [x,y] in [:X, Z:] by XBOOLE_0:def 5;
then
A8: y in Z by Lm16;
not [x,y] in [:Y, Z:] by A6,XBOOLE_0:def 5;
then
A9: not (x in Y & y in Z) by Lm16;
x in X by A7,Lm16;
then x in X \ Y by A7,A9,Lm16,XBOOLE_0:def 5;
hence thesis by A8,Lm16;
end;
[:X, Z:] \ [:Y, Z:] c= [:X, Z:] by XBOOLE_1:36;
hence
A10: [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] by A1,Lm17;
A11: for y,x holds [y,x] in [:Z, X \ Y:] iff [y,x] in [:Z, X:] \ [:Z, Y:]
proof
let y,x;
A12: [x,y]in[:X, Z:]& not[x,y]in[:Y,Z:] iff [y,x]in[:Z,X:]& not[y,x]in[:Z,
Y :] by Th87;
[y,x] in [:Z, X \ Y:] iff [x,y] in [:X \ Y, Z:] by Th87;
hence thesis by A10,A12,XBOOLE_0:def 5;
end;
[:Z, X:] \ [:Z, Y:] c= [:Z, X:] by XBOOLE_1:36;
hence thesis by A11,Lm17;
end;
theorem
[:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:]
proof
A1: [:Y1,X2:] /\ [:X1,Y2:] = [:Y1 /\ X1, X2 /\ Y2:] by Th99;
Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 by XBOOLE_1:17;
then
A2: [:Y1 /\ X1, X2 /\ Y2:] c= [:Y1,Y2:] by Th95;
A3: [:X1\Y1,X2:] \/ [:X1,X2\Y2:] c= [:X1,X2:] \ [:Y1, Y2:]
proof
let z;
A4: now
assume z in [:X1\Y1,X2:];
then consider x,y such that
A5: x in X1\Y1 and
A6: y in X2 and
A7: z=[x,y] by Def2;
not x in Y1 by A5,XBOOLE_0:def 5;
then
A8: not z in [:Y1,Y2:] by A7,Lm16;
x in X1 by A5,XBOOLE_0:def 5;
then z in [:X1,X2:] by A6,A7,Lm16;
hence thesis by A8,XBOOLE_0:def 5;
end;
A9: now
assume z in [:X1,X2\Y2:];
then consider x,y such that
A10: x in X1 and
A11: y in X2\Y2 and
A12: z=[x,y] by Def2;
not y in Y2 by A11,XBOOLE_0:def 5;
then
A13: not z in [:Y1,Y2:] by A12,Lm16;
y in X2 by A11,XBOOLE_0:def 5;
then z in [:X1,X2:] by A10,A12,Lm16;
hence thesis by A13,XBOOLE_0:def 5;
end;
assume z in [:X1\Y1,X2:] \/ [:X1,X2\Y2:];
hence thesis by A4,A9,XBOOLE_0:def 3;
end;
[:X1\Y1,X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,X2\Y2:] = [:X1,X2:] \ [:X1,
Y2 :] by Th101;
then [:X1\Y1,X2:] \/ [:X1,X2\Y2:] = [:X1,X2:] \ [:Y1 /\ X1, X2 /\ Y2:] by A1,
XBOOLE_1:54;
hence thesis by A3,A2,XBOOLE_1:34;
end;
theorem Th103:
X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:]
proof
assume
A1: X1 misses X2 or Y1 misses Y2;
assume not thesis;
then consider z such that
A2: z in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:4;
ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by A2,Th84;
hence contradiction by A1;
end;
theorem
[x,y] in [:{z},Y:] iff x = z & y in Y
proof
A1: x in {z} iff x=z by TARSKI:def 1;
hence [x,y] in [:{z},Y:] implies x=z & y in Y by Lm16;
thus thesis by A1,Lm16;
end;
theorem
[x,y] in [:X,{z}:] iff x in X & y = z
proof
A1: y in {z} iff y=z by TARSKI:def 1;
hence [x,y] in [:X,{z}:] implies x in X & y=z by Lm16;
thus thesis by A1,Lm16;
end;
theorem
X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {} by Th89;
theorem
x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:]
proof
assume x<>y;
then {x} misses {y} by Th11;
hence thesis by Th103;
end;
theorem
[:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X, {y} :]
proof
{x,y}={x} \/ {y} by ENUMSET1:1;
hence thesis by Th96;
end;
theorem Th109:
X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2
proof
assume
A1: X1<>{};
then consider x such that
A2: x in X1 by XBOOLE_0:7;
assume
A3: Y1<>{};
then consider y such that
A4: y in Y1 by XBOOLE_0:7;
assume
A5: [:X1,Y1:] = [:X2,Y2:];
then
A6: [:X2,Y2:] <> {} by A1,A3,Th89;
then
A7: Y2 <> {} by Th89;
for z holds z in X1 iff z in X2
proof let z;
consider y2 such that
A8: y2 in Y2 by A7,XBOOLE_0:7;
thus z in X1 implies z in X2
proof
assume z in X1;
then [z,y] in [:X2,Y2:] by A4,A5,Lm16;
hence thesis by Lm16;
end;
assume z in X2;
then [z,y2] in [:X2,Y2:] by A8,Lm16;
hence thesis by A5,Lm16;
end;
hence X1 = X2 by TARSKI:2;
A9: X2 <> {} by A6,Th89;
for z holds z in Y1 iff z in Y2
proof let z;
consider x2 such that
A10: x2 in X2 by A9,XBOOLE_0:7;
thus z in Y1 implies z in Y2
proof
assume z in Y1;
then [x,z] in [:X2,Y2:] by A2,A5,Lm16;
hence thesis by Lm16;
end;
assume z in Y2;
then [x2,z] in [:X2,Y2:] by A10,Lm16;
hence thesis by A5,Lm16;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= [:X,Y:] or X c= [:Y,X:] implies X = {}
proof
assume
A1: X c= [:X,Y:] or X c= [:Y,X:];
assume
A2: X <> {};
A3: now
defpred P[object] means ex Y st $1=Y & ex z st z in Y & z in X;
consider Z such that
A4: for y holds y in Z iff y in union X & P[y] from XBOOLE_0:sch 1;
consider Y2 such that
A5: Y2 in X \/ Z and
A6: X \/ Z misses Y2 by A2,XREGULAR:1;
now
assume
A7: not ex Y2 st Y2 in X & for Y1 st Y1 in Y2 holds for z holds not
z in Y1 or not z in X;
now
assume
A8: Y2 in X;
then consider Y1 such that
A9: Y1 in Y2 and
A10: ex z st z in Y1 & z in X by A7;
Y1 in union X by A8,A9,TARSKI:def 4;
then Y1 in Z by A4,A10;
then Y1 in X \/ Z by XBOOLE_0:def 3;
hence contradiction by A6,A9,XBOOLE_0:3;
end;
then Y2 in Z by A5,XBOOLE_0:def 3;
then ex X2 st Y2=X2 & ex z st z in X2 & z in X by A4;
then consider z such that
A11: z in Y2 and
A12: z in X;
z in X \/ Z by A12,XBOOLE_0:def 3;
hence contradiction by A6,A11,XBOOLE_0:3;
end;
then consider Y1 such that
A13: Y1 in X and
A14: not ex Y2 st Y2 in Y1 & ex z st z in Y2 & z in X;
A15: now
given y,x such that
A16: x in X and
A17: Y1 = [y,x];
A18: x in {y,x} by TARSKI:def 2;
{y,x} in Y1 by A17,TARSKI:def 2;
hence contradiction by A14,A16,A18;
end;
assume X c= [:Y,X:];
then Y1 in [:Y,X:] by A13;
then ex y,x being object st y in Y & x in X & Y1 = [y,x] by Def2;
hence contradiction by A15;
end;
now
consider z being object such that
A19: z in X by A2,XBOOLE_0:7;
consider Y1 such that
A20: Y1 in X \/ union X and
A21: X \/ union X misses Y1 by A19,XREGULAR:1;
assume
A22: X c= [:X,Y:];
now
assume
A23: Y1 in X;
then consider x,y such that
A24: Y1 = [x,y] by Lm19,A22;
A25: {x} in Y1 by A24,TARSKI:def 2;
Y1 c= union X by A23,Lm14;
then {x} in union X by A25;
then {x} in X \/ union X by XBOOLE_0:def 3;
hence contradiction by A21,A25,XBOOLE_0:3;
end;
then Y1 in union X by A20,XBOOLE_0:def 3;
then consider Y2 such that
A26: Y1 in Y2 and
A27: Y2 in X by TARSKI:def 4;
Y2 in [:X,Y:] by A22,A27;
then consider x,y being object such that
A28: x in X and
y in Y and
A29: Y2=[x,y] by Def2;
Y1={x} or Y1={x,y} by A26,A29,TARSKI:def 2;
then
A30: x in Y1 by TARSKI:def 1,def 2;
x in X \/ union X by A28,XBOOLE_0:def 3;
hence contradiction by A21,A30,XBOOLE_0:3;
end;
hence thesis by A1,A3;
end;
theorem
ex M st N in M & (for X,Y holds X in M & Y c= X implies Y in M) & (for
X holds X in M implies bool X in M) & for X holds X c= M implies X,M
are_equipotent or X in M
proof
consider M such that
A1: N in M and
A2: for X,Y holds X in M & Y c= X implies Y in M and
A3: for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
A4: for X holds X c= M implies X,M are_equipotent or X in M by TARSKI_A:1;
take M;
thus N in M by A1;
thus for X,Y holds X in M & Y c= X implies Y in M by A2;
thus for X holds X in M implies bool X in M
proof
let X;
assume X in M;
then consider Z such that
A5: Z in M and
A6: for Y st Y c= X holds Y in Z by A3;
now
let Y be object;
reconsider YY=Y as set by TARSKI:1;
assume Y in bool X;
then YY c= X by Def1;
hence Y in Z by A6;
end;
hence thesis by A2,A5,TARSKI:def 3;
end;
thus thesis by A4;
end;
reserve e for object, X,X1,X2,Y1,Y2 for set;
theorem
e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:X1 /\ X2, Y1 /\ Y2:]
proof
assume e in [:X1,Y1:] & e in [:X2,Y2:];
then e in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:def 4;
hence thesis by Th99;
end;
begin :: Addenda
:: from BORSUK_1
theorem Th113:
[:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies X1 c= Y1 & X2 c= Y2
proof
assume that
A1: [:X1,X2:] c= [:Y1,Y2:] and
A2: [:X1,X2:] <> {};
A3: [:X1,X2:] = [:X1,X2:] /\ [:Y1,Y2:] by A1,XBOOLE_1:28
.= [:X1/\Y1,X2/\Y2:] by Th99;
X1 <> {} & X2 <> {} by A2,Th89;
then X1 = X1/\Y1 & X2 = X2/\Y2 by A3,Th109;
hence thesis by XBOOLE_1:17;
end;
:: from ALTCAT_1
theorem
for A being non empty set, B,C,D being set st [:A,B:] c= [:C,D:] or [:
B,A:] c= [:D,C:] holds B c= D
proof
let A be non empty set, B,C,D be set such that
A1: [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:];
per cases;
suppose
B = {};
hence thesis;
end;
suppose
B <> {};
then [:A,B:] <> {} & [:B,A:] <> {} by Th89;
hence thesis by A1,Th113;
end;
end;
theorem
x in X implies (X\{x})\/{x}=X
proof
assume
A1: x in X;
thus (X\{x})\/{x}c=X
proof
let y be object;
assume y in (X\{x})\/{x};
then y in X\{x} or y in {x} by XBOOLE_0:def 3;
hence thesis by A1,Th55,TARSKI:def 1;
end;
thus X c= (X\{x})\/{x}
proof
let y be object;
assume y in X;
then y in {x} or y in X\{x} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
not x in X implies (X\/{x})\{x}=X
proof
A1: (X \/ {x}) \ {x} = X \ {x} by XBOOLE_1:40;
assume not x in X;
hence thesis by A1,Th56;
end;
:: from WAYBEL18, 2006.01.06, A.T.
theorem
for x,y,z,Z being set holds Z c= {x,y,z} iff Z = {} or Z = {x} or Z =
{y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z}
proof
let x,y,z,Z be set;
hereby
assume that
A1: Z c= {x,y,z} and
A2: Z <> {} and
A3: Z <> {x} and
A4: Z <> {y} and
A5: Z <> {z} and
A6: Z <> {x,y} and
A7: Z <> {y,z} and
A8: Z <> {x,z};
{x,y,z} c= Z
proof
let a be object;
A9: now
{x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:2
.= {y,z} \ {x} by XBOOLE_1:40;
then
A10: {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
assume not x in Z;
then Z c= {x,y,z} \ {x} by A1,Lm2;
hence contradiction by A2,A4,A5,A7,Lm13,A10,XBOOLE_1:1;
end;
A11: now
{x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:3
.= ({x} \/ {y} \/ {z}) \ {y} by ENUMSET1:1
.= ({x} \/ {z} \/ {y}) \ {y} by XBOOLE_1:4
.= ({x,z} \/ {y}) \ {y} by ENUMSET1:1
.= {x,z} \ {y} by XBOOLE_1:40;
then
A12: {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
assume not y in Z;
then Z c= {x,y,z} \ {y} by A1,Lm2;
hence contradiction by A2,A3,A5,A8,Lm13,A12,XBOOLE_1:1;
end;
A13: now
{x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:3
.= {x,y} \ {z} by XBOOLE_1:40;
then
A14: {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
assume not z in Z;
then Z c= {x,y,z} \ {z} by A1,Lm2;
hence contradiction by A2,A3,A4,A6,Lm13,A14,XBOOLE_1:1;
end;
assume a in {x,y,z};
hence thesis by A9,A11,A13,ENUMSET1:def 1;
end;
hence Z = {x,y,z} by A1;
end;
assume
A15: Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z}
or Z = {x,z} or Z = {x,y,z};
per cases by A15;
suppose
Z = {};
hence thesis;
end;
suppose
Z = {x};
then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence thesis by ENUMSET1:2;
end;
suppose
A16: Z = {y};
{x,y} c= {x,y} \/ {z} by XBOOLE_1:7;
then
A17: {x,y} c= {x,y,z} by ENUMSET1:3;
Z c= {x,y} by A16,Th7;
hence thesis by A17;
end;
suppose
Z = {z};
then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence thesis by ENUMSET1:3;
end;
suppose
Z = {x,y};
then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence thesis by ENUMSET1:3;
end;
suppose
Z = {y,z};
then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence thesis by ENUMSET1:2;
end;
suppose
A18: Z = {x,z};
A19: {x,z} \/ {y} = {x} \/ {z} \/ {y} by ENUMSET1:1
.= {x} \/ ({y} \/ {z}) by XBOOLE_1:4
.= {x} \/ {y,z} by ENUMSET1:1;
Z c= {x,z} \/ {y} by A18,XBOOLE_1:7;
hence thesis by A19,ENUMSET1:2;
end;
suppose
Z = {x,y,z};
hence thesis;
end;
end;
:: from PARTFUN1, 2006.12.05, A.T.
theorem
N c= [:X1,Y1:] & M c= [:X2,Y2:] implies N \/ M c= [:X1 \/ X2,Y1 \/ Y2 :]
proof
assume N c= [:X1,Y1:] & M c= [:X2,Y2:];
then
A1: N \/ M c= [:X1,Y1:] \/ [:X2,Y2:] by XBOOLE_1:13;
X1 c= X1 \/ X2 & Y1 c= Y1 \/ Y2 by XBOOLE_1:7;
then
A2: [:X1,Y1:] c= [:X1 \/ X2,Y1 \/ Y2:] by Th95;
Y2 c= Y1 \/ Y2 & X2 c= X1 \/ X2 by XBOOLE_1:7;
then [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] by Th95;
then [:X1,Y1:] \/ [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] by A2,XBOOLE_1:8;
hence thesis by A1;
end;
Lm20: not x in X & not y in X implies {x,y} misses X
proof
assume
A1: ( not x in X)& not y in X;
thus {x,y} /\ X c= {}
proof
let z be object;
assume z in {x,y} /\ X;
then z in {x,y} & z in X by XBOOLE_0:def 4;
hence thesis by A1,TARSKI:def 2;
end;
thus thesis;
end;
theorem Th119:
not x in X & not y in X implies X = X \ {x,y}
proof
X \ {x,y} = X iff X misses {x,y} by XBOOLE_1:83;
hence thesis by Lm20;
end;
theorem
not x in X & not y in X implies X = X \/ {x,y} \ {x,y}
proof
A1: (X \/ {x,y}) \ {x,y} = X \ {x,y} by XBOOLE_1:40;
assume ( not x in X)& not y in X;
hence thesis by A1,Th119;
end;
:: from INCPROJ, 2007.01.18. AK
definition
let x1, x2, x3 be object;
pred x1, x2, x3 are_mutually_distinct means
x1 <> x2 & x1 <> x3 & x2 <> x3;
end;
definition
let x1, x2, x3, x4 be object;
pred x1, x2, x3, x4 are_mutually_distinct means
x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;
end;
:: from CARD_2, 2007.01.18. AK
definition
let x1, x2, x3, x4, x5 be object;
pred x1, x2, x3, x4, x5 are_mutually_distinct means
x1 <> x2 & x1 <> x3 &
x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4
<> x5;
end;
:: from BORSUK_5, 2007.01.18. AK
definition
let x1, x2, x3, x4, x5, x6 be object;
pred x1, x2, x3, x4, x5, x6 are_mutually_distinct means
x1 <> x2 & x1 <> x3
& x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6;
end;
definition
let x1, x2, x3, x4, x5, x6, x7 be object;
pred x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct means
x1 <> x2 & x1
<> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <>
x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5
& x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7;
end;
:: missing, 2007.02.11, A.T.
theorem
[:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
thus [:{x1,x2},{y1,y2}:] = [:{x1}\/{x2},{y1,y2}:] by ENUMSET1:1
.= [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by Th96
.= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by Th29
.= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by Th29
.= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5;
end;
:: missing, 2008.03.22, A.T.
theorem
x <> y implies A \/ {x} \ {y} = A \ {y} \/ {x} by Th11,XBOOLE_1:87;
:: comp. REALSET1, 2008.07.05, A.T.
definition
let X;
attr X is trivial means
x in X & y in X implies x = y;
end;
registration
cluster empty -> trivial for set;
coherence;
end;
registration
cluster non trivial -> non empty for set;
coherence;
end;
registration
let x;
cluster {x} -> trivial;
coherence
proof
let y,z;
assume that
A1: y in {x} and
A2: z in {x};
y =x by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
end;
registration
cluster trivial non empty for set;
existence
proof
take {{}};
thus thesis;
end;
end;
:: from SPRECT_3, 2008.09.30, A.T.
theorem
for A,B,C being set, p be object
st A c= B & B /\ C = {p} & p in A holds A /\ C = {p}
proof
let A,B,C be set, p be object such that
A1: A c= B;
assume
A2: B /\ C = {p};
p in B /\ C by A2,TARSKI:def 1;
then
A3: p in C by XBOOLE_0:def 4;
assume p in A;
then p in A /\ C by A3,XBOOLE_0:def 4;
hence thesis by A2,Lm3,A1,XBOOLE_1:26;
end;
:: from SPRECT_2, 2008.09.30, A.T.
theorem
for A,B,C being set st A /\ B c= {p} & p in C & C misses B holds A
\/ C misses B
proof
let A,B,C be set such that
A1: A /\ B c= {p} and
A2: p in C and
A3: C misses B;
{p} c= C by A2,Lm1;
then A /\ B c= C by A1;
then A /\ B /\ B c= C /\ B by XBOOLE_1:27;
then
A4: A /\ (B /\ B) c= C /\ B by XBOOLE_1:16;
(A \/ C) /\ B = A /\ B \/ C /\ B by XBOOLE_1:23
.= {} by A3,A4,XBOOLE_1:12;
hence thesis;
end;
theorem
for A,B being set st for x,y being set st x in A & y in B holds x
misses y holds union A misses union B
proof
let A,B be set such that
A1: for x,y being set st x in A & y in B holds x misses y;
for y being set st y in B holds union A misses y
proof
let y be set;
assume y in B;
then for x being set st x in A holds x misses y by A1;
hence thesis by Th79;
end;
hence thesis by Th79;
end;
:: from BORSUK_3, 2009.01.24, A.T.
registration
let X be set, Y be empty set;
cluster [:X, Y:] -> empty;
coherence by Th89;
end;
registration
let X be empty set, Y be set;
cluster [:X, Y:] -> empty;
coherence by Th89;
end;
:: new, 2009.08.26, A.T
theorem
not A in [:A,B:]
proof
assume A in [:A,B:];
then consider x,y being object such that
A1: x in A & y in B & A = [x,y] by Th83;
reconsider x as set by TARSKI:1;
x = {x} or x = {x,y} by A1,TARSKI:def 2;
then x in x by TARSKI:def 1,def 2;
hence contradiction;
end;
theorem
B = [x,{x}] implies B in [:{x},B:]
proof assume
A1: B = [x,{x}];
then [:{x},B:] = { [x,{x}], [x,{x,{x}}] } by Th29;
hence thesis by TARSKI:def 2,A1;
end;
theorem
B in [:A,B:] implies ex x being object st x in A & B = [x,{x}]
proof
assume B in [:A,B:];
then consider x,y being object such that
A1: x in A & y in B & B = [x,y] by Th83;
take x;
thus x in A by A1;
per cases by A1,TARSKI:def 2;
suppose y = {x};
hence thesis by A1;
end;
suppose
A2: y = {x,y};
reconsider y as set by TARSKI:1;
y in y by TARSKI:def 2,A2;
hence thesis;
end;
end;
theorem
B c= A & A is trivial implies B is trivial
proof assume that
A1: B c= A and
A2: A is trivial;
let x,y;
assume x in B & y in B;
then x in A & y in A by A1;
hence thesis by A2;
end;
registration
cluster non trivial for set;
existence
proof
take {{},{{}}}, {},{{}};
thus {} in {{},{{}}} & {{}} in {{},{{}}} by TARSKI:def 2;
thus {} <> {{}};
end;
end;
theorem Th130:
X is non empty trivial implies ex x st X = {x}
proof
assume X is non empty;
then consider x being object such that
A1: x in X;
assume
A2: X is trivial;
take x;
for y being object holds y in X iff x = y by A2,A1;
hence thesis by TARSKI:def 1;
end;
theorem
for x being set, X being trivial set st x in X holds X = {x}
proof
let x be set, X be trivial set;
assume
A1: x in X;
then ex x being object st X = {x} by Th130;
hence thesis by A1,TARSKI:def 1;
end;
:: from JORDAN16, 2011.04.27, A.T.
theorem
for a,b,c,X being set st a in X & b in X & c in X holds {a,b,c} c= X
proof
let a,b,c,X be set;
assume a in X & b in X & c in X;
then {a,b} c= X & {c} c= X by Lm1,Th31;
then {a,b} \/ {c} c= X by XBOOLE_1:8;
hence thesis by ENUMSET1:3;
end;
:: Lemma from RELAT_1, FUNCT_4
theorem
[x,y] in X implies x in union union X & y in union union X
proof
assume
A1: [x,y] in X;
{ x } in {{x},{x,y}} by TARSKI:def 2;
then
A2: {x} in union X by A1,TARSKI:def 4;
{x,y} in {{x},{x,y}} by TARSKI:def 2;
then
A3: {x,y} in union X by A1,TARSKI:def 4;
y in {x,y} & x in {x} by TARSKI:def 1,def 2;
hence thesis by A3,A2,TARSKI:def 4;
end;
theorem Th134:
X c= Y \/ {x} implies x in X or X c= Y
proof
assume that
A1: X c= Y \/ {x} and
A2: not x in X;
X = X /\ (Y \/ {x}) by A1,XBOOLE_1:28
.= X /\ Y \/ X /\ {x} by XBOOLE_1:23
.= X /\ Y \/ {} by A2,Lm6,XBOOLE_0:def 7
.= X /\ Y;
hence thesis by XBOOLE_1:17;
end;
theorem
x in X \/ {y} iff x in X or x = y
proof
x in X \/ {y} iff x in X or x in {y} by XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
theorem
X \/ {x} c= Y iff x in Y & X c= Y
proof
X c= Y & {x} c= Y implies X \/ {x} c= Y by XBOOLE_1:8;
hence thesis by Lm1,XBOOLE_1:11;
end;
theorem
for A, B being set st A c= B & B c= A \/ {a} holds A \/ {a} = B or A = B
proof
let A, B be set;
assume that
A1: A c= B and
A2: B c= A \/ {a};
assume that
A3: A \/ {a} <> B and
A4: A <> B;
not a in B
proof
assume a in B;
then {a} c= B by Lm1;
hence thesis by A1,A2,A3,XBOOLE_1:8;
end;
hence thesis by A2,Th134,A1,A4;
end;
registration let A,B be trivial set;
cluster [:A,B:] -> trivial;
coherence
proof
per cases;
suppose A is empty or B is empty;
hence thesis;
end;
suppose that
A1: A is not empty and
A2: B is not empty;
consider a being object such that
A3: A = {a} by A1,Th130;
consider b being object such that
A4: B = {b} by A2,Th130;
[:A,B:] = {[a,b]} by A3,A4,Th28;
hence thesis;
end;
end;
end;
:: from REALSET1, 2012.08.12, A.T.
theorem
for X being set holds X is non trivial iff
for x holds X\{x} is non empty
proof
let X be set;
hereby
assume
A1: X is non trivial;
let x be object;
X <> {x} by A1;
then consider y being object such that
A2: y in X and
A3: x <> y by A1,Lm12;
not y in {x} by A3,TARSKI:def 1;
hence X\{x} is non empty by A2,XBOOLE_0:def 5;
end;
assume
A4: for x holds X\{x} is non empty;
X\{{}} c= X by XBOOLE_1:36;
then X is non empty by A4;
then consider x being object such that
A5: x in X;
X\{x} is non empty by A4;
then consider y being object such that
A6: y in X\{x};
reconsider x,y as set by TARSKI:1;
take x,y;
thus x in X by A5;
X\{x} c= X by XBOOLE_1:36;
hence y in X by A6;
x in {x} by TARSKI:def 1;
hence x <> y by A6,XBOOLE_0:def 5;
end;