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

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 object ;

cluster {x1,x2,x3} -> non empty ;

coherence
not {x1,x2,x3} is empty by ENUMSET1:def 1;
let x4 be object ;

cluster {x1,x2,x3,x4} -> non empty ;

coherence
not {x1,x2,x3,x4} is empty by ENUMSET1:def 2;
let x5 be object ;

cluster {x1,x2,x3,x4,x5} -> non empty ;

coherence
not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def 3;
let x6 be object ;

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 object ;

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 object ;

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 object ;

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 object ;

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 b₁ being set st b₁ in X ) & ( X is empty implies ex b₁ being set st b₁ is empty ) )

proof end;

consistency
for b₁ being set holds verum ;
sethood
( ( not X is empty & ex b₁ being set st
for b₂ being set st b₂ in X holds
b₂ in b₁ ) or ( X is empty & ex b₁ being set st
for b₂ being set st b₂ is empty holds
b₂ in b₁ ) )

proof end;

end;

:: deftheorem Def1 defines Element SUBSET_1:def 1 :
for X, b₂ being set holds
( ( not X is empty implies ( b₂ is Element of X iff b₂ in X ) ) & ( X is empty implies ( b₂ is Element of X iff b₂ 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 b₁ being Subset of X holds b₁ is empty

proof end;

end;

registration

let X1, X2 be non empty set ;

cluster [:X1,X2:] -> non empty ;

coherence
not [:X1,X2:] is empty

proof end;

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 b₁ being Element of X holds b₁ is Element of D

proof end;

end;

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

proof end;

registration

let E be set ;

cluster empty for Element of bool E;

existence
ex b₁ being Subset of E st b₁ is empty

proof end;

end;

definition

let E be set ;

func {} E -> Subset of E equals :: SUBSET_1:def 2
{} ;

coherence
{} is Subset of E

proof end;

correctness
;

func [#] E -> Subset of E equals :: SUBSET_1:def 3
E;

coherence
E is Subset of E

proof end;

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

proof end;

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

proof end;

theorem :: 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 by Th2;

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

proof end;

definition

let E be set ;
let A be Subset of E;

func A ` -> Subset of E equals :: SUBSET_1:def 4
E \ A;

coherence
E \ A is Subset of E

proof end;

correctness
;
involutiveness
for b₁, b₂ being Subset of E st b₁ = E \ b₂ holds
b₂ = E \ b₁

proof end;

let B be Subset of E;
:: original: \/
redefine func A \/ B -> Subset of E;
coherence
A \/ B is Subset of E

proof end;

:: original: \+\
redefine func A \+\ B -> Subset of E;
coherence
A \+\ B is Subset of E

proof end;

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 func X \ Y -> Subset of X;
coherence
X \ Y is Subset of X

proof end;

end;

definition

let E be set ;
let A be Subset of E;
let X be set ;
:: original: \
redefine func A \ X -> Subset of E;
coherence
A \ X is Subset of E

proof end;

end;

definition

let E be set ;
let A be Subset of E;
let X be set ;
:: original: /\
redefine func A /\ X -> Subset of E;
coherence
A /\ X is Subset of E

proof end;

end;

definition

let E, X be set ;
let A be Subset of E;
:: original: /\
redefine func X /\ A -> Subset of E;
coherence
X /\ A is Subset of E

proof end;

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

proof end;

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 & x in C ) ) ) holds
A = B /\ C

proof end;

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 & not x in C ) ) ) holds
A = B \ C

proof end;

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 & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C

proof end;

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

proof end;

theorem :: SUBSET_1:11

for E being set
for A being Subset of E holds A \/ ([#] E) = [#] E

proof end;

theorem Th12: :: SUBSET_1:12

for E being set
for A, B being Subset of E holds
( A c= B iff B ` c= A ` )

proof end;

theorem :: SUBSET_1:13

for E being set
for A, B being Subset of E holds A \ B = A /\ (B `)

proof end;

theorem :: SUBSET_1:14

for E being set
for A, B being Subset of E holds (A \ B) ` = (A `) \/ B

proof end;

theorem :: SUBSET_1:15

for E being set
for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))

proof end;

theorem :: SUBSET_1:16

for E being set
for A, B being Subset of E st A c= B ` holds
B c= A `

proof end;

theorem :: SUBSET_1:17

for E being set
for A, B being Subset of E st A ` c= B holds
B ` c= A

proof end;

theorem :: SUBSET_1:18

