:: by Czes{\l}aw Byli\'nski

::

:: Received February 1, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

Lm1: for x, X being set holds

( {x} c= X iff x in X )

proof end;

Lm2: for Y, X, x being set st Y c= X & not x in Y holds

Y c= X \ {x}

proof end;

Lm3: for Y, x being set holds

( Y c= {x} iff ( Y = {} or Y = {x} ) )

proof end;

definition

let X be set ;

defpred S_{1}[ set ] means $1 c= X;

func bool X -> set means :Def1: :: ZFMISC_1:def 1

for Z being set holds

( Z in it iff Z c= X );

existence

ex b_{1} being set st

for Z being set holds

( Z in b_{1} iff Z c= X )

for b_{1}, b_{2} being set st ( for Z being set holds

( Z in b_{1} iff Z c= X ) ) & ( for Z being set holds

( Z in b_{2} iff Z c= X ) ) holds

b_{1} = b_{2}

end;
defpred S

func bool X -> set means :Def1: :: ZFMISC_1:def 1

for Z being set holds

( Z in it iff Z c= X );

existence

ex b

for Z being set holds

( Z in b

proof end;

uniqueness for b

( Z in b

( Z in b

b

proof end;

:: deftheorem Def1 defines bool ZFMISC_1:def 1 :

for X being set

for b

( b

( Z in b

definition

let X1, X2 be set ;

defpred S_{1}[ set ] means ex x, y being set st

( x in X1 & y in X2 & $1 = [x,y] );

func [:X1,X2:] -> set means :Def2: :: ZFMISC_1:def 2

for z being set holds

( z in it iff ex x, y being set st

( x in X1 & y in X2 & z = [x,y] ) );

existence

ex b_{1} being set st

for z being set holds

( z in b_{1} iff ex x, y being set st

( x in X1 & y in X2 & z = [x,y] ) )

for b_{1}, b_{2} being set st ( for z being set holds

( z in b_{1} iff ex x, y being set st

( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being set holds

( z in b_{2} iff ex x, y being set st

( x in X1 & y in X2 & z = [x,y] ) ) ) holds

b_{1} = b_{2}

end;
defpred S

( x in X1 & y in X2 & $1 = [x,y] );

func [:X1,X2:] -> set means :Def2: :: ZFMISC_1:def 2

for z being set holds

( z in it iff ex x, y being set st

( x in X1 & y in X2 & z = [x,y] ) );

existence

ex b

for z being set holds

( z in b

( x in X1 & y in X2 & z = [x,y] ) )

proof end;

uniqueness for b

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being set holds

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) ) holds

b

proof end;

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

for X1, X2 being set

for b

( b

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) );

definition

let X1, X2, X3 be set ;

func [:X1,X2,X3:] -> set equals :: ZFMISC_1:def 3

[:[:X1,X2:],X3:];

coherence

[:[:X1,X2:],X3:] is set ;

end;
func [:X1,X2,X3:] -> set equals :: ZFMISC_1:def 3

[:[:X1,X2:],X3:];

coherence

[:[:X1,X2:],X3:] is set ;

:: deftheorem defines [: ZFMISC_1:def 3 :

for X1, X2, X3 being set holds [:X1,X2,X3:] = [:[:X1,X2:],X3:];

definition

let X1, X2, X3, X4 be set ;

func [:X1,X2,X3,X4:] -> set equals :: ZFMISC_1:def 4

[:[:X1,X2,X3:],X4:];

coherence

[:[:X1,X2,X3:],X4:] is set ;

end;
func [:X1,X2,X3,X4:] -> set equals :: ZFMISC_1:def 4

[:[:X1,X2,X3:],X4:];

coherence

[:[:X1,X2,X3:],X4:] is set ;

:: deftheorem defines [: ZFMISC_1:def 4 :

for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];

begin

theorem :: ZFMISC_1:1

proof end;

theorem :: ZFMISC_1:2

proof end;

theorem :: ZFMISC_1:3

canceled;

theorem :: ZFMISC_1:4

canceled;

theorem :: ZFMISC_1:5

canceled;

theorem Th6: :: ZFMISC_1:6

proof end;

theorem :: ZFMISC_1:7

canceled;

theorem Th8: :: ZFMISC_1:8

proof end;

theorem Th9: :: ZFMISC_1:9

proof end;

theorem Th10: :: ZFMISC_1:10

proof end;

theorem :: ZFMISC_1:11

canceled;

theorem Th12: :: ZFMISC_1:12

proof end;

Lm4: for x, X being set st {x} \/ X c= X holds

x in X

proof end;

theorem :: ZFMISC_1:13

proof end;

Lm5: for x, X being set st x in X holds

{x} \/ X = X

proof end;

theorem :: ZFMISC_1:14

proof end;

Lm6: for x, X being set st {x} misses X holds

not x in X

proof end;

theorem :: ZFMISC_1:15

canceled;

theorem :: ZFMISC_1:16

proof end;

Lm7: for x, X being set st not x in X holds

{x} misses X

proof end;

theorem Th17: :: ZFMISC_1:17

proof end;

Lm8: for X, x being set st X /\ {x} = {x} holds

x in X

proof end;

theorem :: ZFMISC_1:18

proof end;

Lm9: for x, X being set st x in X holds

X /\ {x} = {x}

proof end;

theorem :: ZFMISC_1:19

proof end;

Lm10: for x, X being set holds

( {x} \ X = {x} iff not x in X )

proof end;

theorem :: ZFMISC_1:20

proof end;

Lm11: for x, X being set holds

( {x} \ X = {} iff x in X )

proof end;

theorem :: ZFMISC_1:21

proof end;

theorem :: ZFMISC_1:22

proof end;

Lm12: for x, y, X being set holds

( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )

proof end;

theorem :: ZFMISC_1:23

proof end;

theorem :: ZFMISC_1:24

theorem :: ZFMISC_1:25

proof end;

theorem Th26: :: ZFMISC_1:26

proof end;

theorem :: ZFMISC_1:27

proof end;

Lm13: for X, x being set st X <> {x} & X <> {} holds

ex y being set st

( y in X & y <> x )

proof end;

Lm14: for Z, x1, x2 being set holds

( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )

proof end;

theorem :: ZFMISC_1:28

proof end;

theorem :: ZFMISC_1:29

proof end;

theorem :: ZFMISC_1:30

proof end;

Lm15: for X, A being set st X in A holds

X c= union A

proof end;

theorem :: ZFMISC_1:31

proof end;

Lm16: for X, Y being set holds union {X,Y} = X \/ Y

proof end;

theorem :: ZFMISC_1:32

proof end;

theorem Th33: :: ZFMISC_1:33

proof end;

Lm17: for x, y, X, Y being set holds

( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )

proof end;

theorem :: ZFMISC_1:34

proof end;

theorem :: ZFMISC_1:35

proof end;

theorem Th36: :: ZFMISC_1:36

proof end;

theorem :: ZFMISC_1:37

theorem Th38: :: ZFMISC_1:38

proof end;

theorem :: ZFMISC_1:39

theorem :: ZFMISC_1:40

theorem :: ZFMISC_1:41

theorem :: ZFMISC_1:42

for Z, x1, x2 being set holds

( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ) by Lm14;

( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ) by Lm14;

theorem Th43: :: ZFMISC_1:43

for z, X, Y being set holds

( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )

( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )

proof end;

theorem :: ZFMISC_1:44

proof end;

theorem :: ZFMISC_1:45

theorem :: ZFMISC_1:46

theorem :: ZFMISC_1:47

proof end;

theorem :: ZFMISC_1:48

proof end;

theorem :: ZFMISC_1:49

theorem :: ZFMISC_1:50

theorem :: ZFMISC_1:51

theorem :: ZFMISC_1:52

theorem :: ZFMISC_1:53

proof end;

theorem :: ZFMISC_1:54

theorem Th55: :: ZFMISC_1:55

proof end;

theorem :: ZFMISC_1:56

theorem Th57: :: ZFMISC_1:57

proof end;

theorem :: ZFMISC_1:58

theorem :: ZFMISC_1:59

proof end;

theorem :: ZFMISC_1:60

proof end;

theorem :: ZFMISC_1:61

canceled;

theorem :: ZFMISC_1:62

canceled;

theorem :: ZFMISC_1:63

proof end;

theorem Th64: :: ZFMISC_1:64

proof end;

theorem Th65: :: ZFMISC_1:65

proof end;

theorem :: ZFMISC_1:66

proof end;

theorem :: ZFMISC_1:67

theorem :: ZFMISC_1:68

theorem :: ZFMISC_1:69

proof end;

theorem :: ZFMISC_1:70

theorem :: ZFMISC_1:71

canceled;

theorem Th72: :: ZFMISC_1:72

proof end;

theorem Th73: :: ZFMISC_1:73

proof end;

theorem :: ZFMISC_1:74

for x, y, X being set holds

( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )

( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )

proof end;

theorem :: ZFMISC_1:75

proof end;

theorem :: ZFMISC_1:76

canceled;

theorem :: ZFMISC_1:77

canceled;

theorem :: ZFMISC_1:78

canceled;

theorem :: ZFMISC_1:79

proof end;

theorem :: ZFMISC_1:80

proof end;

theorem :: ZFMISC_1:81

proof end;

theorem :: ZFMISC_1:82

proof end;

theorem :: ZFMISC_1:83

proof end;

theorem :: ZFMISC_1:84

proof end;

theorem :: ZFMISC_1:85

canceled;

theorem :: ZFMISC_1:86

proof end;

theorem :: ZFMISC_1:87

canceled;

theorem :: ZFMISC_1:88

canceled;

theorem :: ZFMISC_1:89

canceled;

theorem :: ZFMISC_1:90

canceled;

theorem :: ZFMISC_1:91

canceled;

theorem :: ZFMISC_1:92

theorem :: ZFMISC_1:93

theorem :: ZFMISC_1:94

proof end;

theorem Th95: :: ZFMISC_1:95

proof end;

theorem :: ZFMISC_1:96

proof end;

theorem Th97: :: ZFMISC_1:97

proof end;

theorem Th98: :: ZFMISC_1:98

proof end;

theorem :: ZFMISC_1:99

proof end;

theorem :: ZFMISC_1:100

proof end;

theorem :: ZFMISC_1:101

for A, B being set st ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds

X misses Y ) holds

union (A /\ B) = (union A) /\ (union B)

X misses Y ) holds

union (A /\ B) = (union A) /\ (union B)

proof end;

theorem :: ZFMISC_1:102

canceled;

theorem Th103: :: ZFMISC_1:103

for A, X, Y, z being set st A c= [:X,Y:] & z in A holds

ex x, y being set st

( x in X & y in Y & z = [x,y] )

ex x, y being set st

( x in X & y in Y & z = [x,y] )

proof end;

theorem Th104: :: ZFMISC_1:104

for z, X1, Y1, X2, Y2 being set st z in [:X1,Y1:] /\ [:X2,Y2:] holds

ex x, y being set st

( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )

ex x, y being set st

( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )

proof end;

theorem :: ZFMISC_1:105

proof end;

theorem :: ZFMISC_1:106

theorem Th107: :: ZFMISC_1:107

proof end;

theorem :: ZFMISC_1:108

for X1, Y1, X2, Y2 being set st ( for x, y being set holds

( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) holds

[:X1,Y1:] = [:X2,Y2:]

( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) holds

[:X1,Y1:] = [:X2,Y2:]

proof end;

Lm18: for A, X1, Y1, B, X2, Y2 being set st A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being set holds

( [x,y] in A iff [x,y] in B ) ) holds

A = B

proof end;

Lm19: for A, B being set st ( for z being set st z in A holds

ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds

ex x, y being set st z = [x,y] ) & ( for x, y being set holds

( [x,y] in A iff [x,y] in B ) ) holds

A = B

proof end;

theorem :: ZFMISC_1:109

canceled;

theorem :: ZFMISC_1:110

canceled;

theorem :: ZFMISC_1:111

canceled;

theorem :: ZFMISC_1:112

canceled;

theorem Th113: :: ZFMISC_1:113

proof end;

theorem :: ZFMISC_1:114

proof end;

theorem :: ZFMISC_1:115

proof end;

Lm20: for z, X, Y being set st z in [:X,Y:] holds

ex x, y being set st [x,y] = z

proof end;

theorem :: ZFMISC_1:116

proof end;

theorem :: ZFMISC_1:117

proof end;

theorem Th118: :: ZFMISC_1:118

proof end;

theorem Th119: :: ZFMISC_1:119

proof end;

theorem Th120: :: ZFMISC_1:120

for X, Y, Z being set holds

( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )

( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:121

for X1, X2, Y1, Y2 being set holds [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:122

for X, Y, Z being set holds

( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )

( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )

proof end;

theorem Th123: :: ZFMISC_1:123

proof end;

theorem :: ZFMISC_1:124

proof end;

theorem Th125: :: ZFMISC_1:125

for X, Y, Z being set holds

( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )

( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:126

proof end;

theorem Th127: :: ZFMISC_1:127

proof end;

theorem Th128: :: ZFMISC_1:128

proof end;

theorem Th129: :: ZFMISC_1:129

proof end;

theorem :: ZFMISC_1:130

theorem :: ZFMISC_1:131

for x, y, X, Y being set st x <> y holds

( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )

( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )

proof end;

theorem :: ZFMISC_1:132

for x, y, X being set holds

( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )

( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )

proof end;

theorem :: ZFMISC_1:133

canceled;

theorem Th134: :: ZFMISC_1:134

for X1, Y1, X2, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds

( X1 = X2 & Y1 = Y2 )

( X1 = X2 & Y1 = Y2 )

proof end;

theorem :: ZFMISC_1:135

proof end;

theorem :: ZFMISC_1:136

for N being set ex M being set st

( N in M & ( for X, Y being set st X in M & Y c= X holds

Y in M ) & ( for X being set st X in M holds

bool X in M ) & ( for X being set holds

( not X c= M or X,M are_equipotent or X in M ) ) )

( N in M & ( for X, Y being set st X in M & Y c= X holds

Y in M ) & ( for X being set st X in M holds

bool X in M ) & ( for X being set holds

( not X c= M or X,M are_equipotent or X in M ) ) )

proof end;

theorem :: ZFMISC_1:137

for e, X1, Y1, X2, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds

e in [:(X1 /\ X2),(Y1 /\ Y2):]

e in [:(X1 /\ X2),(Y1 /\ Y2):]

proof end;

begin

theorem Th138: :: ZFMISC_1:138

for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} holds

( X1 c= Y1 & X2 c= Y2 )

( X1 c= Y1 & X2 c= Y2 )

proof end;

theorem :: ZFMISC_1:139

for A being non empty set

for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds

B c= D

for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds

B c= D

proof end;

theorem :: ZFMISC_1:140

proof end;

theorem :: ZFMISC_1:141

proof end;

theorem :: ZFMISC_1:142

for x, y, z, Z being set holds

( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )

( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )

proof end;

theorem :: ZFMISC_1:143

for N, M, X1, Y1, X2, Y2 being set st N c= [:X1,Y1:] & M c= [:X2,Y2:] holds

N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]

N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]

proof end;

Lm21: for x, y, X being set st not x in X & not y in X holds

{x,y} misses X

proof end;

theorem Th144: :: ZFMISC_1:144

proof end;

theorem :: ZFMISC_1:145

proof end;

definition

let x1, x2, x3 be set ;

pred x1,x2,x3 are_mutually_different means :: ZFMISC_1:def 5

( x1 <> x2 & x1 <> x3 & x2 <> x3 );

end;
pred x1,x2,x3 are_mutually_different means :: ZFMISC_1:def 5

( x1 <> x2 & x1 <> x3 & x2 <> x3 );

:: deftheorem defines are_mutually_different ZFMISC_1:def 5 :

for x1, x2, x3 being set holds

( x1,x2,x3 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) );

definition

let x1, x2, x3, x4 be set ;

pred x1,x2,x3,x4 are_mutually_different means :: ZFMISC_1:def 6

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );

end;
pred x1,x2,x3,x4 are_mutually_different means :: ZFMISC_1:def 6

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );

