:: SUBSET_1 semantic presentation

registration

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

end;

registration

let c₁ be set ;
cluster {a₁} -> non empty ;
coherence by TARSKI:def 1;
let c₂ be set ;
cluster {a₁,a₂} -> non empty ;
coherence by TARSKI:def 2;

end;

definition

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

end;

:: deftheorem Def1 SUBSET_1:def 1 :

:: deftheorem Def2 defines Element SUBSET_1:def 2 :

definition

let c₁ be set ;
mode Subset of a₁ is Element of bool a₁;

end;

registration

let c₁ be non empty set ;
cluster non empty Element of bool a₁;
existence

proof end;

end;

registration

let c₁, c₂ be non empty set ;
cluster [:a₁,a₂:] -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃ be non empty set ;
cluster [:a₁,a₂,a₃:] -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃, c₄ be non empty set ;
cluster [:a₁,a₂,a₃,a₄:] -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
redefine mode Element as Element of c₂ -> Element of a₁;
coherence

proof end;

end;

Lemma2: for b₁ being set
for b₂ being Subset of b₁
for b₃ being set st b₃ in b₂ holds
b₃ in b₁

proof end;

registration

let c₁ be set ;
cluster empty Element of bool a₁;
existence

proof end;

end;

definition

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

proof end;

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

proof end;

correctness ;

end;

:: deftheorem Def3 defines {} SUBSET_1:def 3 :

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

theorem Th1: :: SUBSET_1:1

canceled;

theorem Th2: :: SUBSET_1:2

canceled;

theorem Th3: :: SUBSET_1:3

canceled;

theorem Th4: :: SUBSET_1:4

for b₁ being set holds {} is Subset of b₁

proof end;

theorem Th5: :: SUBSET_1:5

canceled;

theorem Th6: :: SUBSET_1:6

canceled;

theorem Th7: :: SUBSET_1:7

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ c= b₃

proof end;

theorem Th8: :: SUBSET_1:8

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

theorem Th9: :: SUBSET_1:9

canceled;

theorem Th10: :: SUBSET_1:10

for b₁ being set
for b₂ being Subset of b₁ st b₂ <> {} holds
ex b₃ being Element of b₁ st b₃ in b₂

proof end;

definition

let c₁ be set ;
let c₂ be Subset of c₁;
func c₂ ` -> Subset of a₁ equals :: SUBSET_1:def 5
a₁ \ a₂;
coherence

proof end;

correctness ;
involutiveness

proof end;

let c₃ be Subset of c₁;
redefine func \/ as c₂ \/ c₃ -> Subset of a₁;
coherence

proof end;

redefine func /\ as c₂ /\ c₃ -> Subset of a₁;
coherence

proof end;

redefine func \ as c₂ \ c₃ -> Subset of a₁;
coherence

proof end;

redefine func \+\ as c₂ \+\ c₃ -> Subset of a₁;
coherence

proof end;

end;

:: deftheorem Def5 defines ` SUBSET_1:def 5 :

theorem Th11: :: SUBSET_1:11

canceled;

theorem Th12: :: SUBSET_1:12

canceled;

theorem Th13: :: SUBSET_1:13

canceled;

theorem Th14: :: SUBSET_1:14

canceled;

theorem Th15: :: SUBSET_1:15

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st ( for b₅ being Element of b₁ holds
( b₅ in b₂ iff ( b₅ in b₃ or b₅ in b₄ ) ) ) holds
b₂ = b₃ \/ b₄

proof end;

theorem Th16: :: SUBSET_1:16

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st ( for b₅ being Element of b₁ holds
( b₅ in b₂ iff ( b₅ in b₃ & b₅ in b₄ ) ) ) holds
b₂ = b₃ /\ b₄

proof end;

theorem Th17: :: SUBSET_1:17

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st ( for b₅ being Element of b₁ holds
( b₅ in b₂ iff ( b₅ in b₃ & not b₅ in b₄ ) ) ) holds
b₂ = b₃ \ b₄

proof end;

theorem Th18: :: SUBSET_1:18

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st ( for b₅ being Element of b₁ holds
( b₅ in b₂ iff ( ( b₅ in b₃ & not b₅ in b₄ ) or ( b₅ in b₄ & not b₅ in b₃ ) ) ) ) holds
b₂ = b₃ \+\ b₄

