:: Properties of Subsets
:: by Zinaida Trybulec
::
:: Received March 4, 1989
:: Copyright (c) 1990-2026 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 ZFMISC_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
registrations XBOOLE_0, ZFMISC_1;
requirements BOOLE;
definitions TARSKI, XBOOLE_0, ZFMISC_1;
equalities XBOOLE_0, ZFMISC_1;
expansions TARSKI, XBOOLE_0, ZFMISC_1;
theorems XBOOLE_0, TARSKI, ENUMSET1, ZFMISC_1, XBOOLE_1;
schemes XBOOLE_0;
begin
reserve E,X,Y,x for set;
registration
let X be set;
cluster bool X -> non empty;
coherence by ZFMISC_1:def 1;
end;
registration
let x1, x2, x3 be object;
cluster { x1, x2, x3 } -> non empty;
coherence by ENUMSET1:def 1;
let x4 be object;
cluster { x1, x2, x3, x4 } -> non empty;
coherence by ENUMSET1:def 2;
let x5 be object;
cluster { x1, x2, x3, x4, x5 } -> non empty;
coherence by ENUMSET1:def 3;
let x6 be object;
cluster { x1, x2, x3, x4, x5, x6 } -> non empty;
coherence by ENUMSET1:def 4;
let x7 be object;
cluster { x1, x2, x3, x4, x5, x6, x7 } -> non empty;
coherence by ENUMSET1:def 5;
let x8 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8 } -> non empty;
coherence by ENUMSET1:def 6;
let x9 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9 } -> non empty;
coherence by ENUMSET1:def 7;
let x10 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 } -> non empty;
coherence by ENUMSET1:def 8;
end;
definition
let X;
mode Element of X -> set means :Def1:
it in X if X is non empty otherwise it is empty;
existence
proof
thus X is non empty implies ex Y being set st Y in X
proof assume X is non empty;
then consider Y being object such that
A1: Y in X;
reconsider Y as set by TARSKI:1;
take Y;
thus thesis by A1;
end;
thus thesis;
end;
consistency;
sethood
proof
per cases;
case X is non empty;
take X;
thus thesis;
end;
case X is empty;
take {{}};
let y be set;
thus thesis by TARSKI:def 1;
end;
end;
end;
definition
let X;
mode Subset of X is Element of bool X;
end;
registration
let X be non empty set;
cluster non empty for Subset of X;
existence
proof
X in bool X by ZFMISC_1:def 1;
then X is Subset of X by Def1;
hence thesis;
end;
end;
registration
let X1,X2 be non empty set;
cluster [: X1,X2 :] -> non empty;
coherence
proof
consider x2 being object such that
A1: x2 in X2 by XBOOLE_0:def 1;
consider x1 being object such that
A2: x1 in X1 by XBOOLE_0:def 1;
[x1,x2] in [:X1,X2:] by A2,A1,ZFMISC_1:def 2;
hence thesis;
end;
end;
registration
let X1,X2,X3 be non empty set;
cluster [: X1,X2,X3 :] -> non empty;
coherence;
end;
registration
let X1,X2,X3,X4 be non empty set;
cluster [: X1,X2,X3,X4 :] -> non empty;
coherence;
end;
definition
let D be non empty set, X be non empty Subset of D;
redefine mode Element of X -> Element of D; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of X;
X in bool D by Def1;
then
A1: X c= D by ZFMISC_1:def 1;
x in X by Def1;
then x in D by A1;
hence thesis by Def1;
end;
end;
Lm1: for X being Subset of E, x being object st x in X holds x in E
proof
let X be Subset of E, x be object such that
A1: x in X;
X in bool E by Def1;
then X c= E by ZFMISC_1:def 1;
hence thesis by A1;
end;
registration
let E;
cluster empty for Subset of E;
existence
proof
{} c= E;
then {} in bool E by ZFMISC_1:def 1;
then {} is Subset of E by Def1;
hence thesis;
end;
end;
definition
let E;
func {}E -> Subset of E equals
{};
coherence
proof
{} c= E;
then {} in bool E by ZFMISC_1:def 1;
hence thesis by Def1;
end;
correctness;
func [#] E -> Subset of E equals
E;
coherence
proof
E in bool E by ZFMISC_1:def 1;
hence thesis by Def1;
end;
correctness;
end;
registration
let E;
cluster {}E -> empty;
coherence;
end;
theorem
{} is Subset of X
proof
{}X = {};
hence thesis;
end;
reserve A,B,C for Subset of E;
theorem Th2:
(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 object;
assume
A2: x in A;
reconsider x as set by TARSKI:1;
x in E by Lm1,A2;
then x is Element of E by Def1;
hence thesis by A1,A2;
end;
theorem
(for x being Element of E holds x in A iff x in B) implies A = B by Th2;
theorem Th4:
A <> {} implies ex x being Element of E st x in A
proof
assume A <> {};
then consider x being object such that
A1: x in A by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
x in E by A1,Lm1;
then x is Element of E by Def1;
hence thesis by A1;
end;
definition
let E,A;
func A` -> Subset of E equals
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 Def1;
end;
correctness;
involutiveness
proof
let S,T be Subset of E;
assume
A1: S = E \ T;
T in bool E by Def1;
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; :: redefines \/ (XBOOLE_0, definition)
coherence
proof
B in bool E by Def1;
then
A2: B c= E by ZFMISC_1:def 1;
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
then A \/ B c= E by A2,XBOOLE_1:8;
then A \/ B in bool E by ZFMISC_1:def 1;
hence thesis by Def1;
end;
redefine func A \+\ B -> Subset of E; :: redefines \+\ (XBOOLE_0, definition)
coherence
proof
B in bool E by Def1;
then B \ A c= B & B c= E by XBOOLE_1:36,ZFMISC_1:def 1;
then
A3: B \ A c= E;
A in bool E by Def1;
then A \ B c= A & A c= E by XBOOLE_1:36,ZFMISC_1:def 1;
then A \ B c= E;
then (A \ B) \/ (B \ A) c= E by A3,XBOOLE_1:8;
then A \+\ B in bool E by ZFMISC_1:def 1;
hence thesis by Def1;
end;
end;
definition
let X,Y be set;
redefine func X \ Y -> Subset of X; :: redefines \ (XBOOLE_0, definition)
coherence
proof
X \ Y c= X by XBOOLE_1:36;
then X \ Y in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
end;
definition
let E,A,X;
redefine func A \ X -> Subset of E; :: redefines \ (XBOOLE_0, definition)
coherence
proof
A in bool E by Def1;
then A \ X c= A & A c= E by XBOOLE_1:36,ZFMISC_1:def 1;
then A \ X c= E;
then A \ X in bool E by ZFMISC_1:def 1;
hence A \ X is Subset of E by Def1;
end;
end;
definition
let E,A,X;
redefine func A /\ X -> Subset of E; :: redefines /\ (XBOOLE_0, definition)
coherence
proof
A in bool E by Def1;
then A /\ X c= A & A c= E by XBOOLE_1:17,ZFMISC_1:def 1;
then A /\ X c= E;
then A /\ X in bool E by ZFMISC_1:def 1;
hence thesis by Def1;
end;
end;
definition
let E,X,A;
redefine func X /\ A -> Subset of E; :: redefines /\ (XBOOLE_0, definition)
coherence
proof
A /\ X is Subset of E;
hence thesis;
end;
end;
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 3;
end;
hence A c= B \/ C by Th2;
now
let x be Element of E;
assume x in B \/ C;
then x in B or x in C by XBOOLE_0:def 3;
hence x in A by A1;
end;
hence thesis by Th2;
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 4;
end;
hence A c= B /\ C by Th2;
now
let x be Element of E;
assume x in B /\ C;
then x in B & x in C by XBOOLE_0:def 4;
hence x in A by A1;
end;
hence thesis by Th2;
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 5;
end;
hence A c= B \ C by Th2;
now
let x be Element of E;
assume x in B \ C;
then x in B & not x in C by XBOOLE_0:def 5;
hence x in A by A1;
end;
hence thesis by Th2;
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 5;
hence x in B \+\ C by XBOOLE_0:def 3;
end;
hence A c= B \+\ C by Th2;
now
let x be Element of E;
assume x in B \+\ C;
then x in B \ C or x in C \ B by XBOOLE_0:def 3;
then x in B & not x in C or x in C & not x in B by XBOOLE_0:def 5;
hence x in A by A1;
end;
hence thesis by Th2;
end;
theorem
[#] E = ({} E)`;
theorem Th10:
A \/ A` = [#]E
proof
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
hence thesis by XBOOLE_1:45;
end;
theorem
A \/ [#]E = [#]E
proof
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
hence thesis by XBOOLE_1:12;
end;
theorem Th12:
A c= B iff B` c= A`
proof
thus A c= B implies B` c= A` by XBOOLE_1:34;
A1: E \ B` = B`` .= B;
E \ A` = A`` .= A;
hence thesis by A1,XBOOLE_1:34;
end;
theorem
A \ B = A /\ B`
proof
A in bool E by Def1;
then
A1: A c= E by ZFMISC_1:def 1;
thus A /\ B` = (A /\ E) \ B by XBOOLE_1:49
.= A \ B by A1,XBOOLE_1:28;
end;
theorem
(A \ B)` = A` \/ B
proof
B in bool E by Def1;
then
A1: B c= E by ZFMISC_1:def 1;
thus (A \ B)` = (E \ A) \/ E /\ B by XBOOLE_1:52
.= A` \/ B by A1,XBOOLE_1:28;
end;
theorem
(A \+\ B)` = A /\ B \/ A` /\ B`
proof
A in bool E by Def1;
then
A1: A c= E by ZFMISC_1:def 1;
thus (A \+\ B)` = E \ (A \/ B) \/ E /\ A /\ B by XBOOLE_1:102
.= A /\ B \/ (E \ (A \/ B)) by A1,XBOOLE_1:28
.= A /\ B \/ (A`) /\ (B`) by XBOOLE_1:53;
end;
theorem
A c= B` implies B c= A`
proof
assume A c= B`;
then B``c= A` by Th12;
hence thesis;
end;
theorem
A` c= B implies B` c= A
proof
assume A` c= B;
then B` c= A`` by Th12;
hence thesis;
end;
theorem
A c= A` iff A = {}E
by XBOOLE_1:38;
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 Th10;
end;
thus thesis by XBOOLE_1:37;
end;
theorem
X c= A & X c= A` implies X = {} by XBOOLE_1:67,79;
theorem
(A \/ B)` c= A` by Th12,XBOOLE_1:7;
theorem
A` c= (A /\ B)` by Th12,XBOOLE_1:17;
theorem Th23:
A misses B iff A c= B`
proof
thus A misses B implies A c= B`
proof
assume
A1: A misses B;
let x be object;
assume
A2: x in A;
then
A3: not x in B by A1,XBOOLE_0:3;
x in E by A2,Lm1;
hence thesis by A3,XBOOLE_0:def 5;
end;
assume
A4: A c= B`;
assume A meets B;
then consider x being object such that
A5: x in A and
A6: x in B by XBOOLE_0:3;
x in E \ B by A4,A5;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem
A misses B` iff A c= B
proof
B``= B;
hence thesis by Th23;
end;
theorem
A misses B & A` misses B` implies A = B`
proof
assume that
A1: A misses B and
A2: A` misses B`;
A3: A in bool E by Def1;
thus A c= B`
proof
let x be object;
assume
A4: x in A;
then
A5: not x in B by A1,XBOOLE_0:3;
A c= E by A3,ZFMISC_1:def 1;
then x in E by A4;
hence thesis by A5,XBOOLE_0:def 5;
end;
let x be object;
A6: x in A` implies not x in B` by A2,XBOOLE_0:3;
assume
A7: x in B`;
then x in E by XBOOLE_0:def 5;
hence thesis by A7,A6,XBOOLE_0:def 5;
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 Th23;
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 object;
assume
A2: a in A;
reconsider a as set by TARSKI:1;
a is Element of A by Def1,A2;
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 object;
assume
A2: a in E;
reconsider a as set by TARSKI:1;
a is Element of E by Def1,A2;
hence thesis by A1;
end;
A in bool E by Def1;
hence thesis 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,Def1;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem Th30:
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 object;
assume
A2: x in A;
reconsider x as set by TARSKI:1;
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
then x in E by A2;
then x is Element of E by Def1;
then
A3: not x in B by A1,A2;
x in E by A2,Lm1;
hence thesis by A3,XBOOLE_0:def 5;
end;
let x be object;
assume
A4: x in B`;
reconsider x as set by TARSKI:1;
B` in bool E by Def1;
then B` c= E by ZFMISC_1:def 1;
then x in E by A4;
then reconsider x as Element of E by Def1;
not x in B by A4,XBOOLE_0:def 5;
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 thesis by Th30;
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 thesis by Th30;
end;
reserve x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 for Element of X;
theorem
X <> {} implies {x1} is Subset of X
proof
assume X <> {};
then
A1: x1 in X by Def1;
{x1} c= X by A1,TARSKI:def 1;
then {x1} in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2} is Subset of X
proof
assume X <> {};
then
A1: x1 in X & x2 in X by Def1;
{x1,x2} c= X by A1,TARSKI:def 2;
then {x1,x2} in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3} is Subset of X
proof
set A = {x1,x2,x3};
assume
A1: X <> {};
then
A2: x3 in X by Def1;
x1 in X & x2 in X by A1,Def1;
then A c= X by A2,ENUMSET1:def 1;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4} is Subset of X
proof
set A = {x1,x2,x3,x4};
assume
A1: X <> {};
then
A2: x3 in X & x4 in X by Def1;
x1 in X & x2 in X by A1,Def1;
then A c= X by A2,ENUMSET1:def 2;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5} is Subset of X
proof
set A = {x1,x2,x3,x4,x5};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 by ENUMSET1:def 3;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X
proof
set A = {x1,x2,x3,x4,x5,x6};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6
by ENUMSET1:def 4;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X
proof
set A = {x1,x2,x3,x4,x5,x6,x7};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7
by ENUMSET1:def 5;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proof
set A = {x1,x2,x3,x4,x5,x6,x7,x8};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A 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:def 6;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
x in X implies {x} is Subset of X
proof
assume x in X;
then {x} c= X by ZFMISC_1:31;
then {x} in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
scheme
SubsetEx { A()-> set, P[object] } :
ex X being Subset of A() st for x holds x
in X iff x in A() & P[x];
consider X being set such that
A1: for x being object holds x in X iff x in A() & P[x] from XBOOLE_0:sch 1;
X c= A()
by A1;
then X in bool A() by ZFMISC_1:def 1;
then reconsider X as Subset of A() by Def1;
take X;
thus thesis by A1;
end;
scheme
SubsetEq {X() -> set, X1,X2()-> Subset of X(), P[set]}: X1() = X2()
provided
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]
proof
for x being Element of X() holds x in X1() iff x in X2() by A1,A2;
hence thesis by Th2;
end;
definition
let X, Y be non empty set;
redefine pred X misses Y; :: redefines misses (XBOOLE_0, definition)
irreflexivity;
end;
definition
let X, Y be non empty set;
redefine pred X meets Y; :: redefines meets (XBOOLE_0, antonym) → misses (XBOOLE_0, definition)
reflexivity;
end;
definition
::$CD
end;
begin :: Addenda
Lm2: (for x being object st x in X holds x in Y)
implies X is Subset of Y
proof
assume for x being object st x in X holds x in Y;
then X c= Y;
then X in bool Y by ZFMISC_1:def 1;
hence thesis by Def1;
end;
Lm3: for x being object holds x in A implies x is Element of E
proof let x be object;
assume
A1: x in A;
reconsider x as set by TARSKI:1;
x in E by Lm1,A1;
hence thesis by Def1;
end;
:: from SETWISEO, 2005.6.11 , A.T.
scheme
SubsetEx { A() -> non empty set, P[object] } :
ex B being Subset of A() st for
x being Element of A() holds x in B iff P[x];
consider B being set such that
A1: for x being object holds x in B iff x in A() & P[x] from XBOOLE_0:sch 1;
for x being object holds x in B implies x in A() by A1;
then reconsider B as Subset of A() by Lm2;
take B;
let x be Element of A();
x in A() by Def1;
hence thesis by A1;
end;
:: from GROUP_2, 2005.6.14 , A.T.
scheme
SubComp{A() -> set, F1,F2() -> Subset of A(), P[set]}: F1() = F2()
provided
A1: for X being Element of A() holds X in F1() iff P[X] and
A2: for X being Element of A() holds X in F2() iff P[X]
proof
thus F1() c= F2()
proof
let x be object;
assume
A3: x in F1();
then reconsider X = x as Element of A() by Lm3;
P[X] by A1,A3;
hence thesis by A2;
end;
let x be object;
assume
A4: x in F2();
then reconsider X = x as Element of A() by Lm3;
P[X] by A2,A4;
hence thesis by A1;
end;
:: from FIN_TOPO, 2006.11.07. A.T.
theorem
A` = B` implies A = B
proof
assume A` = B`;
hence A = B`` .= B;
end;
:: from SGRAPH1, 2008.06.02
registration
let X be empty set;
cluster -> empty for Subset of X;
coherence
proof
let Y be Subset of X;
Y in bool X by Def1;
then Y c= X by ZFMISC_1:def 1;
hence thesis;
end;
end;
:: from TEX_2, 2006.06.18, A.T. (simplified)
definition
let E be set;
let A be Subset of E;
attr A is proper means
A <> E;
end;
registration
let E be set;
cluster [#]E -> non proper;
coherence;
end;
registration
let E be set;
cluster non proper for Subset of E;
existence
proof
take [#]E;
thus thesis;
end;
end;
registration
let E be non empty set;
cluster non proper -> non empty for Subset of E;
coherence;
cluster empty -> proper for Subset of E;
coherence;
end;
registration
let E be non empty set;
cluster proper for Subset of E;
existence
proof
take {} E;
thus {} E <> E;
end;
end;
registration
let E be empty set;
cluster -> non proper for Subset of E;
coherence;
end;
:: from GRCAT_1, 2010.02.18, A.T.
theorem
for X,Y,A being set, z being set st z in A & A c= [:X,Y:] ex x
being Element of X, y being Element of Y st z = [x,y]
proof
let X,Y,A be set, z be set;
assume z in A & A c= [:X,Y:];
then consider x,y being object such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by ZFMISC_1:84;
reconsider x,y as set by TARSKI:1;
reconsider y as Element of Y by A2,Def1;
reconsider x as Element of X by A1,Def1;
take x,y;
thus thesis by A3;
end;
:: from BORSUK_4, 2011.03.04, A.T.
theorem
for X being non empty set, A, B being non empty Subset of X st A c< B
ex p being Element of X st p in B & A c= B \ {p}
proof
let X be non empty set, A, B be non empty Subset of X;
assume
A1: A c< B;
then consider p being Element of X such that
A2: p in B \ A by Th4,XBOOLE_1:105;
A3: not p in A by A2,XBOOLE_0:def 5;
take p;
thus thesis by A1,A2,A3,XBOOLE_0:def 5,ZFMISC_1:34;
end;
definition
let X be set;
redefine attr X is trivial means :: redefines trivial (ZFMISC_1, definition)
for x,y being Element of X holds x = y;
compatibility
proof
thus X is trivial implies for x,y being Element of X holds x = y
proof assume
A1: X is trivial;
let x,y be Element of X;
per cases;
suppose X is non empty;
then x in X & y in X by Def1;
hence x = y by A1;
end;
suppose X is empty;
then x = {} & y = {} by Def1;
hence x = y;
end;
end;
assume
A2: for x,y being Element of X holds x = y;
let x,y be object;
assume
A3: x in X & y in X;
reconsider x,y as set by TARSKI:1;
x is Element of X & y is Element of X by Def1,A3;
hence thesis by A2;
end;
end;
registration let X be non empty set;
cluster non empty trivial for Subset of X;
existence
proof
the Element of X in X by Def1;
then {the Element of X} c= X by ZFMISC_1:31;
then {the Element of X} in bool X by ZFMISC_1:def 1;
then reconsider A = {the Element of X} as Subset of X by Def1;
take A;
thus A is non empty;
let x,y be Element of A;
x in A & y in A by Def1;
then x = the Element of X & y = the Element of X by TARSKI:def 1;
hence thesis;
end;
end;
registration
let X be trivial set;
cluster -> trivial for Subset of X;
coherence
proof
let Y be Subset of X;
let x,y be Element of Y;
per cases;
suppose Y is non empty;
then x in Y & y in Y by Def1;
then x in X & y in X by Lm1;
hence thesis by ZFMISC_1:def 10;
end;
suppose Y is empty;
then x = {} & y = {} by Def1;
hence thesis;
end;
end;
end;
registration
let X be non trivial set;
cluster non trivial for Subset of X;
existence
proof
take [#]X;
thus thesis;
end;
end;
theorem
for D being set, A being Subset of D st A is non trivial
ex d1,d2 being Element of D st d1 in A & d2 in A & d1 <> d2
proof
let D be set, A be Subset of D;
assume A is non trivial;
then consider d1,d2 being object such that
A1: d1 in A & d2 in A and
A2: d1 <> d2;
reconsider d1,d2 as set by TARSKI:1;
d1 in D & d2 in D by A1,Lm1;
then reconsider d1,d2 as Element of D by Def1;
take d1,d2;
thus d1 in A & d2 in A & d1 <> d2 by A1,A2;
end;
theorem Th46:
for X being trivial non empty set
ex x being Element of X st X = {x}
proof let X be trivial non empty set;
consider x being object such that
A1: X = {x} by ZFMISC_1:131;
reconsider x as set by TARSKI:1;
x in X by A1,TARSKI:def 1;
then reconsider x as Element of X by Def1;
take x;
thus X = {x} by A1;
end;
:: from BORSUK_4, 2011.07.31, A.T.
theorem
for X being non empty set, A being non empty Subset of X holds A
is trivial implies ex x being Element of X st A = {x}
proof
let X be non empty set, A be non empty Subset of X;
assume A is trivial;
then ex s being Element of A st A = {s} by Th46;
hence thesis;
end;
theorem
for X be non trivial set, x being Element of X
ex y be object st y in X & x <> y
proof
let X be non trivial set;
let x be Element of X;
consider d1,d2 being object such that
A1: d1 in X & d2 in X and
A2: d1 <> d2 by ZFMISC_1:def 10;
x <> d1 or x <> d2 by A2;
hence thesis by A1;
end;
:: from FUNCT_7, 3.20.2012, A.T.
reserve x for object;
definition
let x,X;
assume
A1: x in X;
func In(x,X) -> Element of X equals
:Def7: x;
correctness
proof
reconsider x as set by TARSKI:1;
x in X by A1;
hence thesis by Def1;
end;
end;
registration
let X be non empty set, x be Element of X;
reduce In(x,X) to x;
reducibility
proof
x in X by Def1;
hence thesis by Def7;
end;
end;
registration
let X,Y be non empty set;
let x be Element of X;
let y be Element of Y;
reduce In([x,y],[:X,Y:]) to [x,y];
reducibility
proof
x in X & y in Y by Def1;
hence thesis by Def7,ZFMISC_1:87;
end;
end;
theorem
x in X /\ Y implies In(x,X) = In(x,Y)
proof
assume
A1: x in X /\ Y;
then
A2: x in Y by XBOOLE_0:def 4;
x in X by A1,XBOOLE_0:def 4;
hence In (x,X) = x by Def7
.= In (x,Y) by A2,Def7;
end;
:: from BORSUK_4, 2012.08.12, A.T.
theorem
for X being non trivial set, p being set ex q being Element of X st q <> p
proof
let X be non trivial set, p be set;
X \ { p } is non empty by ZFMISC_1:139;
then consider q being object such that
A1: q in X \ { p };
reconsider q as set by TARSKI:1;
X \ { p } c= X by XBOOLE_1:36;
then q in X by A1;
then reconsider q as Element of X by Def1;
take q;
thus thesis by A1,ZFMISC_1:56;
end;
theorem
for T being non trivial set, X being non trivial Subset of T,
p being set ex q being Element of T st q in X & q <> p
proof
let T be non trivial set, X be non trivial Subset of T, p be set;
X \ { p } is non empty by ZFMISC_1:139;
then consider q being object such that
A1: q in X \ { p };
reconsider q as set by TARSKI:1;
q in T by A1,Lm1;
then reconsider q as Element of T by Def1;
take q;
thus thesis by A1,ZFMISC_1:56;
end;
:: 2012.12.16, A.T.
scheme Union1 { A()-> set, a()-> Element of A(), F(object) -> set }:
union { F(j) where j is Element of A() : j in {a()}} = F(a())
proof set X = { F(j) where j is Element of A() : j in {a()}};
for x being object holds
x in F(a()) iff ex Y being set st x in Y & Y in X
proof let x be object;
thus x in F(a()) implies ex Y being set st x in Y & Y in X
proof assume
A1: x in F(a());
take F(a());
thus x in F(a()) by A1;
a() in {a()} by TARSKI:def 1;
hence F(a()) in X;
end;
given Y being set such that
A2: x in Y and
A3: Y in X;
ex j being Element of A() st Y = F(j) & j in {a()} by A3;
hence x in F(a()) by A2,TARSKI:def 1;
end;
hence thesis by TARSKI:def 4;
end;
scheme Union2 { A()-> set, a,b()-> Element of A(), F(object) -> set }:
union { F(j) where j is Element of A() : j in {a(),b()}} = F(a()) \/ F(b())
proof set X = { F(j) where j is Element of A() : j in {a(),b()}};
for x being object holds
x in F(a()) \/ F(b()) iff ex Y being set st x in Y & Y in X
proof let x be object;
thus x in F(a()) \/ F(b()) implies ex Y being set st x in Y & Y in X
proof assume x in F(a()) \/ F(b());
then per cases by XBOOLE_0:def 3;
suppose
A1: x in F(a());
take F(a());
thus x in F(a()) by A1;
a() in {a(),b()} by TARSKI:def 2;
hence F(a()) in X;
end;
suppose
A2: x in F(b());
take F(b());
thus x in F(b()) by A2;
b() in {a(),b()} by TARSKI:def 2;
hence F(b()) in X;
end;
end;
given Y being set such that
A3: x in Y and
A4: Y in X;
consider j being Element of A() such that
A5: Y = F(j) and
A6: j in {a(),b()} by A4;
now per cases by A6,TARSKI:def 2;
case j = a();
hence x in F(a()) by A3,A5;
end;
case j = b();
hence x in F(b()) by A3,A5;
end;
end;
hence x in F(a()) \/ F(b()) by XBOOLE_0:def 3;
end;
hence thesis by TARSKI:def 4;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8,x9} is Subset of X
proof
set A = {x1,x2,x3,x4,x5,x6,x7,x8,x9};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or
x=x8 or x=x9 by ENUMSET1:def 7;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;
theorem
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is Subset of X
proof
set A = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10};
assume
A1: X <> {};
A c= X
proof
let x be object;
x in A implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or
x=x8 or x=x9 or x=x10 by ENUMSET1:def 8;
hence thesis by A1,Def1;
end;
then A in bool X by ZFMISC_1:def 1;
hence thesis by Def1;
end;