:: deftheorem defines are_mutually_different ZFMISC_1:def 6 :

for x1, x2, x3, x4 being set holds

( x1,x2,x3,x4 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) );

definition

let x1, x2, x3, x4, x5 be set ;

pred x1,x2,x3,x4,x5 are_mutually_different means :: ZFMISC_1:def 7

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 );

end;
pred x1,x2,x3,x4,x5 are_mutually_different means :: ZFMISC_1:def 7

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 );

:: deftheorem defines are_mutually_different ZFMISC_1:def 7 :

for x1, x2, x3, x4, x5 being set holds

( x1,x2,x3,x4,x5 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 ) );

definition

let x1, x2, x3, x4, x5, x6 be set ;

pred x1,x2,x3,x4,x5,x6 are_mutually_different means :: ZFMISC_1:def 8

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 );

end;
pred x1,x2,x3,x4,x5,x6 are_mutually_different means :: ZFMISC_1:def 8

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 );

:: deftheorem defines are_mutually_different ZFMISC_1:def 8 :

for x1, x2, x3, x4, x5, x6 being set holds

( x1,x2,x3,x4,x5,x6 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 ) );

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;

pred x1,x2,x3,x4,x5,x6,x7 are_mutually_different means :: ZFMISC_1:def 9

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 );