for E being set
for A being Subset of E holds
( A c= A ` iff A = {} E ) by XBOOLE_1:38;

theorem :: SUBSET_1:19

for E being set
for A being Subset of E holds
( A ` c= A iff A = [#] E )

proof end;

theorem :: SUBSET_1:20

for E, X being set
for A being Subset of E st X c= A & 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 ` by Th12, XBOOLE_1:7;

theorem :: SUBSET_1:22

for E being set
for A, B being Subset of E holds A ` c= (A /\ B) ` by Th12, XBOOLE_1:17;

theorem Th23: :: SUBSET_1:23

for E being set
for A, B being Subset of E holds
( A misses B iff A c= B ` )

proof end;

theorem :: SUBSET_1:24

for E being set
for A, B being Subset of E holds
( A misses B ` iff A c= B )

proof end;

theorem :: SUBSET_1:25

for E being set
for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `

proof end;

theorem :: SUBSET_1:26

for E being set
for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `

proof end;

::
:: 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

proof end;

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

proof end;

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 `

proof end;

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 `

proof end;

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 `

proof end;

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 & not x in B ) or ( x in B & not x in A ) ) ) holds
A = B `

proof end;

theorem :: SUBSET_1:33

for X being set
for x1 being Element of X st X <> {} holds
{x1} is Subset of X

proof end;

theorem :: SUBSET_1:34

for X being set
for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: SUBSET_1:41

for X, x being set st x in X holds
{x} is Subset of X

proof end;

scheme :: SUBSET_1:sch 1
SubsetEx{ F₁() -> set , P₁[ object ] } :

ex X being Subset of F₁() st
for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) )

proof end;

scheme :: SUBSET_1:sch 2
SubsetEq{ F₁() -> set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), P₁[ set ] } :

F₂() = F₃()

provided

A1: for y being Element of F₁() holds
( y in F₂() iff P₁[y] ) and
A2: for y being Element of F₁() holds
( y in F₃() iff P₁[y] )

proof end;

definition

let X, Y be non empty set ;
:: original: misses
redefine pred X misses Y;
irreflexivity
for X being non empty set holds R6(b₁,b₁) ;

end;

definition

let X, Y be non empty set ;
:: original: misses
redefine pred X meets Y;
reflexivity
for X being non empty set holds R6(b₁,b₁) ;

end;

definition

end;

:: deftheorem SUBSET_1:def 5 :
canceled;

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

proof end;

Lm3: for E being set
for A being Subset of E
for x being object st x in A holds
x is Element of E

proof end;

:: from SETWISEO, 2005.6.11 , A.T.

scheme :: SUBSET_1:sch 3
SubsetEx{ F₁() -> non empty set , P₁[ object ] } :

ex B being Subset of F₁() st
for x being Element of F₁() holds
( x in B iff P₁[x] )

proof end;

:: from GROUP_2, 2005.6.14 , A.T.

scheme :: SUBSET_1:sch 4
SubComp{ F₁() -> set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), P₁[ set ] } :

F₂() = F₃()

provided

A1: for X being Element of F₁() holds
( X in F₂() iff P₁[X] ) and
A2: for X being Element of F₁() holds
( X in F₃() iff P₁[X] )

proof end;

:: 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

proof end;

:: from SGRAPH1, 2008.06.02

registration

let X be empty set ;

cluster -> empty for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is empty

proof 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 :: 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 ;

end;

registration

let E be set ;

cluster non proper for Element of bool E;

existence
not for b₁ being Subset of E holds b₁ is proper

proof end;

end;

registration

let E be non empty set ;

cluster non proper -> non empty for Element of bool E;

coherence
for b₁ being Subset of E st not b₁ is proper holds
not b₁ is empty ;

cluster empty -> proper for Element of bool E;

coherence
for b₁ being Subset of E st b₁ is empty holds
b₁ is proper ;

end;

registration

let E be non empty set ;

cluster proper for Element of bool E;

existence
ex b₁ being Subset of E st b₁ is proper

proof end;

end;

registration

let E be empty set ;

cluster -> non proper for Element of bool E;

coherence
for b₁ being Subset of E holds not b₁ is proper ;

end;

:: from GRCAT_1, 2010.02.18, A.T.

theorem :: SUBSET_1:43

for X, Y, A, z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]

proof end;

:: 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 & A c= B \ {p} )

proof end;

definition

let X be 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 )

proof end;

end;

:: deftheorem defines trivial SUBSET_1:def 7 :
for X being 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 b₁ being Subset of X st
( not b₁ is empty & b₁ is trivial )

proof end;

end;

registration

let X be trivial set ;

cluster -> trivial for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is trivial

proof end;

end;

registration

let X be non trivial set ;

cluster non trivial for Element of bool X;

existence
not for b₁ being Subset of X holds b₁ is trivial

proof end;

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 & d2 in A & d1 <> d2 )

proof end;

theorem Th46: :: SUBSET_1:46

for X being non empty trivial set ex x being Element of X st X = {x}

proof end;

:: 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}

proof end;

theorem :: SUBSET_1:48

for X being non trivial set
for x being Element of X ex y being object st
( y in X & x <> y )

proof end;

definition

let x be object ;
let X be set ;
assume A1: x in X ;

func In (x,X) -> Element of X equals :Def7: :: SUBSET_1:def 8
x;

correctness
coherence
x is Element of X;

proof end;

end;

:: deftheorem Def7 defines In SUBSET_1:def 8 :
for x being object
for X being set st x in X holds
In (x,X) = x;

registration

let X be non empty set ;
let x be Element of X;

reduce In (x,X) to x;

reducibility
In (x,X) = x

proof end;

end;

theorem :: SUBSET_1:49

for X, Y being set
for x being object st x in X /\ Y holds
In (x,X) = In (x,Y)

proof end;

:: from BORSUK_4, 2012.08.12, A.T.

theorem :: SUBSET_1:50

for X being non trivial set
for p being set ex q being Element of X st q <> p

proof end;

theorem :: SUBSET_1:51

for T being non trivial set
for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X & q <> p )

proof end;

:: 2012.12.16, A.T.

scheme :: SUBSET_1:sch 5
Union1{ F₁() -> set , F₂() -> Element of F₁(), F₃( object ) -> set } :

union { F₃(j) where j is Element of F₁() : j in {F₂()} } = F₃(F₂())

proof end;

scheme :: SUBSET_1:sch 6
Union2{ F₁() -> set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄( object ) -> set } :

union { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } = F₄(F₂()) \/ F₄(F₃())

proof end;

theorem :: SUBSET_1:52

for X being set
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} is Subset of X

proof end;

theorem :: SUBSET_1:53

for X being set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is Subset of X

proof end;