:: Properties of Subsets
:: by Zinaida Trybulec
::
:: Received March 4, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

registration
let X be set ;
cluster bool X ->  non empty ;
coherence
 not bool X is empty by ZFMISC_1:def_1;
end;

registration
let x1, x2, x3 be set ;
cluster{x1,x2,x3} ->  non empty ;
coherence
 not {x1,x2,x3} is empty by ENUMSET1:def_1;
let x4 be set ;
cluster{x1,x2,x3,x4} ->  non empty ;
coherence
 not {x1,x2,x3,x4} is empty by ENUMSET1:def_2;
let x5 be set ;
cluster{x1,x2,x3,x4,x5} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def_3;
let x6 be set ;
cluster{x1,x2,x3,x4,x5,x6} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def_4;
let x7 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def_5;
let x8 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def_6;
let x9 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def_7;
let x10 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def_8;
end;

definition
let X be set ;
mode Element of X ->  set  means :Def1: :: SUBSET_1:def 1
it in X if  not X is empty
otherwise it is empty ;
existence
 ( ( not X is empty implies ex b1 being set st b1 in X ) & ( X is empty implies ex b1 being set st b1 is empty ) ) by XBOOLE_0:def_1;
consistency
 for b1 being set holds verum ;
sethood
 ( ( not X is empty & ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1 ) or ( X is empty & ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1 ) )
proofend;
end;

:: deftheorem Def1 defines Element SUBSET_1:def_1_:_
 for X being set
for b2 being set holds
( ( not X is empty implies ( b2 is Element of X iff b2 in X ) ) & ( X is empty implies ( b2 is Element of X iff b2 is empty ) ) );

definition
let X be set ;
mode Subset of X is Element of bool X;
end;

registration
let X be non empty set ;
cluster non empty for Element of bool X;
existence
 not for b1 being Subset of X holds b1 is empty
proofend;
end;

registration
let X1, X2 be non empty set ;
cluster[:X1,X2:] ->  non empty ;
coherence
 not [:X1,X2:] is empty
proofend;
end;

registration
let X1, X2, X3 be non empty set ;
cluster[:X1,X2,X3:] ->  non empty ;
coherence
 not [:X1,X2,X3:] is empty ;
end;

registration
let X1, X2, X3, X4 be non empty set ;
cluster[:X1,X2,X3,X4:] ->  non empty ;
coherence
 not [:X1,X2,X3,X4:] is empty ;
end;

definition
let D be non empty set ;
let X be non empty Subset of D;
:: original:Element
redefine mode Element of X ->  Element of D;
coherence
 for b1 being Element of X holds b1 is Element of D
proofend;
end;

Lm1:  for E being set
for X being Subset of E
for x being set st x in X holds
x in E
proofend;

registration
let E be set ;
cluster empty for Element of bool E;
existence
 ex b1 being Subset of E st b1 is empty
proofend;
end;

definition
let E be set ;
func {} E ->  Subset of E equals :: SUBSET_1:def 2
 {} ;
coherence
 {} is Subset of E
