:: DOMAIN_1 semantic presentation

theorem Th1: :: DOMAIN_1:1

canceled;

theorem Th2: :: DOMAIN_1:2

canceled;

theorem Th3: :: DOMAIN_1:3

canceled;

theorem Th4: :: DOMAIN_1:4

canceled;

theorem Th5: :: DOMAIN_1:5

canceled;

theorem Th6: :: DOMAIN_1:6

canceled;

theorem Th7: :: DOMAIN_1:7

canceled;

theorem Th8: :: DOMAIN_1:8

canceled;

theorem Th9: :: DOMAIN_1:9

for b₁ being set
for b₂, b₃ being non empty set st b₁ in [:b₂,b₃:] holds
ex b₄ being Element of b₂ex b₅ being Element of b₃ st b₁ = [b₄,b₅]

proof end;

theorem Th10: :: DOMAIN_1:10

canceled;

theorem Th11: :: DOMAIN_1:11

canceled;

theorem Th12: :: DOMAIN_1:12

for b₁, b₂ being non empty set
for b₃, b₄ being Element of [:b₁,b₂:] st b₃ `1 = b₄ `1 & b₃ `2 = b₄ `2 holds
b₃ = b₄

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of c₁;
let c₄ be Element of c₂;
redefine func [ as [c₃,c₄] -> Element of [:a₁,a₂:];
coherence by ZFMISC_1:106;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of [:c₁,c₂:];
redefine func `1 as c₃ `1 -> Element of a₁;
coherence by MCART_1:10;
redefine func `2 as c₃ `2 -> Element of a₂;
coherence by MCART_1:10;

end;

theorem Th13: :: DOMAIN_1:13

canceled;

theorem Th14: :: DOMAIN_1:14

canceled;

theorem Th15: :: DOMAIN_1:15

for b₁ being set
for b₂, b₃, b₄ being non empty set holds
( b₁ in [:b₂,b₃,b₄:] iff ex b₅ being Element of b₂ex b₆ being Element of b₃ex b₇ being Element of b₄ st b₁ = [b₅,b₆,b₇] )

proof end;

theorem Th16: :: DOMAIN_1:16

for b₁, b₂, b₃, b₄ being non empty set st ( for b₅ being set holds
( b₅ in b₁ iff ex b₆ being Element of b₂ex b₇ being Element of b₃ex b₈ being Element of b₄ st b₅ = [b₆,b₇,b₈] ) ) holds
b₁ = [:b₂,b₃,b₄:]

proof end;

theorem Th17: :: DOMAIN_1:17

for b₁, b₂, b₃, b₄ being non empty set holds
( b₁ = [:b₂,b₃,b₄:] iff for b₅ being set holds
( b₅ in b₁ iff ex b₆ being Element of b₂ex b₇ being Element of b₃ex b₈ being Element of b₄ st b₅ = [b₆,b₇,b₈] ) ) by Th15, Th16;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Element of c₁;
let c₅ be Element of c₂;
let c₆ be Element of c₃;
redefine func [ as [c₄,c₅,c₆] -> Element of [:a₁,a₂,a₃:];
coherence by MCART_1:73;

end;

theorem Th18: :: DOMAIN_1:18

canceled;

theorem Th19: :: DOMAIN_1:19

canceled;

theorem Th20: :: DOMAIN_1:20

canceled;

theorem Th21: :: DOMAIN_1:21

canceled;

theorem Th22: :: DOMAIN_1:22

canceled;

theorem Th23: :: DOMAIN_1:23

canceled;

theorem Th24: :: DOMAIN_1:24

for b₁ being set
for b₂, b₃, b₄ being non empty set
for b₅ being Element of [:b₂,b₃,b₄:] holds
( b₁ = b₅ `1 iff for b₆ being Element of b₂
for b₇ being Element of b₃
for b₈ being Element of b₄ st b₅ = [b₆,b₇,b₈] holds
b₁ = b₆ )

proof end;

theorem Th25: :: DOMAIN_1:25

for b₁ being set
for b₂, b₃, b₄ being non empty set
for b₅ being Element of [:b₂,b₃,b₄:] holds
( b₁ = b₅ `2 iff for b₆ being Element of b₂
for b₇ being Element of b₃
for b₈ being Element of b₄ st b₅ = [b₆,b₇,b₈] holds
b₁ = b₇ )

proof end;

theorem Th26: :: DOMAIN_1:26

for b₁ being set
for b₂, b₃, b₄ being non empty set
for b₅ being Element of [:b₂,b₃,b₄:] holds
( b₁ = b₅ `3 iff for b₆ being Element of b₂
for b₇ being Element of b₃
for b₈ being Element of b₄ st b₅ = [b₆,b₇,b₈] holds
b₁ = b₈ )

proof end;

theorem Th27: :: DOMAIN_1:27

canceled;

theorem Th28: :: DOMAIN_1:28

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being Element of [:b₁,b₂,b₃:] st b₄ `1 = b₅ `1 & b₄ `2 = b₅ `2 & b₄ `3 = b₅ `3 holds
b₄ = b₅

proof end;

theorem Th29: :: DOMAIN_1:29

canceled;

theorem Th30: :: DOMAIN_1:30

canceled;

theorem Th31: :: DOMAIN_1:31

for b₁ being set
for b₂, b₃, b₄, b₅ being non empty set holds
( b₁ in [:b₂,b₃,b₄,b₅:] iff ex b₆ being Element of b₂ex b₇ being Element of b₃ex b₈ being Element of b₄ex b₉ being Element of b₅ st b₁ = [b₆,b₇,b₈,b₉] )

proof end;

theorem Th32: :: DOMAIN_1:32

for b₁, b₂, b₃, b₄, b₅ being non empty set st ( for b₆ being set holds
( b₆ in b₁ iff ex b₇ being Element of b₂ex b₈ being Element of b₃ex b₉ being Element of b₄ex b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] ) ) holds
b₁ = [:b₂,b₃,b₄,b₅:]

proof end;

theorem Th33: :: DOMAIN_1:33

for b₁, b₂, b₃, b₄, b₅ being non empty set holds
( b₁ = [:b₂,b₃,b₄,b₅:] iff for b₆ being set holds
( b₆ in b₁ iff ex b₇ being Element of b₂ex b₈ being Element of b₃ex b₉ being Element of b₄ex b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] ) ) by Th31, Th32;

definition

let c₁, c₂, c₃, c₄ be non empty set ;
let c₅ be Element of c₁;
let c₆ be Element of c₂;
let c₇ be Element of c₃;
let c₈ be Element of c₄;
redefine func [ as [c₅,c₆,c₇,c₈] -> Element of [:a₁,a₂,a₃,a₄:];
coherence by MCART_1:84;

end;

theorem Th34: :: DOMAIN_1:34

canceled;

theorem Th35: :: DOMAIN_1:35

canceled;

theorem Th36: :: DOMAIN_1:36

canceled;

theorem Th37: :: DOMAIN_1:37

canceled;

theorem Th38: :: DOMAIN_1:38

canceled;

theorem Th39: :: DOMAIN_1:39

canceled;

theorem Th40: :: DOMAIN_1:40

for b₁ being set
for b₂, b₃, b₄, b₅ being non empty set
for b₆ being Element of [:b₂,b₃,b₄,b₅:] holds
( b₁ = b₆ `1 iff for b₇ being Element of b₂
for b₈ being Element of b₃
for b₉ being Element of b₄
for b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] holds
b₁ = b₇ )

proof end;

theorem Th41: :: DOMAIN_1:41

for b₁ being set
for b₂, b₃, b₄, b₅ being non empty set
for b₆ being Element of [:b₂,b₃,b₄,b₅:] holds
( b₁ = b₆ `2 iff for b₇ being Element of b₂
for b₈ being Element of b₃
for b₉ being Element of b₄
for b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] holds
b₁ = b₈ )

proof end;

theorem Th42: :: DOMAIN_1:42

for b₁ being set
for b₂, b₃, b₄, b₅ being non empty set
for b₆ being Element of [:b₂,b₃,b₄,b₅:] holds
( b₁ = b₆ `3 iff for b₇ being Element of b₂
for b₈ being Element of b₃
for b₉ being Element of b₄
for b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] holds
b₁ = b₉ )

