:: ZFMISC_1 semantic presentation

registration

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

proof end;

end;

Lemma1: for b₁ being set holds {b₁} <> {}

proof end;

Lemma2: for b₁, b₂ being set holds
( {b₁} c= b₂ iff b₁ in b₂ )

proof end;

Lemma3: for b₁, b₂, b₃ being set st b₁ c= b₂ & not b₃ in b₁ holds
b₁ c= b₂ \ {b₃}

proof end;

Lemma4: for b₁, b₂ being set holds
( b₁ c= {b₂} iff ( b₁ = {} or b₁ = {b₂} ) )

proof end;

definition

let c₁ be set ;
defpred S₁[ set ] means a₁ c= c₁;
func bool c₁ -> set means :Def1: :: ZFMISC_1:def 1
for b₁ being set holds
( b₁ in a₂ iff b₁ c= a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines bool ZFMISC_1:def 1 :

definition

let c₁, c₂ be set ;
defpred S₁[ set ] means ex b₁, b₂ being set st
( b₁ in c₁ & b₂ in c₂ & a₁ = [b₁,b₂] );
func [:c₁,c₂:] -> set means :Def2: :: ZFMISC_1:def 2
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being set st
( b₂ in a₁ & b₃ in a₂ & b₁ = [b₂,b₃] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines [: ZFMISC_1:def 2 :

definition

let c₁, c₂, c₃ be set ;
func [:c₁,c₂,c₃:] -> set equals :: ZFMISC_1:def 3
[:[:a₁,a₂:],a₃:];
coherence ;

end;

:: deftheorem Def3 defines [: ZFMISC_1:def 3 :

definition

let c₁, c₂, c₃, c₄ be set ;
func [:c₁,c₂,c₃,c₄:] -> set equals :: ZFMISC_1:def 4
[:[:a₁,a₂,a₃:],a₄:];
coherence ;

end;

:: deftheorem Def4 defines [: ZFMISC_1:def 4 :

theorem Th1: :: ZFMISC_1:1

bool {} = {{} }

proof end;

theorem Th2: :: ZFMISC_1:2

union {} = {}

proof end;

theorem Th3: :: ZFMISC_1:3

canceled;

theorem Th4: :: ZFMISC_1:4

canceled;

theorem Th5: :: ZFMISC_1:5

canceled;

theorem Th6: :: ZFMISC_1:6

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

proof end;

theorem Th7: :: ZFMISC_1:7

canceled;

theorem Th8: :: ZFMISC_1:8

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

proof end;

theorem Th9: :: ZFMISC_1:9

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

proof end;

theorem Th10: :: ZFMISC_1:10

for b₁, b₂, b₃, b₄ being set holds
( not {b₁,b₂} = {b₃,b₄} or b₁ = b₃ or b₁ = b₄ )

proof end;

theorem Th11: :: ZFMISC_1:11

canceled;

theorem Th12: :: ZFMISC_1:12

for b₁, b₂ being set holds {b₁} c= {b₁,b₂}

proof end;

Lemma12: for b₁, b₂ being set st {b₁} \/ b₂ c= b₂ holds
b₁ in b₂

proof end;

theorem Th13: :: ZFMISC_1:13

for b₁, b₂ being set st {b₁} \/ {b₂} = {b₁} holds
b₁ = b₂

proof end;

Lemma13: for b₁, b₂ being set st b₁ in b₂ holds
{b₁} \/ b₂ = b₂

proof end;

theorem Th14: :: ZFMISC_1:14

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

proof end;

Lemma14: for b₁, b₂ being set st {b₁} misses b₂ holds
not b₁ in b₂

proof end;

theorem Th15: :: ZFMISC_1:15

canceled;

theorem Th16: :: ZFMISC_1:16

for b₁, b₂ being set st {b₁} misses {b₂} holds
b₁ <> b₂

proof end;

Lemma15: for b₁, b₂ being set st not b₁ in b₂ holds
{b₁} misses b₂

proof end;

theorem Th17: :: ZFMISC_1:17

for b₁, b₂ being set st b₁ <> b₂ holds
{b₁} misses {b₂}

proof end;

Lemma17: for b₁, b₂ being set st b₁ /\ {b₂} = {b₂} holds
b₂ in b₁

proof end;

theorem Th18: :: ZFMISC_1:18

for b₁, b₂ being set st {b₁} /\ {b₂} = {b₁} holds
b₁ = b₂

proof end;

Lemma18: for b₁, b₂ being set st b₁ in b₂ holds
b₂ /\ {b₁} = {b₁}

proof end;

theorem Th19: :: ZFMISC_1:19

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

proof end;

Lemma19: for b₁, b₂ being set holds
( {b₁} \ b₂ = {b₁} iff not b₁ in b₂ )

proof end;

theorem Th20: :: ZFMISC_1:20

for b₁, b₂ being set holds
( {b₁} \ {b₂} = {b₁} iff b₁ <> b₂ )

proof end;

Lemma20: for b₁, b₂ being set holds
( {b₁} \ b₂ = {} iff b₁ in b₂ )

proof end;

theorem Th21: :: ZFMISC_1:21

for b₁, b₂ being set st {b₁} \ {b₂} = {} holds
b₁ = b₂

proof end;

theorem Th22: :: ZFMISC_1:22

for b₁, b₂ being set holds {b₁} \ {b₁,b₂} = {}

proof end;

Lemma21: for b₁, b₂, b₃ being set holds
( {b₁,b₂} \ b₃ = {b₁} iff ( not b₁ in b₃ & ( b₂ in b₃ or b₁ = b₂ ) ) )

proof end;

theorem Th23: :: ZFMISC_1:23

for b₁, b₂ being set st b₁ <> b₂ holds
{b₁,b₂} \ {b₂} = {b₁}

proof end;

theorem Th24: :: ZFMISC_1:24

for b₁, b₂ being set st {b₁} c= {b₂} holds
b₁ = b₂ by Th6;

theorem Th25: :: ZFMISC_1:25

for b₁, b₂, b₃ being set holds
( not {b₁} c= {b₂,b₃} or b₁ = b₂ or b₁ = b₃ )

proof end;

theorem Th26: :: ZFMISC_1:26

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

proof end;

theorem Th27: :: ZFMISC_1:27

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

proof end;

Lemma23: for b₁, b₂ being set st b₁ <> {b₂} & b₁ <> {} holds
ex b₃ being set st
( b₃ in b₁ & b₃ <> b₂ )

proof end;

Lemma24: for b₁, b₂, b₃ being set holds
( b₁ c= {b₂,b₃} iff ( b₁ = {} or b₁ = {b₂} or b₁ = {b₃} or b₁ = {b₂,b₃} ) )

proof end;

theorem Th28: :: ZFMISC_1:28

for b₁, b₂, b₃, b₄ being set holds
( not {b₁,b₂} c= {b₃,b₄} or b₁ = b₃ or b₁ = b₄ )

proof end;

theorem Th29: :: ZFMISC_1:29

for b₁, b₂ being set st b₁ <> b₂ holds
{b₁} \+\ {b₂} = {b₁,b₂}

proof end;

theorem Th30: :: ZFMISC_1:30

for b₁ being set holds bool {b₁} = {{} ,{b₁}}

proof end;

Lemma25: for b₁, b₂ being set st b₁ in b₂ holds
b₁ c= union b₂

proof end;

theorem Th31: :: ZFMISC_1:31

for b₁ being set holds union {b₁} = b₁

proof end;

Lemma26: for b₁, b₂ being set holds union {b₁,b₂} = b₁ \/ b₂

proof end;

theorem Th32: :: ZFMISC_1:32

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

proof end;

theorem Th33: :: ZFMISC_1:33

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

proof end;

Lemma28: for b₁, b₂, b₃, b₄ being set holds
( [b₁,b₂] in [:b₃,b₄:] iff ( b₁ in b₃ & b₂ in b₄ ) )

proof end;

theorem Th34: :: ZFMISC_1:34

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

proof end;

theorem Th35: :: ZFMISC_1:35

for b₁, b₂ being set holds [:{b₁},{b₂}:] = {[b₁,b₂]}

proof end;

theorem Th36: :: ZFMISC_1:36

for b₁, b₂, b₃ being set holds
( [:{b₁},{b₂,b₃}:] = {[b₁,b₂],[b₁,b₃]} & [:{b₁,b₂},{b₃}:] = {[b₁,b₃],[b₂,b₃]} )

proof end;

theorem Th37: :: ZFMISC_1:37

for b₁, b₂ being set holds
( {b₁} c= b₂ iff b₁ in b₂ ) by Lemma2;

theorem Th38: :: ZFMISC_1:38

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

proof end;

theorem Th39: :: ZFMISC_1:39

for b₁, b₂ being set holds
( b₁ c= {b₂} iff ( b₁ = {} or b₁ = {b₂} ) ) by Lemma4;

theorem Th40: :: ZFMISC_1:40

for b₁, b₂, b₃ being set st b₁ c= b₂ & not b₃ in b₁ holds
b₁ c= b₂ \ {b₃} by Lemma3;

theorem Th41: :: ZFMISC_1:41

for b₁, b₂ being set st b₁ <> {b₂} & b₁ <> {} holds
ex b₃ being set st
( b₃ in b₁ & b₃ <> b₂ ) by Lemma23;

theorem Th42: :: ZFMISC_1:42

for b₁, b₂, b₃ being set holds
( b₁ c= {b₂,b₃} iff ( b₁ = {} or b₁ = {b₂} or b₁ = {b₃} or b₁ = {b₂,b₃} ) ) by Lemma24;

theorem Th43: :: ZFMISC_1:43

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

proof end;

theorem Th44: :: ZFMISC_1:44

for b₁, b₂, b₃ being set st {b₁} = b₂ \/ b₃ & b₂ <> b₃ & not b₂ = {} holds
b₃ = {}

proof end;

theorem Th45: :: ZFMISC_1:45

for b₁, b₂ being set st {b₁} \/ b₂ c= b₂ holds
b₁ in b₂ by Lemma12;

theorem Th46: :: ZFMISC_1:46

for b₁, b₂ being set st b₁ in b₂ holds
{b₁} \/ b₂ = b₂ by Lemma13;

theorem Th47: :: ZFMISC_1:47

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

proof end;

theorem Th48: :: ZFMISC_1:48

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

proof end;

theorem Th49: :: ZFMISC_1:49

for b₁, b₂ being set holds {b₁} \/ b₂ <> {}

proof end;

theorem Th50: :: ZFMISC_1:50

for b₁, b₂, b₃ being set holds {b₁,b₂} \/ b₃ <> {}

proof end;

theorem Th51: :: ZFMISC_1:51

for b₁, b₂ being set st b₁ /\ {b₂} = {b₂} holds
b₂ in b₁ by Lemma17;

theorem Th52: :: ZFMISC_1:52

for b₁, b₂ being set st b₁ in b₂ holds
b₂ /\ {b₁} = {b₁} by Lemma18;

theorem Th53: :: ZFMISC_1:53

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

proof end;

theorem Th54: :: ZFMISC_1:54

for b₁, b₂ being set st {b₁} misses b₂ holds
not b₁ in b₂ by Lemma14;

theorem Th55: :: ZFMISC_1:55

for b₁, b₂, b₃ being set st {b₁,b₂} misses b₃ holds
not b₁ in b₃

proof end;

theorem Th56: :: ZFMISC_1:56

for b₁, b₂ being set st not b₁ in b₂ holds
{b₁} misses b₂ by Lemma15;

theorem Th57: :: ZFMISC_1:57

for b₁, b₂, b₃ being set st not b₁ in b₂ & not b₃ in b₂ holds
{b₁,b₃} misses b₂

proof end;

theorem Th58: :: ZFMISC_1:58

for b₁, b₂ being set holds
( {b₁} misses b₂ or {b₁} /\ b₂ = {b₁} )

proof end;

theorem Th59: :: ZFMISC_1:59

for b₁, b₂, b₃ being set holds
( not {b₁,b₂} /\ b₃ = {b₁} or not b₂ in b₃ or b₁ = b₂ )

proof end;

theorem Th60: :: ZFMISC_1:60

for b₁, b₂, b₃ being set st b₁ in b₂ & ( not b₃ in b₂ or b₁ = b₃ ) holds
{b₁,b₃} /\ b₂ = {b₁}

proof end;

theorem Th61: :: ZFMISC_1:61

canceled;

theorem Th62: :: ZFMISC_1:62

canceled;

theorem Th63: :: ZFMISC_1:63

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

proof end;

theorem Th64: :: ZFMISC_1:64

for b₁, b₂, b₃ being set holds
( b₁ in b₂ \ {b₃} iff ( b₁ in b₂ & b₁ <> b₃ ) )

proof end;

theorem Th65: :: ZFMISC_1:65

for b₁, b₂ being set holds
( b₁ \ {b₂} = b₁ iff not b₂ in b₁ )

proof end;

theorem Th66: :: ZFMISC_1:66

for b₁, b₂ being set holds
( not b₁ \ {b₂} = {} or b₁ = {} or b₁ = {b₂} )

proof end;

theorem Th67: :: ZFMISC_1:67

for b₁, b₂ being set holds
( {b₁} \ b₂ = {b₁} iff not b₁ in b₂ ) by Lemma19;

theorem Th68: :: ZFMISC_1:68

for b₁, b₂ being set holds
( {b₁} \ b₂ = {} iff b₁ in b₂ ) by Lemma20;

theorem Th69: :: ZFMISC_1:69

for b₁, b₂ being set holds
( {b₁} \ b₂ = {} or {b₁} \ b₂ = {b₁} )

proof end;

theorem Th70: :: ZFMISC_1:70

for b₁, b₂, b₃ being set holds
( {b₁,b₂} \ b₃ = {b₁} iff ( not b₁ in b₃ & ( b₂ in b₃ or b₁ = b₂ ) ) ) by Lemma21;

theorem Th71: :: ZFMISC_1:71

canceled;

theorem Th72: :: ZFMISC_1:72

for b₁, b₂, b₃ being set holds
( {b₁,b₂} \ b₃ = {b₁,b₂} iff ( not b₁ in b₃ & not b₂ in b₃ ) )

proof end;

theorem Th73: :: ZFMISC_1:73

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

proof end;

theorem Th74: :: ZFMISC_1:74

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

proof end;

theorem Th75: :: ZFMISC_1:75

for b₁, b₂, b₃ being set holds
( b₁ \ {b₂,b₃} = {} iff ( b₁ = {} or b₁ = {b₂} or b₁ = {b₃} or b₁ = {b₂,b₃} ) )

proof end;

theorem Th76: :: ZFMISC_1:76

canceled;

theorem Th77: :: ZFMISC_1:77

canceled;

theorem Th78: :: ZFMISC_1:78

canceled;

theorem Th79: :: ZFMISC_1:79

for b₁, b₂ being set st b₁ c= b₂ holds
bool b₁ c= bool b₂

proof end;

theorem Th80: :: ZFMISC_1:80

for b₁ being set holds {b₁} c= bool b₁

proof end;

theorem Th81: :: ZFMISC_1:81

for b₁, b₂ being set holds (bool b₁) \/ (bool b₂) c= bool (b₁ \/ b₂)

proof end;

theorem Th82: :: ZFMISC_1:82

for b₁, b₂ being set st (bool b₁) \/ (bool b₂) = bool (b₁ \/ b₂) holds
b₁,b₂ are_c=-comparable

proof end;

theorem Th83: :: ZFMISC_1:83

for b₁, b₂ being set holds bool (b₁ /\ b₂) = (bool b₁) /\ (bool b₂)

proof end;

theorem Th84: :: ZFMISC_1:84

for b₁, b₂ being set holds bool (b₁ \ b₂) c= {{} } \/ ((bool b₁) \ (bool b₂))

proof end;

theorem Th85: :: ZFMISC_1:85

canceled;

theorem Th86: :: ZFMISC_1:86

for b₁, b₂ being set holds (bool (b₁ \ b₂)) \/ (bool (b₂ \ b₁)) c= bool (b₁ \+\ b₂)

proof end;

theorem Th87: :: ZFMISC_1:87

canceled;

theorem Th88: :: ZFMISC_1:88

canceled;

theorem Th89: :: ZFMISC_1:89

canceled;

theorem Th90: :: ZFMISC_1:90

canceled;

theorem Th91: :: ZFMISC_1:91

canceled;

theorem Th92: :: ZFMISC_1:92

for b₁, b₂ being set st b₁ in b₂ holds
b₁ c= union b₂ by Lemma25;

theorem Th93: :: ZFMISC_1:93

for b₁, b₂ being set holds union {b₁,b₂} = b₁ \/ b₂ by Lemma26;

theorem Th94: :: ZFMISC_1:94

for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
b₃ c= b₂ ) holds
union b₁ c= b₂

proof end;

theorem Th95: :: ZFMISC_1:95

for b₁, b₂ being set st b₁ c= b₂ holds
union b₁ c= union b₂

proof end;

theorem Th96: :: ZFMISC_1:96

for b₁, b₂ being set holds union (b₁ \/ b₂) = (union b₁) \/ (union b₂)

proof end;

theorem Th97: :: ZFMISC_1:97

for b₁, b₂ being set holds union (b₁ /\ b₂) c= (union b₁) /\ (union b₂)

proof end;

theorem Th98: :: ZFMISC_1:98

for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
b₃ misses b₂ ) holds
union b₁ misses b₂

proof end;

theorem Th99: :: ZFMISC_1:99

for b₁ being set holds union (bool b₁) = b₁

proof end;

theorem Th100: :: ZFMISC_1:100

for b₁ being set holds b₁ c= bool (union b₁)

proof end;

theorem Th101: :: ZFMISC_1:101

for b₁, b₂ being set st ( for b₃, b₄ being set st b₃ <> b₄ & b₃ in b₁ \/ b₂ & b₄ in b₁ \/ b₂ holds
b₃ misses b₄ ) holds
union (b₁ /\ b₂) = (union b₁) /\ (union b₂)

proof end;

theorem Th102: :: ZFMISC_1:102

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

proof end;

theorem Th103: :: ZFMISC_1:103

for b₁, b₂, b₃, b₄ being set st b₁ c= [:b₂,b₃:] & b₄ in b₁ holds
ex b₅, b₆ being set st
( b₅ in b₂ & b₆ in b₃ & b₄ = [b₅,b₆] )

proof end;

theorem Th104: :: ZFMISC_1:104

for b₁, b₂, b₃, b₄, b₅ being set st b₁ in [:b₂,b₃:] /\ [:b₄,b₅:] holds
ex b₆, b₇ being set st
( b₁ = [b₆,b₇] & b₆ in b₂ /\ b₄ & b₇ in b₃ /\ b₅ )

proof end;

theorem Th105: :: ZFMISC_1:105

for b₁, b₂ being set holds [:b₁,b₂:] c= bool (bool (b₁ \/ b₂))

proof end;

theorem Th106: :: ZFMISC_1:106

for b₁, b₂, b₃, b₄ being set holds
( [b₁,b₂] in [:b₃,b₄:] iff ( b₁ in b₃ & b₂ in b₄ ) ) by Lemma28;

theorem Th107: :: ZFMISC_1:107

for b₁, b₂, b₃, b₄ being set st [b₁,b₂] in [:b₃,b₄:] holds
[b₂,b₁] in [:b₄,b₃:]

proof end;

theorem Th108: :: ZFMISC_1:108

for b₁, b₂, b₃, b₄ being set st ( for b₅, b₆ being set holds
( [b₅,b₆] in [:b₁,b₂:] iff [b₅,b₆] in [:b₃,b₄:] ) ) holds
[:b₁,b₂:] = [:b₃,b₄:]

proof end;

theorem Th109: :: ZFMISC_1:109

for b₁, b₂, b₃, b₄ being set st b₁ c= [:b₂,b₃:] & ( for b₅, b₆ being set st [b₅,b₆] in b₁ holds
[b₅,b₆] in b₄ ) holds
b₁ c= b₄

proof end;

theorem Th110: :: ZFMISC_1:110

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ c= [:b₂,b₃:] & b₄ c= [:b₅,b₆:] & ( for b₇, b₈ being set holds
( [b₇,b₈] in b₁ iff [b₇,b₈] in b₄ ) ) holds
b₁ = b₄

proof end;

theorem Th111: :: ZFMISC_1:111

for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
ex b₄, b₅ being set st b₃ = [b₄,b₅] ) & ( for b₃, b₄ being set st [b₃,b₄] in b₁ holds
[b₃,b₄] in b₂ ) holds
b₁ c= b₂

proof end;

theorem Th112: :: ZFMISC_1:112

for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
ex b₄, b₅ being set st b₃ = [b₄,b₅] ) & ( for b₃ being set st b₃ in b₂ holds
ex b₄, b₅ being set st b₃ = [b₄,b₅] ) & ( for b₃, b₄ being set holds
( [b₃,b₄] in b₁ iff [b₃,b₄] in b₂ ) ) holds
b₁ = b₂

proof end;

theorem Th113: :: ZFMISC_1:113

for b₁, b₂ being set holds
( [:b₁,b₂:] = {} iff ( b₁ = {} or b₂ = {} ) )

proof end;

theorem Th114: :: ZFMISC_1:114

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} & [:b₁,b₂:] = [:b₂,b₁:] holds
b₁ = b₂

