:: Boolean Properties of Sets - Theorems
:: by Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
registrations XBOOLE_0;
requirements BOOLE;
begin
reserve x,A,B,X,X9,Y,Y9,Z,V for set;
::$N Modus Barbara
theorem :: XBOOLE_1:1
X c= Y & Y c= Z implies X c= Z;
theorem :: XBOOLE_1:2
{} c= X;
theorem :: XBOOLE_1:3
X c= {} implies X = {};
theorem :: XBOOLE_1:4
(X \/ Y) \/ Z = X \/ (Y \/ Z);
theorem :: XBOOLE_1:5
(X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z);
theorem :: XBOOLE_1:6
X \/ (X \/ Y) = X \/ Y;
theorem :: XBOOLE_1:7
X c= X \/ Y;
theorem :: XBOOLE_1:8
X c= Z & Y c= Z implies X \/ Y c= Z;
theorem :: XBOOLE_1:9
X c= Y implies X \/ Z c= Y \/ Z;
theorem :: XBOOLE_1:10
X c= Y implies X c= Z \/ Y;
theorem :: XBOOLE_1:11
X \/ Y c= Z implies X c= Z;
theorem :: XBOOLE_1:12
X c= Y implies X \/ Y = Y;
theorem :: XBOOLE_1:13
X c= Y & Z c= V implies X \/ Z c= Y \/ V;
theorem :: XBOOLE_1:14
(Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = Y \/ Z;
theorem :: XBOOLE_1:15
X \/ Y = {} implies X = {};
theorem :: XBOOLE_1:16
(X /\ Y) /\ Z = X /\ (Y /\ Z);
theorem :: XBOOLE_1:17
X /\ Y c= X;
theorem :: XBOOLE_1:18
X c= Y /\ Z implies X c= Y;
theorem :: XBOOLE_1:19
Z c= X & Z c= Y implies Z c= X /\ Y;
theorem :: XBOOLE_1:20
(X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = Y /\ Z;
theorem :: XBOOLE_1:21
X /\ (X \/ Y) = X;
theorem :: XBOOLE_1:22
X \/ (X /\ Y) = X;
theorem :: XBOOLE_1:23
X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;
theorem :: XBOOLE_1:24
X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);
theorem :: XBOOLE_1:25
(X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);
theorem :: XBOOLE_1:26
X c= Y implies X /\ Z c= Y /\ Z;
theorem :: XBOOLE_1:27
X c= Y & Z c= V implies X /\ Z c= Y /\ V;
theorem :: XBOOLE_1:28
X c= Y implies X /\ Y = X;
theorem :: XBOOLE_1:29
X /\ Y c= X \/ Z;
theorem :: XBOOLE_1:30
X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;
theorem :: XBOOLE_1:31
(X /\ Y) \/ (X /\ Z) c= Y \/ Z;
theorem :: XBOOLE_1:32
X \ Y = Y \ X implies X = Y;
theorem :: XBOOLE_1:33
X c= Y implies X \ Z c= Y \ Z;
theorem :: XBOOLE_1:34
X c= Y implies Z \ Y c= Z \ X;
theorem :: XBOOLE_1:35
X c= Y & Z c= V implies X \ V c= Y \ Z;
theorem :: XBOOLE_1:36
X \ Y c= X;
theorem :: XBOOLE_1:37
X \ Y = {} iff X c= Y;
theorem :: XBOOLE_1:38
X c= Y \ X implies X = {};
theorem :: XBOOLE_1:39
X \/ (Y \ X) = X \/ Y;
theorem :: XBOOLE_1:40
(X \/ Y) \ Y = X \ Y;
theorem :: XBOOLE_1:41
(X \ Y) \ Z = X \ (Y \/ Z);
theorem :: XBOOLE_1:42
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);
theorem :: XBOOLE_1:43
X c= Y \/ Z implies X \ Y c= Z;
theorem :: XBOOLE_1:44
X \ Y c= Z implies X c= Y \/ Z;
theorem :: XBOOLE_1:45
X c= Y implies Y = X \/ (Y \ X);
theorem :: XBOOLE_1:46
X \ (X \/ Y) = {};
theorem :: XBOOLE_1:47
X \ X /\ Y = X \ Y;
theorem :: XBOOLE_1:48
X \ (X \ Y) = X /\ Y;
theorem :: XBOOLE_1:49
X /\ (Y \ Z) = (X /\ Y) \ Z;
theorem :: XBOOLE_1:50
X /\ (Y \ Z) = X /\ Y \ X /\ Z;
theorem :: XBOOLE_1:51
X /\ Y \/ (X \ Y) = X;
theorem :: XBOOLE_1:52
X \ (Y \ Z) = (X \ Y) \/ X /\ Z;
theorem :: XBOOLE_1:53
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);
theorem :: XBOOLE_1:54
X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);
theorem :: XBOOLE_1:55
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);
theorem :: XBOOLE_1:56
X c< Y & Y c< Z implies X c< Z;
theorem :: XBOOLE_1:57
not (X c< Y & Y c< X);
theorem :: XBOOLE_1:58
X c< Y & Y c= Z implies X c< Z;
theorem :: XBOOLE_1:59
X c= Y & Y c< Z implies X c< Z;
theorem :: XBOOLE_1:60
X c= Y implies not Y c< X;
theorem :: XBOOLE_1:61
X <> {} implies {} c< X;
theorem :: XBOOLE_1:62
not X c< {};
::$N Modus Celarent
::$N Modus Darii
theorem :: XBOOLE_1:63
X c= Y & Y misses Z implies X misses Z;
theorem :: XBOOLE_1:64
A c= X & B c= Y & X misses Y implies A misses B;
theorem :: XBOOLE_1:65
X misses {};
theorem :: XBOOLE_1:66
X meets X iff X <> {};
theorem :: XBOOLE_1:67
X c= Y & X c= Z & Y misses Z implies X = {};
::$N Modus Darapti
theorem :: XBOOLE_1:68
for A being non empty set st A c= Y & A c= Z holds Y meets Z;
theorem :: XBOOLE_1:69
for A being non empty set st A c= Y holds A meets Y;
theorem :: XBOOLE_1:70
X meets Y \/ Z iff X meets Y or X meets Z;
theorem :: XBOOLE_1:71
X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z;
theorem :: XBOOLE_1:72
X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9;
theorem :: XBOOLE_1:73
X c= Y \/ Z & X misses Z implies X c= Y;
theorem :: XBOOLE_1:74
X meets Y /\ Z implies X meets Y;
theorem :: XBOOLE_1:75
X meets Y implies X /\ Y meets Y;
theorem :: XBOOLE_1:76
Y misses Z implies X /\ Y misses X /\ Z;
theorem :: XBOOLE_1:77
X meets Y & X c= Z implies X meets Y /\ Z;
theorem :: XBOOLE_1:78
X misses Y implies X /\ (Y \/ Z) = X /\ Z;
theorem :: XBOOLE_1:79
X \ Y misses Y;
theorem :: XBOOLE_1:80
X misses Y implies X misses Y \ Z;
theorem :: XBOOLE_1:81
X misses Y \ Z implies Y misses X \ Z;
theorem :: XBOOLE_1:82
X \ Y misses Y \ X;
theorem :: XBOOLE_1:83
X misses Y iff X \ Y = X;
theorem :: XBOOLE_1:84
X meets Y & X misses Z implies X meets Y \ Z;
theorem :: XBOOLE_1:85
X c= Y implies X misses Z \ Y;
theorem :: XBOOLE_1:86
X c= Y & X misses Z implies X c= Y \ Z;
theorem :: XBOOLE_1:87
Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y;
theorem :: XBOOLE_1:88
X misses Y implies (X \/ Y) \ Y = X;
theorem :: XBOOLE_1:89
X /\ Y misses X \ Y;
theorem :: XBOOLE_1:90
X \ (X /\ Y) misses Y;
theorem :: XBOOLE_1:91
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);
theorem :: XBOOLE_1:92
X \+\ X = {};
theorem :: XBOOLE_1:93
X \/ Y = (X \+\ Y) \/ X /\ Y;
theorem :: XBOOLE_1:94
X \/ Y = X \+\ Y \+\ X /\ Y;
theorem :: XBOOLE_1:95
X /\ Y = X \+\ Y \+\ (X \/ Y);
theorem :: XBOOLE_1:96
X \ Y c= X \+\ Y;
theorem :: XBOOLE_1:97
X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;
theorem :: XBOOLE_1:98
X \/ Y = X \+\ (Y \ X);
theorem :: XBOOLE_1:99
(X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));
theorem :: XBOOLE_1:100
X \ Y = X \+\ (X /\ Y);
theorem :: XBOOLE_1:101
X \+\ Y = (X \/ Y) \ X /\ Y;
theorem :: XBOOLE_1:102
X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;
theorem :: XBOOLE_1:103
X /\ Y misses X \+\ Y;
theorem :: XBOOLE_1:104
X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable;
begin :: Addenda
theorem :: XBOOLE_1:105
for X, Y being set st X c< Y holds Y \ X <> {};
theorem :: XBOOLE_1:106
X c= A \ B implies X c= A & X misses B;
theorem :: XBOOLE_1:107
X c= A \+\ B iff X c= A \/ B & X misses A /\ B;
theorem :: XBOOLE_1:108
X c= A implies X /\ Y c= A;
theorem :: XBOOLE_1:109
X c= A implies X \ Y c= A;
theorem :: XBOOLE_1:110
X c= A & Y c= A implies X \+\ Y c= A;
theorem :: XBOOLE_1:111
(X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z;
theorem :: XBOOLE_1:112
(X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z;
theorem :: XBOOLE_1:113
X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V);
theorem :: XBOOLE_1:114
for A,B,C,D being set st A misses D & B misses D & C misses D holds A
\/ B \/ C misses D;
::$CT
theorem :: XBOOLE_1:116
X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z);
theorem :: XBOOLE_1:117
for P,G,C being set st C c= G holds P \ C = (P \ G) \/ (P /\ (G \ C));