:: SUBSET_1 semantic presentation

registration

let X be set ;
cluster bool X -> non empty ;
coherence by ZFMISC_1:def 1;

end;

registration

let x be set ;
cluster {x} -> non empty ;
coherence by TARSKI:def 1;
let y be set ;
cluster {x,y} -> non empty ;
coherence by TARSKI:def 2;

end;

definition

let X be set ;
canceled;
mode Element of X -> set means :Def2: :: SUBSET_1:def 2
it in X if not X is empty
otherwise it is empty;
existence by XBOOLE_0:def 1;
consistency ;

end;

:: deftheorem SUBSET_1:def 1 :

:: deftheorem Def2 defines Element SUBSET_1:def 2 :

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 Element of bool X;
existence

proof end;

end;

registration

let X1, X2 be non empty set ;
cluster [:X1,X2:] -> non empty ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

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

proof end;

registration

let E be set ;
cluster empty Element of bool E;
existence

proof end;

end;

definition

let E be set ;
func {} E -> empty Subset of E equals :: SUBSET_1:def 3
{} ;
coherence

proof end;

correctness ;
func [#] E -> Subset of E equals :: SUBSET_1:def 4
E;
coherence

proof end;

correctness ;

end;

:: deftheorem defines {} SUBSET_1:def 3 :

:: deftheorem defines [#] SUBSET_1:def 4 :

theorem :: SUBSET_1:1

canceled;

theorem :: SUBSET_1:2

canceled;

theorem :: SUBSET_1:3

canceled;

theorem :: SUBSET_1:4

for X being set holds {} is Subset of X

proof end;

theorem :: SUBSET_1:5

canceled;

theorem :: SUBSET_1:6

canceled;

theorem Th7: :: SUBSET_1:7

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 Th8: :: SUBSET_1:8

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

proof end;

theorem :: SUBSET_1:9

canceled;

theorem :: SUBSET_1:10

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 5
E \ A;
coherence

proof end;

correctness ;
involutiveness

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

:: deftheorem defines ` SUBSET_1:def 5 :

theorem :: SUBSET_1:11

canceled;

theorem :: SUBSET_1:12

canceled;

theorem :: SUBSET_1:13

canceled;

theorem :: SUBSET_1:14

canceled;

theorem :: SUBSET_1:15

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

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

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

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

canceled;

theorem :: SUBSET_1:20

canceled;

theorem Th21: :: SUBSET_1:21

for E being set holds {} E = ([#] E) ` by XBOOLE_1:37;

theorem :: SUBSET_1:22

for E being set holds [#] E = ({} E) ` ;

theorem :: SUBSET_1:23

canceled;

theorem :: SUBSET_1:24

canceled;

theorem Th25: :: SUBSET_1:25

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

proof end;

theorem Th26: :: SUBSET_1:26

for E being set
for A being Subset of E holds A misses A ` by XBOOLE_1:79;

theorem :: SUBSET_1:27

canceled;

theorem :: SUBSET_1:28

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

proof end;

theorem :: SUBSET_1:29

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

theorem :: SUBSET_1:30

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

theorem Th31: :: SUBSET_1:31

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

proof end;

theorem :: SUBSET_1:32

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

proof end;

theorem :: SUBSET_1:33

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

proof end;

theorem :: SUBSET_1:34

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

proof end;

theorem :: SUBSET_1:35

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

proof end;

theorem :: SUBSET_1:36

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

proof end;

theorem :: SUBSET_1:37

canceled;

theorem :: SUBSET_1:38

for E being set
for A being Subset of E holds
( A c= A ` iff A = {} E )

proof end;

theorem :: SUBSET_1:39

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

proof end;

theorem :: SUBSET_1:40

for E, X being set
for A being Subset of E st X c= A & X c= A ` holds
X = {}

proof end;

theorem :: SUBSET_1:41

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

proof end;

theorem :: SUBSET_1:42

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

proof end;

theorem Th43: :: SUBSET_1:43

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

proof end;

theorem :: SUBSET_1:44

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

proof end;

theorem :: SUBSET_1:45

canceled;

theorem :: SUBSET_1:46

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

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;

theorem :: SUBSET_1:48

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

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

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 Th51: :: SUBSET_1:51

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

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

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

for E, x being set
for A being Subset of E st x in A ` holds
not x in A by XBOOLE_0:def 4;

theorem :: SUBSET_1:55

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

proof end;

theorem :: SUBSET_1:56

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

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

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

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

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

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

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

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₁[ set ] } :

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 , P₁[ set ] } :

for X1, X2 being Subset of F₁() st ( for y being Element of F₁() holds
( y in X1 iff P₁[y] ) ) & ( for y being Element of F₁() holds
( y in X2 iff P₁[y] ) ) holds
X1 = X2

proof end;

definition

let X, Y be non empty set ;
:: original: misses
redefine pred X misses Y;
irreflexivity

proof end;

end;

definition

let X, Y be non empty set ;
:: original: misses
redefine pred X meets Y;
reflexivity

proof end;

end;

definition

let S be set ;
assume A1: contradiction ;
func choose S -> Element of S means :: SUBSET_1:def 6
verum;
correctness by A1;

end;

:: deftheorem defines choose SUBSET_1:def 6 :

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

proof end;

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

proof end;

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

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

proof end;

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;