proof end;

theorem Th115: :: ZFMISC_1:115

for b₁, b₂ being set st [:b₁,b₁:] = [:b₂,b₂:] holds
b₁ = b₂

proof end;

theorem Th116: :: ZFMISC_1:116

for b₁ being set st b₁ c= [:b₁,b₁:] holds
b₁ = {}

proof end;

theorem Th117: :: ZFMISC_1:117

for b₁, b₂, b₃ being set st b₁ <> {} & ( [:b₂,b₁:] c= [:b₃,b₁:] or [:b₁,b₂:] c= [:b₁,b₃:] ) holds
b₂ c= b₃

proof end;

theorem Th118: :: ZFMISC_1:118

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
( [:b₁,b₃:] c= [:b₂,b₃:] & [:b₃,b₁:] c= [:b₃,b₂:] )

proof end;

theorem Th119: :: ZFMISC_1:119

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
[:b₁,b₃:] c= [:b₂,b₄:]

proof end;

theorem Th120: :: ZFMISC_1:120

for b₁, b₂, b₃ being set holds
( [:(b₁ \/ b₂),b₃:] = [:b₁,b₃:] \/ [:b₂,b₃:] & [:b₃,(b₁ \/ b₂):] = [:b₃,b₁:] \/ [:b₃,b₂:] )