proof end;

theorem Th19: :: SUBSET_1:19

canceled;

theorem Th20: :: SUBSET_1:20

canceled;

theorem Th21: :: SUBSET_1:21

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

theorem Th22: :: SUBSET_1:22

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

theorem Th23: :: SUBSET_1:23

canceled;

theorem Th24: :: SUBSET_1:24

canceled;

theorem Th25: :: SUBSET_1:25

for b₁ being set
for b₂ being Subset of b₁ holds b₂ \/ (b₂ ` ) = [#] b₁

proof end;

theorem Th26: :: SUBSET_1:26

for b₁ being set
for b₂ being Subset of b₁ holds b₂ misses b₂ ` by XBOOLE_1:79;

theorem Th27: :: SUBSET_1:27

canceled;

theorem Th28: :: SUBSET_1:28

for b₁ being set
for b₂ being Subset of b₁ holds b₂ \/ ([#] b₁) = [#] b₁

proof end;

theorem Th29: :: SUBSET_1:29

for b₁ being set
for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ` = (b₂ ` ) /\ (b₃ ` ) by XBOOLE_1:53;

theorem Th30: :: SUBSET_1:30

for b₁ being set
for b₂, b₃ being Subset of b₁ holds (b₂ /\ b₃) ` = (b₂ ` ) \/ (b₃ ` ) by XBOOLE_1:54;

theorem Th31: :: SUBSET_1:31

for b₁ being set
for b₂, b₃ being Subset of b₁ holds
( b₂ c= b₃ iff b₃ ` c= b₂ ` )

proof end;

theorem Th32: :: SUBSET_1:32

for b₁ being set
for b₂, b₃ being Subset of b₁ holds b₂ \ b₃ = b₂ /\ (b₃ ` )

proof end;

theorem Th33: :: SUBSET_1:33

for b₁ being set
for b₂, b₃ being Subset of b₁ holds (b₂ \ b₃) ` = (b₂ ` ) \/ b₃

proof end;

theorem Th34: :: SUBSET_1:34

for b₁ being set
for b₂, b₃ being Subset of b₁ holds (b₂ \+\ b₃) ` = (b₂ /\ b₃) \/ ((b₂ ` ) /\ (b₃ ` ))

proof end;

theorem Th35: :: SUBSET_1:35

for b₁ being set
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ ` holds
b₃ c= b₂ `

proof end;

theorem Th36: :: SUBSET_1:36

for b₁ being set
for b₂, b₃ being Subset of b₁ st b₂ ` c= b₃ holds
b₃ ` c= b₂

proof end;

theorem Th37: :: SUBSET_1:37

canceled;

theorem Th38: :: SUBSET_1:38

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ c= b₂ ` iff b₂ = {} b₁ )

proof end;

theorem Th39: :: SUBSET_1:39

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ ` c= b₂ iff b₂ = [#] b₁ )

proof end;

theorem Th40: :: SUBSET_1:40

for b₁, b₂ being set
for b₃ being Subset of b₁ st b₂ c= b₃ & b₂ c= b₃ ` holds
b₂ = {}

proof end;

theorem Th41: :: SUBSET_1:41

for b₁ being set
for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ` c= b₂ `

proof end;

theorem Th42: :: SUBSET_1:42

for b₁ being set
for b₂, b₃ being Subset of b₁ holds b₂ ` c= (b₂ /\ b₃) `

proof end;

theorem Th43: :: SUBSET_1:43

for b₁ being set
for b₂, b₃ being Subset of b₁ holds
( b₂ misses b₃ iff b₂ c= b₃ ` )

proof end;

theorem Th44: :: SUBSET_1:44

for b₁ being set
for b₂, b₃ being Subset of b₁ holds
( b₂ misses b₃ ` iff b₂ c= b₃ )

proof end;

theorem Th45: :: SUBSET_1:45

canceled;

theorem Th46: :: SUBSET_1:46

for b₁ being set
for b₂, b₃ being Subset of b₁ st b₂ misses b₃ & b₂ ` misses b₃ ` holds
b₂ = b₃ `

proof end;

theorem Th47: :: SUBSET_1:47

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st b₂ c= b₃ & b₄ misses b₃ holds
b₂ c= b₄ `

proof end;

theorem Th48: :: SUBSET_1:48

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₂ holds b₄ in b₃ ) holds
b₂ c= b₃

proof end;

theorem Th49: :: SUBSET_1:49

for b₁ being set
for b₂ being Subset of b₁ st ( for b₃ being Element of b₁ holds b₃ in b₂ ) holds
b₁ = b₂

proof end;

theorem Th50: :: SUBSET_1:50

for b₁ being set st b₁ <> {} holds
for b₂ being Subset of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
b₃ in b₂ `

proof end;

theorem Th51: :: SUBSET_1:51

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁ holds
( b₄ in b₂ iff not b₄ in b₃ ) ) holds
b₂ = b₃ `

proof end;

theorem Th52: :: SUBSET_1:52

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁ holds
( not b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃ `

proof end;

theorem Th53: :: SUBSET_1:53

for b₁ being set
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁ holds
( ( b₄ in b₂ & not b₄ in b₃ ) or ( b₄ in b₃ & not b₄ in b₂ ) ) ) holds
b₂ = b₃ `

proof end;

theorem Th54: :: SUBSET_1:54

for b₁, b₂ being set
for b₃ being Subset of b₁ st b₂ in b₃ ` holds
not b₂ in b₃ by XBOOLE_0:def 4;

theorem Th55: :: SUBSET_1:55

for b₁ being set
for b₂ being Element of b₁ st b₁ <> {} holds
{b₂} is Subset of b₁

proof end;

theorem Th56: :: SUBSET_1:56

for b₁ being set
for b₂, b₃ being Element of b₁ st b₁ <> {} holds
{b₂,b₃} is Subset of b₁

proof end;

theorem Th57: :: SUBSET_1:57

for b₁ being set
for b₂, b₃, b₄ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄} is Subset of b₁

proof end;

theorem Th58: :: SUBSET_1:58

for b₁ being set
for b₂, b₃, b₄, b₅ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄,b₅} is Subset of b₁

proof end;

theorem Th59: :: SUBSET_1:59

for b₁ being set
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄,b₅,b₆} is Subset of b₁

proof end;

theorem Th60: :: SUBSET_1:60

for b₁ being set
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄,b₅,b₆,b₇} is Subset of b₁