proofend;
correctness
;
func [#] E ->  Subset of E equals :: SUBSET_1:def 3
E;
coherence
 E is Subset of E
proofend;
correctness
;
end;

:: deftheorem  defines {} SUBSET_1:def_2_:_
 for E being set holds {} E = {} ;

:: deftheorem  defines [#] SUBSET_1:def_3_:_
 for E being set holds [#] E = E;

registration
let E be set ;
cluster {} E ->  empty ;
coherence
 {} E is empty ;
end;

theorem :: SUBSET_1:1
for X being set holds {} is Subset of X
proofend;

theorem Th2: :: SUBSET_1:2
for E being set
for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
proofend;

theorem Th3: :: SUBSET_1:3
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
proofend;

theorem Th4: :: SUBSET_1:4
for E being set
for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
proofend;

definition
let E be set ;
let A be Subset of E;
funcA `  ->  Subset of E equals :: SUBSET_1:def 4
E \ A;
coherence
 E \ A is Subset of E
proofend;
correctness
;
involutiveness
 for b1, b2 being Subset of E st b1 = E \ b2 holds
b2 = E \ b1
proofend;
let B be Subset of E;
:: original:\/
redefine funcA \/ B ->  Subset of E;
coherence
 A \/ B is Subset of E
proofend;
:: original:\+\
redefine funcA \+\ B ->  Subset of E;
coherence
 A \+\ B is Subset of E
proofend;
end;

:: deftheorem  defines ` SUBSET_1:def_4_:_
 for E being set
for A being Subset of E holds A ` = E \ A;

definition
let X, Y be set ;
:: original:\
redefine funcX \ Y ->  Subset of X;
coherence
 X \ Y is Subset of X
proofend;
end;

definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original:\
redefine funcA \ X ->  Subset of E;
coherence
 A \ X is Subset of E
proofend;
end;

definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original:/\
redefine funcA /\ X ->  Subset of E;
coherence
 A /\ X is Subset of E
proofend;
end;

definition
let E, X be set ;
let A be Subset of E;
:: original:/\
redefine funcX /\ A ->  Subset of E;
coherence
 X /\ A is Subset of E
proofend;
end;

theorem :: SUBSET_1:5
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) holds
A = B \/ C
proofend;

theorem :: SUBSET_1:6
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B &amp; x in C ) ) ) holds
A = B /\ C
proofend;

theorem :: SUBSET_1:7
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B &amp; not x in C ) ) ) holds
A = B \ C
proofend;

theorem :: SUBSET_1:8
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B &amp; not x in C ) or ( x in C &amp; not x in B ) ) ) ) holds
A = B \+\ C
proofend;

theorem :: SUBSET_1:9
for E being set holds [#] E = ({} E) ` ;

theorem Th10: :: SUBSET_1:10
for E being set
for A being Subset of E holds A \/ (A `) = [#] E
proofend;

theorem :: SUBSET_1:11
for E being set
for A being Subset of E holds A \/ ([#] E) = [#] E
proofend;

theorem Th12: :: SUBSET_1:12
for E being set
for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
proofend;

theorem :: SUBSET_1:13
for E being set
for A, B being Subset of E holds A \ B = A /\ (B `)
proofend;

theorem :: SUBSET_1:14
for E being set
for A, B being Subset of E holds (A \ B) ` = (A `) \/ B
proofend;

theorem :: SUBSET_1:15
for E being set
for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
proofend;

theorem :: SUBSET_1:16
for E being set
for A, B being Subset of E st A c= B ` holds
B c= A `
proofend;

theorem :: SUBSET_1:17
for E being set
for A, B being Subset of E st A ` c= B holds
B ` c= A
proofend;

theorem :: SUBSET_1:18
for E being set
for A being Subset of E holds
( A c= A ` iff A = {} E )
proofend;

theorem :: SUBSET_1:19
for E being set
for A being Subset of E holds
( A ` c= A iff A = [#] E )
proofend;

theorem :: SUBSET_1:20
for E, X being set
for A being Subset of E st X c= A &amp; X c= A ` holds
X = {} by XBOOLE_1:67, XBOOLE_1:79;

theorem :: SUBSET_1:21
for E being set
for A, B being Subset of E holds (A \/ B) ` c= A `
proofend;

theorem :: SUBSET_1:22
for E being set
for A, B being Subset of E holds A ` c= (A /\ B) `
proofend;

theorem Th23: :: SUBSET_1:23
for E being set
for A, B being Subset of E holds
( A misses B iff A c= B ` )
proofend;

theorem :: SUBSET_1:24
for E being set
for A, B being Subset of E holds
( A misses B ` iff A c= B )
proofend;

theorem :: SUBSET_1:25
for E being set
for A, B being Subset of E st A misses B &amp; A ` misses B ` holds
A = B `
proofend;

theorem :: SUBSET_1:26
for E being set
for A, B, C being Subset of E st A c= B &amp; C misses B holds
A c= C `
proofend;

::
:: ADDITIONAL THEOREMS
::
theorem :: SUBSET_1:27
for E being set
for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
proofend;

theorem :: SUBSET_1:28
for E being set
for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
proofend;

theorem :: SUBSET_1:29
for E being set st E <> {} holds
for B being Subset of E
for x being Element of E st not x in B holds
x in B `
proofend;

theorem Th30: :: SUBSET_1:30
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
proofend;

theorem :: SUBSET_1:31
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( not x in A iff x in B ) ) holds
A = B `
proofend;

theorem :: SUBSET_1:32
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( ( x in A &amp; not x in B ) or ( x in B &amp; not x in A ) ) ) holds
A = B `
proofend;

theorem :: SUBSET_1:33
for X being set
for x1 being Element of X st X <> {} holds
{x1} is Subset of X
proofend;

theorem :: SUBSET_1:34
for X being set
for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X
proofend;

theorem :: SUBSET_1:35
for X being set
for x1, x2, x3 being Element of X st X <> {} holds
{x1,x2,x3} is Subset of X
proofend;

theorem :: SUBSET_1:36
for X being set
for x1, x2, x3, x4 being Element of X st X <> {} holds
{x1,x2,x3,x4} is Subset of X
proofend;

theorem :: SUBSET_1:37
for X being set
for x1, x2, x3, x4, x5 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5} is Subset of X
proofend;

theorem :: SUBSET_1:38
for X being set
for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6} is Subset of X
proofend;

theorem :: SUBSET_1:39
for X being set
for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
proofend;

theorem :: SUBSET_1:40
for X being set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proofend;

theorem :: SUBSET_1:41
for x, X being set st x in X holds
{x} is Subset of X
proofend;

scheme :: SUBSET_1:sch 1
SubsetEx{ F1() ->  set , P1[ set ] } :
 ex X being Subset of F1() st
for x being set holds
( x in X iff ( x in F1() &amp; P1[x] ) )
proofend;

scheme :: SUBSET_1:sch 2
SubsetEq{ F1() ->  set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), P1[ set ] } :
 F2() = F3()