proof end;

theorem Th121: :: ZFMISC_1:121

for b₁, b₂, b₃, b₄ being set holds [:(b₁ \/ b₂),(b₃ \/ b₄):] = (([:b₁,b₃:] \/ [:b₁,b₄:]) \/ [:b₂,b₃:]) \/ [:b₂,b₄:]

proof end;

theorem Th122: :: ZFMISC_1:122

for b₁, b₂, b₃ being set holds
( [:(b₁ /\ b₂),b₃:] = [:b₁,b₃:] /\ [:b₂,b₃:] & [:b₃,(b₁ /\ b₂):] = [:b₃,b₁:] /\ [:b₃,b₂:] )

proof end;

theorem Th123: :: ZFMISC_1:123

for b₁, b₂, b₃, b₄ being set holds [:(b₁ /\ b₂),(b₃ /\ b₄):] = [:b₁,b₃:] /\ [:b₂,b₄:]

proof end;

theorem Th124: :: ZFMISC_1:124

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
[:b₁,b₄:] /\ [:b₂,b₃:] = [:b₁,b₃:]

proof end;

theorem Th125: :: ZFMISC_1:125

for b₁, b₂, b₃ being set holds
( [:(b₁ \ b₂),b₃:] = [:b₁,b₃:] \ [:b₂,b₃:] & [:b₃,(b₁ \ b₂):] = [:b₃,b₁:] \ [:b₃,b₂:] )