proof end;

theorem Th61: :: SUBSET_1:61

for b₁ being set
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄,b₅,b₆,b₇,b₈} is Subset of b₁

proof end;

theorem Th62: :: SUBSET_1:62

for b₁ being set
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st b₁ <> {} holds
{b₂,b₃,b₄,b₅,b₆,b₇,b₈,b₉} is Subset of b₁

proof end;

theorem Th63: :: SUBSET_1:63

for b₁, b₂ being set st b₁ in b₂ holds
{b₁} is Subset of b₂

proof end;

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

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

proof end;

scheme :: SUBSET_1:sch 2
s2{ F₁() -> set , P₁[ set ] } :

for b₁, b₂ being Subset of F₁() st ( for b₃ being Element of F₁() holds
( b₃ in b₁ iff P₁[b₃] ) ) & ( for b₃ being Element of F₁() holds
( b₃ in b₂ iff P₁[b₃] ) ) holds
b₁ = b₂

proof end;

definition

let c₁, c₂ be non empty set ;
redefine pred misses as c₁ misses c₂;
irreflexivity

proof end;

end;

definition

let c₁, c₂ be non empty set ;
redefine pred misses as c₁ meets c₂;
reflexivity

proof end;

end;

definition

let c₁ be set ;
assume E11: contradiction ;
func choose c₁ -> Element of a₁ means :: SUBSET_1:def 6
verum;
correctness by E11;

end;

:: deftheorem Def6 defines choose SUBSET_1:def 6 :

Lemma11: for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
b₃ in b₂ ) holds
b₁ is Subset of b₂

proof end;

Lemma12: for b₁, b₂ being set
for b₃ being Subset of b₂ st b₁ in b₃ holds
b₁ is Element of b₂

proof end;

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

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

proof end;

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

F₂() = F₃()

provided

E13: for b₁ being Element of F₁() holds
( b₁ in F₂() iff P₁[b₁] ) and
E14: for b₁ being Element of F₁() holds
( b₁ in F₃() iff P₁[b₁] )

proof end;