provided
A1: for y being Element of F1() holds
( y in F2() iff P1[y] ) and
A2: for y being Element of F1() holds
( y in F3() iff P1[y] )
proofend;

definition
let X, Y be non empty set ;
:: original:misses
redefine predX misses Y;
irreflexivity
 for X being non empty set holds R5(b1,b1)
proofend;
end;

definition
let X, Y be non empty set ;
:: original:misses
redefine predX meets Y;
reflexivity
 for X being non empty set holds R5(b1,b1)
proofend;
end;

definition
let S be set ;
func choose S ->  Element of S equals :: SUBSET_1:def 5
 the Element of S;
correctness
coherence
the Element of S is Element of S;
;
end;

:: deftheorem  defines choose SUBSET_1:def_5_:_
 for S being set holds choose S = the Element of S;

begin

Lm2:  for X, Y being set st ( for x being set st x in X holds
x in Y ) holds
X is Subset of Y
proofend;

Lm3:  for x, E being set
for A being Subset of E st x in A holds
x is Element of E
proofend;

scheme :: SUBSET_1:sch 3
SubsetEx{ F1() ->  non empty set , P1[ set ] } :
 ex B being Subset of F1() st
for x being Element of F1() holds
( x in B iff P1[x] )
proofend;

scheme :: SUBSET_1:sch 4
SubComp{ F1() ->  set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), P1[ set ] } :
 F2() = F3()
provided
A1: for X being Element of F1() holds
( X in F2() iff P1[X] ) and
A2: for X being Element of F1() holds
( X in F3() iff P1[X] )
proofend;

:: from FIN_TOPO, 2006.11.07. A.T.
theorem :: SUBSET_1:42
for E being set
for A, B being Subset of E st A ` = B ` holds
A = B
proofend;

:: from SGRAPH1, 2008.06.02
registration
let X be empty set ;
cluster  ->  empty for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is empty
proofend;
end;

:: from TEX_2, 2006.06.18, A.T. (simplified)
definition
let E be set ;
let A be Subset of E;
attrA is proper  means :: SUBSET_1:def 6
A <> E;
end;

:: deftheorem  defines proper SUBSET_1:def_6_:_
 for E being set
for A being Subset of E holds
( A is proper iff A <> E );

registration
let E be set ;
cluster [#] E ->  non proper ;
coherence
 not [#] E is proper
proofend;
end;

registration
let E be set ;
cluster non proper for Element of bool E;
existence
 not for b1 being Subset of E holds b1 is proper
proofend;
end;

registration
let E be non empty set ;
cluster non proper  ->  non empty for Element of bool E;
coherence
 for b1 being Subset of E st not b1 is proper holds
not b1 is empty
proofend;
cluster empty  ->  proper for Element of bool E;
coherence
 for b1 being Subset of E st b1 is empty holds
b1 is proper ;
end;

registration
let E be non empty set ;
cluster proper for Element of bool E;
existence
 ex b1 being Subset of E st b1 is proper
proofend;
end;

registration
let E be empty set ;
cluster  ->  non proper for Element of bool E;
coherence
 for b1 being Subset of E holds not b1 is proper
proofend;
end;

:: from GRCAT_1, 2010.02.18, A.T.
theorem :: SUBSET_1:43
for X, Y, A, z being set st z in A &amp; A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
proofend;

:: from BORSUK_4, 2011.03.04, A.T.
theorem :: SUBSET_1:44
for X being non empty set
for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B &amp; A c= B \ {p} )
proofend;

definition
let X be non empty set ;
redefine attr X is trivial  means :: SUBSET_1:def 7
 for x, y being Element of X holds x = y;
compatibility
 ( X is trivial iff for x, y being Element of X holds x = y )
proofend;
end;

:: deftheorem  defines trivial SUBSET_1:def_7_:_
 for X being non empty set holds
( X is trivial iff for x, y being Element of X holds x = y );

registration
let X be non empty set ;
cluster non empty trivial for Element of bool X;
existence
 ex b1 being Subset of X st
( not b1 is empty &amp; b1 is trivial )
proofend;
end;

registration
let X be trivial set ;
cluster  ->  trivial for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is trivial
proofend;
end;

registration
let X be non trivial set ;
cluster non trivial for Element of bool X;
existence
 not for b1 being Subset of X holds b1 is trivial
proofend;
end;

theorem :: SUBSET_1:45
for D being set
for A being Subset of D st not A is trivial holds
ex d1, d2 being Element of D st
( d1 in A &amp; d2 in A &amp; d1 <> d2 )
proofend;

theorem Th46: :: SUBSET_1:46
for X being non empty trivial set ex x being Element of X st X = {x}
proofend;

:: from BORSUK_4, 2011.07.31, A.T.
theorem :: SUBSET_1:47
for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
proofend;

theorem :: SUBSET_1:48
for X being non trivial set
for x being Element of X ex y being set st
( y in X &amp; x <> y )
proofend;