end;
pred x1,x2,x3,x4,x5,x6,x7 are_mutually_different means :: ZFMISC_1:def 9

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 );

:: deftheorem defines are_mutually_different ZFMISC_1:def 9 :

for x1, x2, x3, x4, x5, x6, x7 being set holds

( x1,x2,x3,x4,x5,x6,x7 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 ) );

theorem :: ZFMISC_1:146

proof end;

theorem :: ZFMISC_1:147

definition

let X be set ;

attr X is trivial means :: ZFMISC_1:def 10

for x, y being set st x in X & y in X holds

x = y;

end;
attr X is trivial means :: ZFMISC_1:def 10

for x, y being set st x in X & y in X holds

x = y;

:: deftheorem defines trivial ZFMISC_1:def 10 :

for X being set holds

( X is trivial iff for x, y being set st x in X & y in X holds

x = y );

registration

cluster empty -> trivial set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is trivial

end;
coherence

for b

b

proof end;

theorem :: ZFMISC_1:148

proof end;

theorem :: ZFMISC_1:149

proof end;

theorem :: ZFMISC_1:150

canceled;

theorem :: ZFMISC_1:151

for A, B being set st ( for x, y being set st x in A & y in B holds

x misses y ) holds

union A misses union B

x misses y ) holds

union A misses union B

proof end;

registration
end;

registration
end;

theorem :: ZFMISC_1:152

proof end;

theorem :: ZFMISC_1:153

proof end;

theorem :: ZFMISC_1:154

proof end;