proof end;

theorem Th126: :: ZFMISC_1:126

for b₁, b₂, b₃, b₄ being set holds [:b₁,b₂:] \ [:b₃,b₄:] = [:(b₁ \ b₃),b₂:] \/ [:b₁,(b₂ \ b₄):]

proof end;

theorem Th127: :: ZFMISC_1:127

for b₁, b₂, b₃, b₄ being set st ( b₁ misses b₂ or b₃ misses b₄ ) holds
[:b₁,b₃:] misses [:b₂,b₄:]

proof end;

theorem Th128: :: ZFMISC_1:128

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

proof end;

theorem Th129: :: ZFMISC_1:129

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

proof end;

theorem Th130: :: ZFMISC_1:130

for b₁, b₂ being set st b₁ <> {} holds
( [:{b₂},b₁:] <> {} & [:b₁,{b₂}:] <> {} )

proof end;

theorem Th131: :: ZFMISC_1:131

for b₁, b₂, b₃, b₄ being set st b₁ <> b₂ holds
( [:{b₁},b₃:] misses [:{b₂},b₄:] & [:b₃,{b₁}:] misses [:b₄,{b₂}:] )

proof end;

theorem Th132: :: ZFMISC_1:132

for b₁, b₂, b₃ being set holds
( [:{b₁,b₂},b₃:] = [:{b₁},b₃:] \/ [:{b₂},b₃:] & [:b₃,{b₁,b₂}:] = [:b₃,{b₁}:] \/ [:b₃,{b₂}:] )

