:: Boolean Properties of Sets - Theorems
:: by Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: XBOOLE_1:1
for
X,
Y,
Z being
set st
X c= Y &
Y c= Z holds
X c= Z
theorem Th2: :: XBOOLE_1:2
theorem Th3: :: XBOOLE_1:3
theorem Th4: :: XBOOLE_1:4
theorem :: XBOOLE_1:5
theorem :: XBOOLE_1:6
theorem Th7: :: XBOOLE_1:7
for
X,
Y being
set holds
X c= X \/ Y
theorem Th8: :: XBOOLE_1:8
for
X,
Z,
Y being
set st
X c= Z &
Y c= Z holds
X \/ Y c= Z
theorem :: XBOOLE_1:9
theorem :: XBOOLE_1:10
for
X,
Y,
Z being
set st
X c= Y holds
X c= Z \/ Y
theorem :: XBOOLE_1:11
for
X,
Y,
Z being
set st
X \/ Y c= Z holds
X c= Z
theorem Th12: :: XBOOLE_1:12
for
X,
Y being
set st
X c= Y holds
X \/ Y = Y
theorem :: XBOOLE_1:13
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X \/ Z c= Y \/ V
theorem :: XBOOLE_1:14
for
Y,
X,
Z being
set st
Y c= X &
Z c= X & ( for
V being
set st
Y c= V &
Z c= V holds
X c= V ) holds
X = Y \/ Z
theorem :: XBOOLE_1:15
theorem Th16: :: XBOOLE_1:16
theorem Th17: :: XBOOLE_1:17
for
X,
Y being
set holds
X /\ Y c= X
theorem :: XBOOLE_1:18
for
X,
Y,
Z being
set st
X c= Y /\ Z holds
X c= Y
theorem Th19: :: XBOOLE_1:19
for
Z,
X,
Y being
set st
Z c= X &
Z c= Y holds
Z c= X /\ Y
theorem :: XBOOLE_1:20
for
X,
Y,
Z being
set st
X c= Y &
X c= Z & ( for
V being
set st
V c= Y &
V c= Z holds
V c= X ) holds
X = Y /\ Z
theorem :: XBOOLE_1:21
for
X,
Y being
set holds
X /\ (X \/ Y) = X
theorem Th22: :: XBOOLE_1:22
for
X,
Y being
set holds
X \/ (X /\ Y) = X
theorem Th23: :: XBOOLE_1:23
theorem Th24: :: XBOOLE_1:24
theorem :: XBOOLE_1:25
theorem Th26: :: XBOOLE_1:26
theorem :: XBOOLE_1:27
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X /\ Z c= Y /\ V
theorem Th28: :: XBOOLE_1:28
for
X,
Y being
set st
X c= Y holds
X /\ Y = X
theorem :: XBOOLE_1:29
theorem :: XBOOLE_1:30
theorem :: XBOOLE_1:31
Lm1:
for X, Y being set holds
( X \ Y = {} iff X c= Y )
theorem :: XBOOLE_1:32
for
X,
Y being
set st
X \ Y = Y \ X holds
X = Y
theorem Th33: :: XBOOLE_1:33
for
X,
Y,
Z being
set st
X c= Y holds
X \ Z c= Y \ Z
theorem Th34: :: XBOOLE_1:34
for
X,
Y,
Z being
set st
X c= Y holds
Z \ Y c= Z \ X
Lm2:
for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
theorem :: XBOOLE_1:35
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X \ V c= Y \ Z
theorem Th36: :: XBOOLE_1:36
for
X,
Y being
set holds
X \ Y c= X
theorem :: XBOOLE_1:37
theorem :: XBOOLE_1:38
for
X,
Y being
set st
X c= Y \ X holds
X = {}
theorem Th39: :: XBOOLE_1:39
for
X,
Y being
set holds
X \/ (Y \ X) = X \/ Y
theorem :: XBOOLE_1:40
for
X,
Y being
set holds
(X \/ Y) \ Y = X \ Y
theorem Th41: :: XBOOLE_1:41
for
X,
Y,
Z being
set holds
(X \ Y) \ Z = X \ (Y \/ Z)
theorem Th42: :: XBOOLE_1:42
for
X,
Y,
Z being
set holds
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
theorem :: XBOOLE_1:43
for
X,
Y,
Z being
set st
X c= Y \/ Z holds
X \ Y c= Z
theorem :: XBOOLE_1:44
for
X,
Y,
Z being
set st
X \ Y c= Z holds
X c= Y \/ Z
theorem :: XBOOLE_1:45
for
X,
Y being
set st
X c= Y holds
Y = X \/ (Y \ X)
theorem :: XBOOLE_1:46
theorem Th47: :: XBOOLE_1:47
for
X,
Y being
set holds
X \ (X /\ Y) = X \ Y
theorem :: XBOOLE_1:48
for
X,
Y being
set holds
X \ (X \ Y) = X /\ Y
theorem Th49: :: XBOOLE_1:49
for
X,
Y,
Z being
set holds
X /\ (Y \ Z) = (X /\ Y) \ Z
theorem Th50: :: XBOOLE_1:50
for
X,
Y,
Z being
set holds
X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
theorem Th51: :: XBOOLE_1:51
for
X,
Y being
set holds
(X /\ Y) \/ (X \ Y) = X
theorem Th52: :: XBOOLE_1:52
for
X,
Y,
Z being
set holds
X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
theorem :: XBOOLE_1:53
for
X,
Y,
Z being
set holds
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
theorem :: XBOOLE_1:54
theorem Th55: :: XBOOLE_1:55
for
X,
Y being
set holds
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
Lm3:
for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z
theorem :: XBOOLE_1:56
for
X,
Y,
Z being
set st
X c< Y &
Y c< Z holds
X c< Z
theorem :: XBOOLE_1:57
for
X,
Y being
set holds
( not
X c< Y or not
Y c< X ) ;
theorem :: XBOOLE_1:58
for
X,
Y,
Z being
set st
X c< Y &
Y c= Z holds
X c< Z
theorem :: XBOOLE_1:59
for
X,
Y,
Z being
set st
X c= Y &
Y c< Z holds
X c< Z by Lm3;
theorem Th60: :: XBOOLE_1:60
for
X,
Y being
set st
X c= Y holds
not
Y c< X
theorem :: XBOOLE_1:61
theorem :: XBOOLE_1:62
theorem Th63: :: XBOOLE_1:63
theorem :: XBOOLE_1:64
theorem :: XBOOLE_1:65
theorem :: XBOOLE_1:66
theorem :: XBOOLE_1:67
theorem :: XBOOLE_1:68
theorem :: XBOOLE_1:69
theorem Th70: :: XBOOLE_1:70
theorem :: XBOOLE_1:71
theorem :: XBOOLE_1:72
theorem :: XBOOLE_1:73
theorem Th74: :: XBOOLE_1:74
theorem :: XBOOLE_1:75
theorem :: XBOOLE_1:76
theorem :: XBOOLE_1:77
theorem :: XBOOLE_1:78
theorem Th79: :: XBOOLE_1:79
theorem :: XBOOLE_1:80
theorem :: XBOOLE_1:81
theorem :: XBOOLE_1:82
theorem Th83: :: XBOOLE_1:83
theorem :: XBOOLE_1:84
theorem :: XBOOLE_1:85
theorem Th86: :: XBOOLE_1:86
theorem :: XBOOLE_1:87
theorem Th88: :: XBOOLE_1:88
theorem Th89: :: XBOOLE_1:89
theorem :: XBOOLE_1:90
theorem :: XBOOLE_1:91
theorem :: XBOOLE_1:92
theorem Th93: :: XBOOLE_1:93
Lm4:
for X, Y being set holds X /\ Y misses X \+\ Y
Lm5:
for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y)
theorem :: XBOOLE_1:94
theorem :: XBOOLE_1:95
theorem :: XBOOLE_1:96
theorem :: XBOOLE_1:97
theorem :: XBOOLE_1:98
theorem :: XBOOLE_1:99
theorem :: XBOOLE_1:100
theorem :: XBOOLE_1:101
theorem :: XBOOLE_1:102
theorem :: XBOOLE_1:103
theorem :: XBOOLE_1:104
theorem :: XBOOLE_1:105
theorem Th106: :: XBOOLE_1:106
theorem :: XBOOLE_1:107
theorem :: XBOOLE_1:108
for
X,
A,
Y being
set st
X c= A holds
X /\ Y c= A
theorem Th109: :: XBOOLE_1:109
for
X,
A,
Y being
set st
X c= A holds
X \ Y c= A
theorem :: XBOOLE_1:110
theorem Th111: :: XBOOLE_1:111
for
X,
Z,
Y being
set holds
(X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
theorem :: XBOOLE_1:112
theorem :: XBOOLE_1:113
theorem :: XBOOLE_1:114
theorem :: XBOOLE_1:115