Copyright (c) 1989 Association of Mizar Users
environ
vocabulary BOOLE, SUBSET_1, NEWTON;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
clusters XBOOLE_0;
requirements BOOLE;
definitions TARSKI, XBOOLE_0;
theorems XBOOLE_0, TARSKI, ENUMSET1, ZFMISC_1, XBOOLE_1;
schemes XBOOLE_0;
begin
reserve E,X,x,y for set;
definition let X be set;
cluster bool X -> non empty;
coherence by ZFMISC_1:def 1;
end;
definition let x;
cluster { x } -> non empty;
coherence by TARSKI:def 1;
let y;
cluster { x, y } -> non empty;
coherence by TARSKI:def 2;
end;
definition let X;
canceled;
mode Element of X means
:Def2: it in X if X is non empty
otherwise it is empty;
existence by XBOOLE_0:def 1;
consistency;
end;
definition let X;
mode Subset of X is Element of bool X;
end;
definition let X be non empty set;
cluster non empty Subset of X;
existence
proof
X in bool X by ZFMISC_1:def 1;
then X is Subset of X by Def2;
hence thesis;
end;
end;
definition let X1,X2 be non empty set;
cluster [: X1,X2 :] -> non empty;
coherence
proof
consider x1 being set such that
A1: x1 in X1 by XBOOLE_0:def 1;
consider x2 being set such that
A2: x2 in X2 by XBOOLE_0:def 1;
[x1,x2] in [:X1,X2:] by A1,A2,ZFMISC_1:def 2;
hence thesis;
end;
end;
definition let X1,X2,X3 be non empty set;
cluster [: X1,X2,X3 :] -> non empty;
coherence
proof
consider x12 being set such that
A1: x12 in [:X1,X2:] by XBOOLE_0:def 1;
consider x3 being set such that
A2: x3 in X3 by XBOOLE_0:def 1;
[x12,x3] in [:[:X1,X2:],X3:] by A1,A2,ZFMISC_1:def 2;
hence thesis by ZFMISC_1:def 3;
end;
end;
definition let X1,X2,X3,X4 be non empty set;
cluster [: X1,X2,X3,X4 :] -> non empty;
coherence
proof
consider x123 being set such that
A1: x123 in [:X1,X2,X3:] by XBOOLE_0:def 1;
consider x4 being set such that
A2: x4 in X4 by XBOOLE_0:def 1;
[x123,x4] in [:[:X1,X2,X3:],X4:] by A1,A2,ZFMISC_1:def 2;
hence thesis by ZFMISC_1:def 4;
end;
end;
definition let D be non empty set, X be non empty Subset of D;
redefine mode Element of X -> Element of D;
coherence
proof let x be Element of X;
A1: x in X by Def2;
X in bool D by Def2;
then X c= D by ZFMISC_1:def 1;
then x in D by A1,TARSKI:def 3;
hence x is Element of D by Def2;
end;
end;
Lm1:
for X being Subset of E, x being set st x in X
holds x in E
proof let X be Subset of E, x be set such that
A1: x in X;
X in bool E by Def2;
then X c= E by ZFMISC_1:def 1;
hence x in E by A1,TARSKI:def 3;
end;
definition let E;
cluster empty Subset of E;
existence
proof
{} c= E by XBOOLE_1:2;
then {} in bool E by ZFMISC_1:def 1;
then {} is Subset of E by Def2;
hence thesis;
end;
end;
definition let E;
func {} E -> empty Subset of E equals
{};
coherence
proof
{} c= E by XBOOLE_1:2;
then {} in bool E by ZFMISC_1:def 1;
hence thesis by Def2;
end;
correctness;
func [#] E -> Subset of E equals :Def4: E;
coherence
proof
E in bool E by ZFMISC_1:def 1;
hence E is Subset of E by Def2;
end;
correctness;
end;
canceled 3;
theorem
{} is Subset of X
proof
{}X = {};
hence {} is Subset of X;
end;
reserve A,B,C for Subset of E;
canceled 2;
theorem
Th7: (for x being Element of E holds x in A implies x in B) implies A c= B
proof
assume A1: for x being Element of E holds x in A implies x in B;
let x be set;
assume A2: x in A;
then x in E by Lm1;
then x is Element of E by Def2;
hence thesis by A1,A2;
end;
theorem Th8:
(for x being Element of E holds x in A iff x in B) implies A = B
proof
assume for x being Element of E holds x in A iff x in B;
hence A c= B & B c= A by Th7;
end;
canceled;
theorem
A <> {} implies ex x being Element of E st x in A
proof
assume A <> {};
then consider x being set such that
A1: x in A by XBOOLE_0:def 1;
x in E by A1,Lm1;
then x is Element of E by Def2;
hence thesis by A1;
end;
definition let E,A;
func A` -> Subset of E equals :Def5: E \ A;
coherence
proof
E \ A c= E by XBOOLE_1:36;
then E \ A in bool E by ZFMISC_1:def 1;
hence thesis by Def2;
end;
correctness;
involutiveness
proof let S,T be Subset of E;
assume
A1: S = E \ T;
T in bool E by Def2;
then T c= E by ZFMISC_1:def 1;
hence T = {} \/ E /\ T by XBOOLE_1:28
.= (E \ E) \/ E /\ T by XBOOLE_1:37
.= E \ S by A1,XBOOLE_1:52;
end;
let B;
redefine func A \/ B -> Subset of E;
coherence
proof
A in bool E & B in bool E by Def2;
then A c= E & B c= E by ZFMISC_1:def 1;
then A \/ B c= E by XBOOLE_1:8;
then A \/ B in bool E by ZFMISC_1:def 1;
hence thesis by Def2;
end;
func A /\ B -> Subset of E;
coherence
proof
A2: A in bool E by Def2;
A3: A /\ B c= A by XBOOLE_1:17;
A c= E by A2,ZFMISC_1:def 1;
then A /\ B c= E by A3,XBOOLE_1:1;
then A /\ B in bool E by ZFMISC_1:def 1;
hence A /\ B is Subset of E by Def2;
end;
func A \ B -> Subset of E;
coherence
proof
A4: A in bool E by Def2;
A5: A \ B c= A by XBOOLE_1:36;
A c= E by A4,ZFMISC_1:def 1;
then A \ B c= E by A5,XBOOLE_1:1;
then A \ B in bool E by ZFMISC_1:def 1;
hence A \ B is Subset of E by Def2;
end;
func A \+\ B -> Subset of E;
coherence
proof
A6: A in bool E & B in bool E by Def2;
A7: A \ B c= A & B \ A c= B by XBOOLE_1:36;
A c= E & B c= E by A6,ZFMISC_1:def 1;
then A \ B c= E & B \ A c= E by A7,XBOOLE_1:1;
then (A \ B) \/ (B \ A) c= E by XBOOLE_1:8;
then A \+\ B c= E by XBOOLE_0:def 6;
then A \+\ B in bool E by ZFMISC_1:def 1;
hence A \+\ B is Subset of E by Def2;
end;
end;
canceled 4;
theorem
(for x being Element of E holds x in A iff x in B or x in C)
implies A = B \/ C
proof
assume A1: for x being Element of E holds x in A iff x in B or x in C;
now
let x be Element of E;
assume x in A;
then x in B or x in C by A1;
hence x in B \/ C by XBOOLE_0:def 2;
end;
hence A c= B \/ C by Th7;
now
let x be Element of E;
assume x in B \/ C;
then x in B or x in C by XBOOLE_0:def 2;
hence x in A by A1;
end;
hence thesis by Th7;
end;
theorem
(for x being Element of E holds x in A iff x in B & x in C)
implies A = B /\ C
proof
assume A1: for x being Element of E holds x in A iff x in B & x in C;
now
let x be Element of E;
assume x in A;
then x in B & x in C by A1;
hence x in B /\ C by XBOOLE_0:def 3;
end;
hence A c= B /\ C by Th7;
now
let x be Element of E;
assume x in B /\ C;
then x in B & x in C by XBOOLE_0:def 3;
hence x in A by A1;
end;
hence thesis by Th7;
end;
theorem
(for x being Element of E holds x in A iff x in B & not x in C)
implies A = B \ C
proof
assume A1: for x being Element of E holds x in A iff x in B & not x in C;
now
let x be Element of E;
assume x in A;
then x in B & not x in C by A1;
hence x in B \ C by XBOOLE_0:def 4;
end;
hence A c= B \ C by Th7;
now
let x be Element of E;
assume x in B \ C;
then x in B & not x in C by XBOOLE_0:def 4;
hence x in A by A1;
end;
hence B \ C c= A by Th7;
end;
theorem
(for x being Element of E holds x in A iff not(x in B iff x in C))
implies A = B \+\ C
proof
assume A1: for x being Element of E holds x in A iff not(x in B iff x in C);
now
let x be Element of E;
assume x in A;
then x in B & not x in C or x in C & not x in B by A1;
then x in B \ C or x in C \ B by XBOOLE_0:def 4;
then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 2;
hence x in B \+\ C by XBOOLE_0:def 6;
end;
hence A c= B \+\ C by Th7;
now
let x be Element of E;
assume x in B \+\ C;
then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 6;
then x in B \ C or x in C \ B by XBOOLE_0:def 2;
then x in B & not x in C or x in C & not x in B by XBOOLE_0:def 4;
hence x in A by A1;
end;
hence thesis by Th7;
end;
canceled 2;
theorem
Th21: {} E = ([#] E)`
proof
thus ([#]E)` = E \ [#]E by Def5
.= E \ E by Def4
.= {}E by XBOOLE_1:37;
end;
theorem
Th22: [#] E = ({} E)`
proof
thus [#]E = E \ {} by Def4
.= ({}E)` by Def5;
end;
canceled 2;
theorem
Th25: A \/ A` = [#]E
proof
A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
thus A \/ A` = A \/ (E \ A) by Def5
.= E by A1,XBOOLE_1:45
.= [#] E by Def4;
end;
theorem Th26:
A misses A`
proof
A1:A misses (E \ A) by XBOOLE_1:79;
A /\ A` = A /\ (E \ A) by Def5
.= {} by A1,XBOOLE_0:def 7;
hence thesis by XBOOLE_0:def 7;
end;
canceled;
theorem
A \/ [#]E = [#]E
proof
A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
thus A \/ [#]E = A \/ E by Def4
.= E by A1,XBOOLE_1:12
.= [#]E by Def4;
end;
theorem
(A \/ B)` = A` /\ B`
proof
thus (A \/ B)` = E \ (A \/ B) by Def5
.= (E \ A) /\ (E \ B) by XBOOLE_1:53
.= A` /\ (E \ B) by Def5
.= A` /\ B` by Def5;
end;
theorem
(A /\ B)` = A` \/ B`
proof
thus (A /\ B)` = E \ (A /\ B) by Def5
.= (E \ A) \/ (E \ B) by XBOOLE_1:54
.= A` \/ (E \ B) by Def5
.= A` \/ B` by Def5;
end;
theorem
Th31: A c= B iff B` c= A`
proof
E \ A = A` & E \ B = B` by Def5;
hence A c= B implies B` c= A` by XBOOLE_1:34;
A1: E \ A` = A`` by Def5 .= A;
E \ B` = B`` by Def5 .= B;
hence thesis by A1,XBOOLE_1:34;
end;
theorem
A \ B = A /\ B`
proof
A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
thus A /\ B` = A /\ (E \ B) by Def5
.= (A /\ E) \ B by XBOOLE_1:49
.= A \ B by A1,XBOOLE_1:28;
end;
theorem
(A \ B)` = A` \/ B
proof
A in bool E & B in bool E by Def2;
then A1: A c= E & B c= E by ZFMISC_1:def 1;
thus (A \ B)` = E \ (A \ B) by Def5
.= (E \ A) \/ E /\ B by XBOOLE_1:52
.= A` \/ E /\ B by Def5
.= A` \/ B by A1,XBOOLE_1:28;
end;
theorem
(A \+\ B)` = A /\ B \/ A` /\ B`
proof
A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
thus (A \+\ B)` = E \ (A \+\ B) by Def5
.= E \ (A \/ B) \/ E /\ A /\ B by XBOOLE_1:102
.= A /\ B \/ (E \ (A \/ B)) by A1,XBOOLE_1:28
.= A /\ B \/ (E \ A) /\ (E \ B) by XBOOLE_1:53
.= A /\ B \/ A` /\ (E \ B) by Def5
.= A /\ B \/ (A`) /\ (B`) by Def5;
end;
theorem
A c= B` implies B c= A`
proof
assume A c= B`;
then B``c= A` by Th31;
hence thesis;
end;
theorem
A` c= B implies B` c= A
proof
assume A` c= B;
then B` c= A`` by Th31;
hence thesis;
end;
canceled;
theorem
A c= A` iff A = {}E
proof
thus A c= A` implies A = {}E
proof
assume A c= A`;
then A c= E \ A by Def5;
hence thesis by XBOOLE_1:38;
end;
A1: A in bool E by Def2;
assume A = {}E;
then A` = [#]E by Th22 .= E by Def4;
hence A c= A` by A1,ZFMISC_1:def 1;
end;
theorem
A` c= A iff A = [#]E
proof
thus A` c= A implies A = [#]E
proof
assume A` c= A;
hence A = A \/ A` by XBOOLE_1:12
.= [#]E by Th25;
end;
assume A = [#]E;
then A` = {}E by Th21 .= {};
hence A` c= A by XBOOLE_1:2;
end;
theorem
X c= A & X c= A` implies X = {}
proof
A misses A` by Th26;
hence thesis by XBOOLE_1:67;
end;
theorem
(A \/ B)` c= A`
proof
A c= A \/ B by XBOOLE_1:7;
hence thesis by Th31;
end;
theorem
A` c= (A /\ B)`
proof
A /\ B c= A by XBOOLE_1:17;
hence thesis by Th31;
end;
theorem
Th43: A misses B iff A c= B`
proof
thus A misses B implies A c= B`
proof
assume
A1: A misses B;
let x;
assume A2: x in A;
then A3: x in E by Lm1;
not x in B by A1,A2,XBOOLE_0:3;
then x in E \ B by A3,XBOOLE_0:def 4;
hence x in B` by Def5;
end;
assume A4: A c= B`;
assume A meets B;
then consider x such that
A5: x in A & x in B by XBOOLE_0:3;
A c= E \ B by A4,Def5;
then x in E \ B by A5,TARSKI:def 3;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem
A misses B` iff A c= B
proof
B``= B;
hence thesis by Th43;
end;
canceled;
theorem
A misses B & A` misses B` implies A = B`
proof
A1: A in bool E by Def2;
assume that A2: A misses B and
A3: A` misses B`;
thus A c= B`
proof
let x;
assume A4: x in A;
A c= E by A1,ZFMISC_1:def 1;
then A5: x in E by A4,TARSKI:def 3;
not x in B by A2,A4,XBOOLE_0:3;
then x in E \ B by A5,XBOOLE_0:def 4;
hence thesis by Def5;
end;
let x;
assume x in B`;
then x in E \ B by Def5;
then A6: x in E & not x in B by XBOOLE_0:def 4;
x in A` implies not x in B` by A3,XBOOLE_0:3;
then x in E \ A implies not x in E \ B by Def5;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem
A c= B & C misses B implies A c= C`
proof
assume A c= B & C misses B;
then A misses C by XBOOLE_1:63;
hence thesis by Th43;
end;
::
:: ADDITIONAL THEOREMS
::
theorem
(for a being Element of A holds a in B) implies A c= B
proof
assume A1: for a being Element of A holds a in B;
let a be set;
assume
a in A;
then a is Element of A by Def2;
hence thesis by A1;
end;
theorem
(for x being Element of E holds x in A) implies E = A
proof
assume A1: for x being Element of E holds x in A;
thus E c= A
proof
let a be set;
assume
a in E;
then a is Element of E by Def2;
hence thesis by A1;
end;
A in bool E by Def2;
hence A c= E by ZFMISC_1:def 1;
end;
theorem
E <> {} implies for B for x being Element of E st not x in B holds x in B`
proof
assume
A1: E <> {};
let B be Subset of E;
let x be Element of E;
assume
A2: not x in B;
x in E by A1,Def2;
then x in E \ B by A2,XBOOLE_0:def 4;
hence x in B` by Def5;
end;
theorem Th51:
for A,B st for x being Element of E holds x in A iff not x in B
holds A = B`
proof
let A,B be Subset of E;
assume A1: for x being Element of E holds x in A iff not x in B;
thus A c= B`
proof
let x be set;
assume A2: x in A;
A in bool E by Def2;
then A c= E by ZFMISC_1:def 1;
then x in E by A2,TARSKI:def 3;
then x is Element of E by Def2;
then x in E & not x in B by A1,A2,Lm1;
then x in E \ B by XBOOLE_0:def 4;
hence thesis by Def5;
end;
let x be set;
A3: B` in bool E by Def2;
assume A4: x in B`;
B` c= E by A3,ZFMISC_1:def 1;
then x in E by A4,TARSKI:def 3;
then reconsider x as Element of E by Def2;
x in E \ B by A4,Def5;
then not x in B by XBOOLE_0:def 4;
hence thesis by A1;
end;
theorem
for A,B st for x being Element of E holds not x in A iff x in B
holds A = B`
proof
let A,B;
assume for x being Element of E holds not x in A iff x in B;
then for x being Element of E holds x in A iff not x in B;
hence A = B` by Th51;
end;
theorem
for A,B st for x being Element of E holds not(x in A iff x in B)
holds A = B`
proof let A,B;
assume for x being Element of E holds not(x in A iff x in B);
then for x being Element of E holds x in A iff not x in B;
hence A = B` by Th51;
end;
theorem
x in A` implies not x in A
proof
assume x in A`;
then x in E \ A by Def5;
hence thesis by XBOOLE_0:def 4;
end;
reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X;
theorem
X <> {} implies {x1} is Subset of X
proof assume
X <> {};
then A1: x1 in X by Def2;
{x1} c= X
proof
let x;
assume x in {x1};
hence x in X by A1,TARSKI:def 1;
end;
then {x1} in bool X by ZFMISC_1:def 1;
hence {x1} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X by Def2;
{x1,x2} c= X
proof
let x;
assume x in {x1,x2};
hence x in X by A1,TARSKI:def 2;
end;
then {x1,x2} in bool X by ZFMISC_1:def 1;
hence {x1,x2} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X & x3 in X by Def2;
{x1,x2,x3} c= X
proof
let x;
assume x in {x1,x2,x3};
hence x in X by A1,ENUMSET1:def 1;
end;
then {x1,x2,x3} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3,x4} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X & x3 in X & x4 in X by Def2;
{x1,x2,x3,x4} c= X
proof
let x;
assume x in {x1,x2,x3,x4};
hence x in X by A1,ENUMSET1:18;
end;
then {x1,x2,x3,x4} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5} is Subset of X
proof assume
A1: X <> {};
{x1,x2,x3,x4,x5} c= X
proof
let x;
assume
A2: x in {x1,x2,x3,x4,x5};
x in { x1,x2,x3,x4,x5 } implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5
by ENUMSET1:23;
hence x in X by A1,A2,Def2;
end;
then {x1,x2,x3,x4,x5} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4,x5} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X
proof assume
A1: X <> {};
{x1,x2,x3,x4,x5,x6} c= X
proof
let x;
assume A2: x in {x1,x2,x3,x4,x5,x6};
x in { x1,x2,x3,x4,x5,x6} implies
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 by ENUMSET1:28;
hence x in X by A1,A2,Def2;
end;
then {x1,x2,x3,x4,x5,x6} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4,x5,x6} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X
proof assume
A1: X <> {};
{x1,x2,x3,x4,x5,x6,x7} c= X
proof
let x;
assume A2: x in {x1,x2,x3,x4,x5,x6,x7};
x in { x1,x2,x3,x4,x5,x6,x7} implies
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 by ENUMSET1:33;
hence x in X by A1,A2,Def2;
end;
then {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def2;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proof assume
A1: X <> {};
{x1,x2,x3,x4,x5,x6,x7,x8} c= X
proof
let x;
assume A2: x in {x1,x2,x3,x4,x5,x6,x7,x8};
x in { x1,x2,x3,x4,x5,x6,x7,x8} implies
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8
by ENUMSET1:38;
hence x in X by A1,A2,Def2;
end;
then {x1,x2,x3,x4,x5,x6,x7,x8} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X by Def2;
end;
theorem
x in X implies {x} is Subset of X
proof assume x in X;
then {x} c= X by ZFMISC_1:37;
then {x} in bool X by ZFMISC_1:def 1;
hence thesis by Def2;
end;
scheme Subset_Ex { A()-> set, P[set] } :
ex X being Subset of A() st for x holds x in X iff x in A() & P[x]
proof
defpred X[set] means P[$1];
consider X being set such that
A1: for x holds
x in X iff x in A() & X[x] from Separation;
X c= A()
proof
let x;
thus thesis by A1;
end;
then X in bool A() by ZFMISC_1:def 1;
then reconsider X as Subset of A() by Def2;
take X;
thus thesis by A1;
end;
scheme Subset_Eq {X() -> set, P[set]}:
for X1,X2 being Subset of X() st
(for y being Element of X() holds y in X1 iff P[y]) &
(for y being Element of X() holds y in X2 iff P[y]) holds
X1 = X2
proof
let X1,X2 be Subset of X() such that
A1:for y being Element of X() holds y in X1 iff P[y] and
A2:for y being Element of X() holds y in X2 iff P[y];
for x being Element of X() holds x in X1 iff x in X2
proof
let x be Element of X();
hereby assume x in X1;
then P[x] by A1;
hence x in X2 by A2;
end;
assume x in X2;
then P[x] by A2;
hence thesis by A1;
end;
hence thesis by Th8;
end;
definition let X, Y be non empty set;
redefine pred X misses Y;
irreflexivity
proof
let A be non empty set;
consider x being set such that A1: x in A by XBOOLE_0:def 1;
thus thesis by A1,XBOOLE_0:3;
end;
antonym X meets Y;
end;
definition
let S be set; assume
A1: contradiction;
func choose S -> Element of S means
not contradiction;
correctness by A1;
end;