proof end;

theorem Th133: :: ZFMISC_1:133

canceled;

theorem Th134: :: ZFMISC_1:134

for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₂ <> {} & [:b₁,b₂:] = [:b₃,b₄:] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th135: :: ZFMISC_1:135

for b₁, b₂ being set st ( b₁ c= [:b₁,b₂:] or b₁ c= [:b₂,b₁:] ) holds
b₁ = {}

proof end;

theorem Th136: :: ZFMISC_1:136

for b₁ being set ex b₂ being set st
( b₁ in b₂ & ( for b₃, b₄ being set st b₃ in b₂ & b₄ c= b₃ holds
b₄ in b₂ ) & ( for b₃ being set st b₃ in b₂ holds
bool b₃ in b₂ ) & ( for b₃ being set holds
( not b₃ c= b₂ or b₃,b₂ are_equipotent or b₃ in b₂ ) ) )

proof end;

theorem Th137: :: ZFMISC_1:137

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

proof end;

theorem Th138: :: ZFMISC_1:138

for b₁, b₂, b₃, b₄ being set st [:b₁,b₂:] c= [:b₃,b₄:] & [:b₁,b₂:] <> {} holds
( b₁ c= b₃ & b₂ c= b₄ )

proof end;

theorem Th139: :: ZFMISC_1:139

for b₁ being non empty set
for b₂, b₃, b₄ being set st ( [:b₁,b₂:] c= [:b₃,b₄:] or [:b₂,b₁:] c= [:b₄,b₃:] ) holds
b₂ c= b₄

proof end;

theorem Th140: :: ZFMISC_1:140

for b₁, b₂ being set st b₁ in b₂ holds
(b₂ \ {b₁}) \/ {b₁} = b₂

proof end;

theorem Th141: :: ZFMISC_1:141

for b₁, b₂ being set st not b₁ in b₂ holds
(b₂ \/ {b₁}) \ {b₁} = b₂

proof end;