proof end;

theorem Th43: :: DOMAIN_1:43

for b₁ being set
for b₂, b₃, b₄, b₅ being non empty set
for b₆ being Element of [:b₂,b₃,b₄,b₅:] holds
( b₁ = b₆ `4 iff for b₇ being Element of b₂
for b₈ being Element of b₃
for b₉ being Element of b₄
for b₁₀ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀] holds
b₁ = b₁₀ )

proof end;

theorem Th44: :: DOMAIN_1:44

canceled;

theorem Th45: :: DOMAIN_1:45

for b₁, b₂, b₃, b₄ being non empty set
for b₅, b₆ being Element of [:b₁,b₂,b₃,b₄:] st b₅ `1 = b₆ `1 & b₅ `2 = b₆ `2 & b₅ `3 = b₆ `3 & b₅ `4 = b₆ `4 holds
b₅ = b₆

proof end;

scheme :: DOMAIN_1:sch 1
s1{ P₁[ set ] } :

for b₁ being non empty set holds { b₂ where B is Element of b₁ : P₁[b₂] } is Subset of b₁

proof end;

scheme :: DOMAIN_1:sch 2
s2{ P₁[ set , set ] } :

for b₁, b₂ being non empty set holds { [b₃,b₄] where B is Element of b₁, B is Element of b₂ : P₁[b₃,b₄] } is Subset of [:b₁,b₂:]

proof end;

scheme :: DOMAIN_1:sch 3
s3{ P₁[ set , set , set ] } :

for b₁, b₂, b₃ being non empty set holds { [b₄,b₅,b₆] where B is Element of b₁, B is Element of b₂, B is Element of b₃ : P₁[b₄,b₅,b₆] } is Subset of [:b₁,b₂,b₃:]

proof end;

scheme :: DOMAIN_1:sch 4
s4{ P₁[ set , set , set , set ] } :

for b₁, b₂, b₃, b₄ being non empty set holds { [b₅,b₆,b₇,b₈] where B is Element of b₁, B is Element of b₂, B is Element of b₃, B is Element of b₄ : P₁[b₅,b₆,b₇,b₈] } is Subset of [:b₁,b₂,b₃,b₄:]

proof end;

scheme :: DOMAIN_1:sch 5
s5{ P₁[ set ], P₂[ set ] } :

for b₁ being non empty set st ( for b₂ being Element of b₁ st P₁[b₂] holds
P₂[b₂] ) holds
{ b₂ where B is Element of b₁ : P₁[b₂] } c= { b₂ where B is Element of b₁ : P₂[b₂] }

proof end;

scheme :: DOMAIN_1:sch 6
s6{ P₁[ set ], P₂[ set ] } :

for b₁ being non empty set st ( for b₂ being Element of b₁ holds
( P₁[b₂] iff P₂[b₂] ) ) holds
{ b₂ where B is Element of b₁ : P₁[b₂] } = { b₂ where B is Element of b₁ : P₂[b₂] }

proof end;

scheme :: DOMAIN_1:sch 7
s7{ F₁() -> non empty set , P₁[ set ] } :

{ b₁ where B is Element of F₁() : P₁[b₁] } is Subset of F₁()

proof end;

theorem Th46: :: DOMAIN_1:46

canceled;

theorem Th47: :: DOMAIN_1:47

canceled;

theorem Th48: :: DOMAIN_1:48

for b₁ being non empty set holds b₁ = { b₂ where B is Element of b₁ : verum }

proof end;

theorem Th49: :: DOMAIN_1:49

for b₁, b₂ being non empty set holds [:b₁,b₂:] = { [b₃,b₄] where B is Element of b₁, B is Element of b₂ : verum }

proof end;

theorem Th50: :: DOMAIN_1:50

for b₁, b₂, b₃ being non empty set holds [:b₁,b₂,b₃:] = { [b₄,b₅,b₆] where B is Element of b₁, B is Element of b₂, B is Element of b₃ : verum }

proof end;

theorem Th51: :: DOMAIN_1:51

for b₁, b₂, b₃, b₄ being non empty set holds [:b₁,b₂,b₃,b₄:] = { [b₅,b₆,b₇,b₈] where B is Element of b₁, B is Element of b₂, B is Element of b₃, B is Element of b₄ : verum }

proof end;

theorem Th52: :: DOMAIN_1:52

for b₁ being non empty set
for b₂ being Subset of b₁ holds b₂ = { b₃ where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th53: :: DOMAIN_1:53

for b₁, b₂ being non empty set
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds [:b₃,b₄:] = { [b₅,b₆] where B is Element of b₁, B is Element of b₂ : ( b₅ in b₃ & b₆ in b₄ ) }

proof end;

theorem Th54: :: DOMAIN_1:54

for b₁, b₂, b₃ being non empty set
for b₄ being Subset of b₁
for b₅ being Subset of b₂
for b₆ being Subset of b₃ holds [:b₄,b₅,b₆:] = { [b₇,b₈,b₉] where B is Element of b₁, B is Element of b₂, B is Element of b₃ : ( b₇ in b₄ & b₈ in b₅ & b₉ in b₆ ) }

proof end;

theorem Th55: :: DOMAIN_1:55

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being Subset of b₁
for b₆ being Subset of b₂
for b₇ being Subset of b₃
for b₈ being Subset of b₄ holds [:b₅,b₆,b₇,b₈:] = { [b₉,b₁₀,b₁₁,b₁₂] where B is Element of b₁, B is Element of b₂, B is Element of b₃, B is Element of b₄ : ( b₉ in b₅ & b₁₀ in b₆ & b₁₁ in b₇ & b₁₂ in b₈ ) }

proof end;

theorem Th56: :: DOMAIN_1:56

for b₁ being non empty set holds {} b₁ = { b₂ where B is Element of b₁ : contradiction }

proof end;

theorem Th57: :: DOMAIN_1:57

for b₁ being non empty set
for b₂ being Subset of b₁ holds b₂ ` = { b₃ where B is Element of b₁ : not b₃ in b₂ }

proof end;

theorem Th58: :: DOMAIN_1:58

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ /\ b₃ = { b₄ where B is Element of b₁ : ( b₄ in b₂ & b₄ in b₃ ) }

proof end;

theorem Th59: :: DOMAIN_1:59

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \/ b₃ = { b₄ where B is Element of b₁ : ( b₄ in b₂ or b₄ in b₃ ) }

proof end;

theorem Th60: :: DOMAIN_1:60

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \ b₃ = { b₄ where B is Element of b₁ : ( b₄ in b₂ & not b₄ in b₃ ) }

proof end;

theorem Th61: :: DOMAIN_1:61

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \+\ b₃ = { b₄ where B is Element of b₁ : ( ( b₄ in b₂ & not b₄ in b₃ ) or ( not b₄ in b₂ & b₄ in b₃ ) ) }

proof end;

theorem Th62: :: DOMAIN_1:62

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \+\ b₃ = { b₄ where B is Element of b₁ : ( not b₄ in b₂ iff b₄ in b₃ ) }

proof end;

theorem Th63: :: DOMAIN_1:63

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \+\ b₃ = { b₄ where B is Element of b₁ : ( b₄ in b₂ iff not b₄ in b₃ ) }

proof end;

theorem Th64: :: DOMAIN_1:64

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ \+\ b₃ = { b₄ where B is Element of b₁ : ( ( b₄ in b₂ & not b₄ in b₃ ) or ( b₄ in b₃ & not b₄ in b₂ ) ) }

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func { as {c₂} -> Subset of a₁;
coherence by SUBSET_1:55;
let c₃ be Element of c₁;
redefine func { as {c₂,c₃} -> Subset of a₁;
coherence by SUBSET_1:56;
let c₄ be Element of c₁;
redefine func { as {c₂,c₃,c₄} -> Subset of a₁;
coherence by SUBSET_1:57;
let c₅ be Element of c₁;
redefine func { as {c₂,c₃,c₄,c₅} -> Subset of a₁;
coherence by SUBSET_1:58;
let c₆ be Element of c₁;
redefine func { as {c₂,c₃,c₄,c₅,c₆} -> Subset of a₁;
coherence by SUBSET_1:59;
let c₇ be Element of c₁;
redefine func { as {c₂,c₃,c₄,c₅,c₆,c₇} -> Subset of a₁;
coherence by SUBSET_1:60;
let c₈ be Element of c₁;
redefine func { as {c₂,c₃,c₄,c₅,c₆,c₇,c₈} -> Subset of a₁;
coherence by SUBSET_1:61;
let c₉ be Element of c₁;
redefine func { as {c₂,c₃,c₄,c₅,c₆,c₇,c₈,c₉} -> Subset of a₁;
coherence by SUBSET_1:62;

end;

scheme :: DOMAIN_1:sch 8
s8{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(b₁) where B is Element of F₁() : P₁[b₁] } is Subset of F₂()

proof end;

scheme :: DOMAIN_1:sch 9
s9{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₃(), P₁[ set , set ] } :

{ F₄(b₁,b₂) where B is Element of F₁(), B is Element of F₂() : P₁[b₁,b₂] } is Subset of F₃()

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Element of [:[:c₁,c₂:],c₃:];
redefine func `11 as c₄ `11 -> Element of a₁;
coherence

proof end;

redefine func `12 as c₄ `12 -> Element of a₂;
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Element of [:c₁,[:c₂,c₃:]:];
redefine func `21 as c₄ `21 -> Element of a₂;
coherence

proof end;

redefine func `22 as c₄ `22 -> Element of a₃;
coherence

proof end;

end;

scheme :: DOMAIN_1:sch 10
s10{ F₁() -> non empty set , P₁[ set ], P₂[ set ] } :

{ b₁ where B is Element of F₁() : ( P₁[b₁] & P₂[b₁] ) } = { b₁ where B is Element of F₁() : P₁[b₁] } /\ { b₁ where B is Element of F₁() : P₂[b₁] }

proof end;