:: PZFMISC1 semantic presentation

theorem Th1: :: PZFMISC1:1

for b₁, b₂, b₃ being set
for b₄ being ManySortedSet of b₁ st b₂ in b₁ holds
dom (b₄ +* (b₂ .--> b₃)) = b₁

proof end;

theorem Th2: :: PZFMISC1:2

for b₁ being Function st b₁ = {} holds
b₁ is ManySortedSet of {} by PBOOLE:def 3, RELAT_1:60;

theorem Th3: :: PZFMISC1:3

for b₁ being set st not b₁ is empty holds
for b₂ being ManySortedSet of b₁ holds
( not b₂ is empty-yielding or not b₂ is non-empty )

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func {c₂} -> ManySortedSet of a₁ means :Def1: :: PZFMISC1:def 1
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = {(a₂ . b₁)};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines { PZFMISC1:def 1 :

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster {a₂} -> V3 locally-finite ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
func {c₂,c₃} -> ManySortedSet of a₁ means :Def2: :: PZFMISC1:def 2
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = {(a₂ . b₁),(a₃ . b₁)};
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines { PZFMISC1:def 2 :

registration

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
cluster {a₂,a₃} -> V3 locally-finite ;
coherence

proof end;

end;

theorem Th4: :: PZFMISC1:4

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ = {b₃} iff for b₄ being ManySortedSet of b₁ holds
( b₄ in b₂ iff b₄ = b₃ ) )

proof end;

theorem Th5: :: PZFMISC1:5

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( for b₅ being ManySortedSet of b₁ holds
( b₅ in b₂ iff ( b₅ = b₃ or b₅ = b₄ ) ) ) holds
b₂ = {b₃,b₄}

proof end;

theorem Th6: :: PZFMISC1:6

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ = {b₃,b₄} holds
for b₅ being ManySortedSet of b₁ st ( b₅ = b₃ or b₅ = b₄ ) holds
b₅ in b₂

proof end;

theorem Th7: :: PZFMISC1:7

canceled;

theorem Th8: :: PZFMISC1:8

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ in {b₃} holds
b₂ = b₃

proof end;

theorem Th9: :: PZFMISC1:9

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ in {b₂}

proof end;

theorem Th10: :: PZFMISC1:10

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( b₂ = b₃ or b₂ = b₄ ) holds
b₂ in {b₃,b₄}

proof end;

theorem Th11: :: PZFMISC1:11

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds {b₂} \/ {b₃} = {b₂,b₃}

proof end;

theorem Th12: :: PZFMISC1:12

for b₁ being set
for b₂ being ManySortedSet of b₁ holds {b₂,b₂} = {b₂}

proof end;

theorem Th13: :: PZFMISC1:13

canceled;

theorem Th14: :: PZFMISC1:14

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st {b₂} c= {b₃} holds
b₂ = b₃

proof end;

theorem Th15: :: PZFMISC1:15

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st {b₂} = {b₃} holds
b₂ = b₃

proof end;

theorem Th16: :: PZFMISC1:16

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st {b₂} = {b₃,b₄} holds
( b₂ = b₃ & b₂ = b₄ )

proof end;

theorem Th17: :: PZFMISC1:17

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st {b₂} = {b₃,b₄} holds
b₃ = b₄

proof end;

theorem Th18: :: PZFMISC1:18

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( {b₂} c= {b₂,b₃} & {b₃} c= {b₂,b₃} )

proof end;

theorem Th19: :: PZFMISC1:19

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st ( {b₂} \/ {b₃} = {b₂} or {b₂} \/ {b₃} = {b₃} ) holds
b₂ = b₃

proof end;

theorem Th20: :: PZFMISC1:20

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds {b₂} \/ {b₂,b₃} = {b₂,b₃}

proof end;

theorem Th21: :: PZFMISC1:21

canceled;

theorem Th22: :: PZFMISC1:22

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty & {b₂} /\ {b₃} = [0] b₁ holds
b₂ <> b₃

proof end;

theorem Th23: :: PZFMISC1:23

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st ( {b₂} /\ {b₃} = {b₂} or {b₂} /\ {b₃} = {b₃} ) holds
b₂ = b₃

proof end;

theorem Th24: :: PZFMISC1:24

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( {b₂} /\ {b₂,b₃} = {b₂} & {b₃} /\ {b₂,b₃} = {b₃} )

proof end;

theorem Th25: :: PZFMISC1:25

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty & {b₂} \ {b₃} = {b₂} holds
b₂ <> b₃

proof end;

theorem Th26: :: PZFMISC1:26

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st {b₂} \ {b₃} = [0] b₁ holds
b₂ = b₃

proof end;

theorem Th27: :: PZFMISC1:27

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( {b₂} \ {b₂,b₃} = [0] b₁ & {b₃} \ {b₂,b₃} = [0] b₁ )

proof end;

theorem Th28: :: PZFMISC1:28

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st {b₂} c= {b₃} holds
{b₂} = {b₃}

proof end;

theorem Th29: :: PZFMISC1:29

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st {b₂,b₃} c= {b₄} holds
( b₂ = b₄ & b₃ = b₄ )

proof end;

theorem Th30: :: PZFMISC1:30

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st {b₂,b₃} c= {b₄} holds
{b₂,b₃} = {b₄}

proof end;

theorem Th31: :: PZFMISC1:31

for b₁ being set
for b₂ being ManySortedSet of b₁ holds bool {b₂} = {([0] b₁),{b₂}}

proof end;

theorem Th32: :: PZFMISC1:32

for b₁ being set
for b₂ being ManySortedSet of b₁ holds {b₂} c= bool b₂

proof end;

theorem Th33: :: PZFMISC1:33

for b₁ being set
for b₂ being ManySortedSet of b₁ holds union {b₂} = b₂

proof end;

theorem Th34: :: PZFMISC1:34

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds union {{b₂},{b₃}} = {b₂,b₃}

proof end;

theorem Th35: :: PZFMISC1:35

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds union {b₂,b₃} = b₂ \/ b₃

proof end;

theorem Th36: :: PZFMISC1:36

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( {b₂} c= b₃ iff b₂ in b₃ )

proof end;

theorem Th37: :: PZFMISC1:37

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( {b₂,b₃} c= b₄ iff ( b₂ in b₄ & b₃ in b₄ ) )

proof end;

theorem Th38: :: PZFMISC1:38

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( b₂ = [0] b₁ or b₂ = {b₃} or b₂ = {b₄} or b₂ = {b₃,b₄} ) holds
b₂ c= {b₃,b₄}

proof end;

theorem Th39: :: PZFMISC1:39

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( b₂ in b₃ or b₂ = b₄ ) holds
b₂ in b₃ \/ {b₄}

proof end;

theorem Th40: :: PZFMISC1:40

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( b₂ \/ {b₃} c= b₄ iff ( b₃ in b₄ & b₂ c= b₄ ) )

proof end;

theorem Th41: :: PZFMISC1:41

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st {b₂} \/ b₃ = b₃ holds
b₂ in b₃

proof end;

theorem Th42: :: PZFMISC1:42

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ in b₃ holds
{b₂} \/ b₃ = b₃

proof end;

theorem Th43: :: PZFMISC1:43

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( {b₂,b₃} \/ b₄ = b₄ iff ( b₂ in b₄ & b₃ in b₄ ) )

proof end;

theorem Th44: :: PZFMISC1:44

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty holds
{b₂} \/ b₃ <> [0] b₁

proof end;

theorem Th45: :: PZFMISC1:45

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st not b₁ is empty holds
{b₂,b₃} \/ b₄ <> [0] b₁

proof end;

theorem Th46: :: PZFMISC1:46

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ /\ {b₃} = {b₃} holds
b₃ in b₂

proof end;

theorem Th47: :: PZFMISC1:47

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ in b₃ holds
b₃ /\ {b₂} = {b₂}

proof end;

theorem Th48: :: PZFMISC1:48

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( ( b₂ in b₃ & b₄ in b₃ ) iff {b₂,b₄} /\ b₃ = {b₂,b₄} )

proof end;

theorem Th49: :: PZFMISC1:49

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty & {b₂} /\ b₃ = [0] b₁ holds
not b₂ in b₃

proof end;

theorem Th50: :: PZFMISC1:50

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st not b₁ is empty & {b₂,b₃} /\ b₄ = [0] b₁ holds
( not b₂ in b₄ & not b₃ in b₄ )

proof end;

theorem Th51: :: PZFMISC1:51

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ in b₃ \ {b₄} holds
b₂ in b₃

proof end;

theorem Th52: :: PZFMISC1:52

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st not b₁ is empty & b₂ in b₃ \ {b₄} holds
b₂ <> b₄

proof end;

theorem Th53: :: PZFMISC1:53

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty & b₂ \ {b₃} = b₂ holds
not b₃ in b₂

proof end;

theorem Th54: :: PZFMISC1:54

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st not b₁ is empty & {b₂} \ b₃ = {b₂} holds
not b₂ in b₃

proof end;

theorem Th55: :: PZFMISC1:55

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( {b₂} \ b₃ = [0] b₁ iff b₂ in b₃ )

proof end;

theorem Th56: :: PZFMISC1:56

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st not b₁ is empty & {b₂,b₃} \ b₄ = {b₂} holds
not b₂ in b₄

proof end;

theorem Th57: :: PZFMISC1:57

canceled;

theorem Th58: :: PZFMISC1:58

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st not b₁ is empty & {b₂,b₃} \ b₄ = {b₂,b₃} holds
( not b₂ in b₄ & not b₃ in b₄ )

proof end;

theorem Th59: :: PZFMISC1:59

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( {b₂,b₃} \ b₄ = [0] b₁ iff ( b₂ in b₄ & b₃ in b₄ ) )

proof end;

theorem Th60: :: PZFMISC1:60

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( b₂ = [0] b₁ or b₂ = {b₃} or b₂ = {b₄} or b₂ = {b₃,b₄} ) holds
b₂ \ {b₃,b₄} = [0] b₁

proof end;

theorem Th61: :: PZFMISC1:61

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st ( b₂ = [0] b₁ or b₃ = [0] b₁ ) holds
[|b₂,b₃|] = [0] b₁

proof end;

theorem Th62: :: PZFMISC1:62

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & b₃ is non-empty & [|b₂,b₃|] = [|b₃,b₂|] holds
b₂ = b₃

proof end;

theorem Th63: :: PZFMISC1:63

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st [|b₂,b₂|] = [|b₃,b₃|] holds
b₂ = b₃

proof end;

theorem Th64: :: PZFMISC1:64

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ is non-empty & ( [|b₃,b₂|] c= [|b₄,b₂|] or [|b₂,b₃|] c= [|b₂,b₄|] ) holds
b₃ c= b₄

proof end;

theorem Th65: :: PZFMISC1:65

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ holds
( [|b₂,b₄|] c= [|b₃,b₄|] & [|b₄,b₂|] c= [|b₄,b₃|] )

proof end;

theorem Th66: :: PZFMISC1:66

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
[|b₂,b₄|] c= [|b₃,b₅|]

proof end;

theorem Th67: :: PZFMISC1:67

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( [|(b₂ \/ b₃),b₄|] = [|b₂,b₄|] \/ [|b₃,b₄|] & [|b₄,(b₂ \/ b₃)|] = [|b₄,b₂|] \/ [|b₄,b₃|] )

proof end;

theorem Th68: :: PZFMISC1:68

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ holds [|(b₂ \/ b₃),(b₄ \/ b₅)|] = (([|b₂,b₄|] \/ [|b₂,b₅|]) \/ [|b₃,b₄|]) \/ [|b₃,b₅|]

proof end;

theorem Th69: :: PZFMISC1:69

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( [|(b₂ /\ b₃),b₄|] = [|b₂,b₄|] /\ [|b₃,b₄|] & [|b₄,(b₂ /\ b₃)|] = [|b₄,b₂|] /\ [|b₄,b₃|] )

proof end;

theorem Th70: :: PZFMISC1:70

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ holds [|(b₂ /\ b₃),(b₄ /\ b₅)|] = [|b₂,b₄|] /\ [|b₃,b₅|]

proof end;

theorem Th71: :: PZFMISC1:71

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
[|b₂,b₅|] /\ [|b₃,b₄|] = [|b₂,b₄|]

proof end;

theorem Th72: :: PZFMISC1:72

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( [|(b₂ \ b₃),b₄|] = [|b₂,b₄|] \ [|b₃,b₄|] & [|b₄,(b₂ \ b₃)|] = [|b₄,b₂|] \ [|b₄,b₃|] )

proof end;

theorem Th73: :: PZFMISC1:73

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ holds [|b₂,b₃|] \ [|b₄,b₅|] = [|(b₂ \ b₄),b₃|] \/ [|b₂,(b₃ \ b₅)|]

proof end;

theorem Th74: :: PZFMISC1:74

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st ( b₂ /\ b₃ = [0] b₁ or b₄ /\ b₅ = [0] b₁ ) holds
[|b₂,b₄|] /\ [|b₃,b₅|] = [0] b₁

proof end;

theorem Th75: :: PZFMISC1:75

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty holds
( [|{b₃},b₂|] is non-empty & [|b₂,{b₃}|] is non-empty )

proof end;

theorem Th76: :: PZFMISC1:76

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( [|{b₂,b₃},b₄|] = [|{b₂},b₄|] \/ [|{b₃},b₄|] & [|b₄,{b₂,b₃}|] = [|b₄,{b₂}|] \/ [|b₄,{b₃}|] )

proof end;

theorem Th77: :: PZFMISC1:77

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st b₂ is non-empty & b₃ is non-empty & [|b₂,b₃|] = [|b₄,b₅|] holds
( b₂ = b₄ & b₃ = b₅ )

proof end;

theorem Th78: :: PZFMISC1:78

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st ( b₂ c= [|b₂,b₃|] or b₂ c= [|b₃,b₂|] ) holds
b₂ = [0] b₁

proof end;

theorem Th79: :: PZFMISC1:79

for b₁ being set
for b₂, b₃, b₄, b₅, b₆ being ManySortedSet of b₁ st b₂ in [|b₃,b₄|] & b₂ in [|b₅,b₆|] holds
b₂ in [|(b₃ /\ b₅),(b₄ /\ b₆)|]

proof end;

theorem Th80: :: PZFMISC1:80

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st [|b₂,b₃|] c= [|b₄,b₅|] & [|b₂,b₃|] is non-empty holds
( b₂ c= b₄ & b₃ c= b₅ )

proof end;

theorem Th81: :: PZFMISC1:81

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ holds
[|b₂,b₂|] c= [|b₃,b₃|]

proof end;

theorem Th82: :: PZFMISC1:82

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ /\ b₃ = [0] b₁ holds
[|b₂,b₃|] /\ [|b₃,b₂|] = [0] b₁

proof end;

theorem Th83: :: PZFMISC1:83

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st b₂ is non-empty & ( [|b₂,b₃|] c= [|b₄,b₅|] or [|b₃,b₂|] c= [|b₅,b₄|] ) holds
b₃ c= b₅

proof end;

theorem Th84: :: PZFMISC1:84

for b₁ being set
for b₂, b₃, b₄, b₅, b₆, b₇ being ManySortedSet of b₁ st b₂ c= [|b₃,b₄|] & b₅ c= [|b₆,b₇|] holds
b₂ \/ b₅ c= [|(b₃ \/ b₆),(b₄ \/ b₇)|]

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
pred c₂ is_transformable_to c₃ means :: PZFMISC1:def 3
for b₁ being set st b₁ in a₁ & a₃ . b₁ = {} holds
a₂ . b₁ = {} ;
reflexivity ;

end;

:: deftheorem Def3 defines is_transformable_to PZFMISC1:def 3 :