The Mizar abstract of XBOOLE

Journal of Formalized Mathematics
EMM, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users
The abstract of the Mizar article:: Boolean Properties of Sets --- Theorems
by
Library Committee
Received April 8, 2002
MML identifier: XBOOLE_1
[ Mizar article, MML identifier index ]
environ

 vocabulary BOOLE, ZFMISC_1;
 notation TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 clusters XBOOLE_0;
 requirements BOOLE;


begin

 reserve x,A,B,X,X',Y,Y',Z,V for set;

theorem :: XBOOLE_1:1  :: BOOLE'29:
  X c= Y & Y c= Z implies X c= Z;

theorem :: XBOOLE_1:2  :: BOOLE'27:
  {} c= X;

theorem :: XBOOLE_1:3  :: BOOLE'30:
  X c= {} implies X = {};

:: \/

theorem :: XBOOLE_1:4  :: BOOLE'64:
  (X \/ Y) \/ Z = X \/ (Y \/ Z);

theorem :: XBOOLE_1:5 :: SYSREL'2:
    (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z);

theorem :: XBOOLE_1:6 :: SYSREL'3:
    X \/ (X \/ Y) = X \/ Y;

theorem :: XBOOLE_1:7  :: BOOLE'31:
  X c= X \/ Y;

theorem :: XBOOLE_1:8  :: BOOLE'32:
  X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: XBOOLE_1:9  :: BOOLE'33:
  X c= Y implies X \/ Z c= Y \/ Z;

theorem :: XBOOLE_1:10 :: AMI_5'2:
    X c= Y implies X c= Z \/ Y;

theorem :: XBOOLE_1:11 :: SETWISEO'7:
    X \/ Y c= Z implies X c= Z;

theorem :: XBOOLE_1:12  :: BOOLE'35:
  X c= Y implies X \/ Y = Y;

theorem :: XBOOLE_1:13 :: BOOLE'34:
    X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: XBOOLE_1:14 :: BOOLE'56:
    (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 :: BOOLE'59:
    X \/ Y = {} implies X = {};

:: /\

theorem :: XBOOLE_1:16  :: BOOLE'67:
  (X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: XBOOLE_1:17  :: BOOLE'37:
  X /\ Y c= X;

theorem :: XBOOLE_1:18 :: SYSREL'4:
    X c= Y /\ Z implies X c= Y;

theorem :: XBOOLE_1:19  :: BOOLE'39:
  Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: XBOOLE_1:20 :: BOOLE'57:
    (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 :: BOOLE'68:
    X /\ (X \/ Y) = X;

theorem :: XBOOLE_1:22  :: BOOLE'69:
  X \/ (X /\ Y) = X;

theorem :: XBOOLE_1:23  :: BOOLE'70:
  X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: XBOOLE_1:24  :: BOOLE'71:
  X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);

theorem :: XBOOLE_1:25 :: BOOLE'72:
    (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

theorem :: XBOOLE_1:26  :: BOOLE'40:
  X c= Y implies X /\ Z c= Y /\ Z;

theorem :: XBOOLE_1:27 :: BOOLE'41:
    X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: XBOOLE_1:28  :: BOOLE'42:
  X c= Y implies X /\ Y = X;

theorem :: XBOOLE_1:29 :: BOOLE'38:
    X /\ Y c= X \/ Z;

theorem :: XBOOLE_1:30 :: BOOLE'44:
    X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: XBOOLE_1:31 :: BOOLE'53:
    (X /\ Y) \/ (X /\ Z) c= Y \/ Z;

:: \

theorem :: XBOOLE_1:32 :: BOOLE'90:
    X \ Y = Y \ X implies X = Y;

theorem :: XBOOLE_1:33  :: BOOLE'46:
  X c= Y implies X \ Z c= Y \ Z;

theorem :: XBOOLE_1:34  :: BOOLE'47:
  X c= Y implies Z \ Y c= Z \ X;

theorem :: XBOOLE_1:35 :: BOOLE'48:
    X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: XBOOLE_1:36  :: BOOLE'49:
  X \ Y c= X;

theorem :: XBOOLE_1:37 :: BOOLE'45:
    X \ Y = {} iff X c= Y;

theorem :: XBOOLE_1:38 :: BOOLE'50:
    X c= Y \ X implies X = {};

theorem :: XBOOLE_1:39  :: BOOLE'79:
  X \/ (Y \ X) = X \/ Y;

theorem :: XBOOLE_1:40 :: BOOLE'83:
    (X \/ Y) \ Y = X \ Y;

theorem :: XBOOLE_1:41  :: BOOLE'88:
  (X \ Y) \ Z = X \ (Y \/ Z);

theorem :: XBOOLE_1:42  :: BOOLE'89:
  (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: XBOOLE_1:43 :: BOOLE'52:
    X c= Y \/ Z implies X \ Y c= Z;

theorem :: XBOOLE_1:44 :: NORMFORM'2:
    X \ Y c= Z implies X c= Y \/ Z;

theorem :: XBOOLE_1:45 :: BOOLE'54:
    X c= Y implies Y = X \/ (Y \ X);

theorem :: XBOOLE_1:46 :: BOOLE'76:
    X \ (X \/ Y) = {};

theorem :: XBOOLE_1:47  :: BOOLE'77:
  X \ X /\ Y = X \ Y;

theorem :: XBOOLE_1:48 :: BOOLE'82:
    X \ (X \ Y) = X /\ Y;

theorem :: XBOOLE_1:49  :: BOOLE'116:
  X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: XBOOLE_1:50  :: BOOLE'117
  X /\ (Y \ Z) = X /\ Y \ X /\ Z;

theorem :: XBOOLE_1:51  :: BOOLE'80:
  X /\ Y \/ (X \ Y) = X;

theorem :: XBOOLE_1:52  :: BOOLE'81:
  X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: XBOOLE_1:53 :: BOOLE'85:
    X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: XBOOLE_1:54  :: BOOLE'86:
   X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: XBOOLE_1:55  :: BOOLE'87:
  (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: XBOOLE_1:56 :: BOOLE'123:
    X c< Y & Y c< Z implies X c< Z;

theorem :: XBOOLE_1:57 :: BOOLE'126:
    not (X c< Y & Y c< X);

theorem :: XBOOLE_1:58 :: BOOLE'121:
    X c< Y & Y c= Z implies X c< Z;

theorem :: XBOOLE_1:59 :: BOOLE'122:
    X c= Y & Y c< Z implies X c< Z;

theorem :: XBOOLE_1:60  :: BOOLE'127:
  X c= Y implies not Y c< X;

theorem :: XBOOLE_1:61 :: BOOLE'124:
    X <> {} implies {} c< X;

theorem :: XBOOLE_1:62 :: BOOLE'125:
    not X c< {};

:: meets & misses

theorem :: XBOOLE_1:63  :: BOOLE'55:
  X c= Y & Y misses Z implies X misses Z;

theorem :: XBOOLE_1:64 :: AMI_5'1:
    A c= X & B c= Y & X misses Y implies A misses B;

theorem :: XBOOLE_1:65 :: BOOLE'104:
    X misses {};

theorem :: XBOOLE_1:66 :: BOOLE'110:
    X meets X iff X <> {};

theorem :: XBOOLE_1:67 :: BOOLE'51:
    X c= Y & X c= Z & Y misses Z implies X = {};

theorem :: XBOOLE_1:68 :: JORDAN9'2:
    for A being non empty set st A c= Y & A c= Z holds Y meets Z;

theorem :: XBOOLE_1:69 :: TOPREAL6'27:
    for A being non empty set st A c= Y holds A meets Y;

theorem :: XBOOLE_1:70  :: BOOLE'100:
  X meets Y \/ Z iff X meets Y or X meets Z;

theorem :: XBOOLE_1:71 :: TOPREAL6'28:
    X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z;

theorem :: XBOOLE_1:72 :: SETWISEO'9:
    X' \/ Y' = X \/ Y & X misses X' & Y misses Y' implies X = Y';

theorem :: XBOOLE_1:73 :: BOOLE'120:
    X c= Y \/ Z & X misses Z implies X c= Y;

theorem :: XBOOLE_1:74  :: BOOLE'102:
  X meets Y /\ Z implies X meets Y;

theorem :: XBOOLE_1:75 :: JORDAN9'1:
    X meets Y implies X /\ Y meets Y;

theorem :: XBOOLE_1:76 :: PROB_2'7:
    Y misses Z implies X /\ Y misses X /\ Z;

theorem :: XBOOLE_1:77 :: BORSUK_1'1:
    X meets Y & X c= Z implies X meets Y /\ Z;

theorem :: XBOOLE_1:78 :: SPRECT_3'1:
    X misses Y implies X /\ (Y \/ Z) = X /\ Z;

theorem :: XBOOLE_1:79  :: BOOLE'78:
  X \ Y misses Y;

theorem :: XBOOLE_1:80 :: BOOLE'113:
    X misses Y implies X misses Y \ Z;

theorem :: XBOOLE_1:81 :: AMI_1'12:
    X misses Y \ Z implies Y misses X \ Z;

theorem :: XBOOLE_1:82 :: RLVECT_2'102:
    X \ Y misses Y \ X;

theorem :: XBOOLE_1:83  :: BOOLE'84:
  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 :: DYNKIN'3:
    X c= Y implies X misses Z \ Y;

theorem :: XBOOLE_1:86  :: JCT_MISC'1:
  X c= Y & X misses Z implies X c= Y \ Z;

theorem :: XBOOLE_1:87 :: CQC_THE3'60:
    Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y;

theorem :: XBOOLE_1:88  :: FINSUB_1'2:
  X misses Y implies (X \/ Y) \ Y = X;

theorem :: XBOOLE_1:89  :: BOOLE'111:
  X /\ Y misses X \ Y;

theorem :: XBOOLE_1:90
    X \ (X /\ Y) misses Y;

:: \+\

theorem :: XBOOLE_1:91 :: BOOLE'99:
    (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: XBOOLE_1:92 :: BOOLE'93:
    X \+\ X = {};

theorem :: XBOOLE_1:93  :: BOOLE'95:
  X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: XBOOLE_1:94 :: FINSUB_1'4:
    X \/ Y = X \+\ Y \+\ X /\ Y;

theorem :: XBOOLE_1:95 :: FINSUB_1'6:
    X /\ Y = X \+\ Y \+\ (X \/ Y);

theorem :: XBOOLE_1:96 :: BOOLE'58:
    X \ Y c= X \+\ Y;

theorem :: XBOOLE_1:97 :: BOOLE'115:
    X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: XBOOLE_1:98 :: FINSUB_1'3:
    X \/ Y = X \+\ (Y \ X);

theorem :: XBOOLE_1:99 :: BOOLE'97:
    (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: XBOOLE_1:100 :: FINSUB_1'5:
    X \ Y = X \+\ (X /\ Y);

theorem :: XBOOLE_1:101 :: BOOLE'96:
    X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: XBOOLE_1:102 :: BOOLE'98:
    X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: XBOOLE_1:103 :: BOOLE'112:
    X /\ Y misses X \+\ Y;

:: comparable

theorem :: XBOOLE_1:104 :: TREES_1'20:
    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  :: ZFMISC_1:85
   X c= A \ B implies X c= A & X misses B;

theorem :: XBOOLE_1:107 :: ZFMISC_1:87
     X c= A \+\ B iff X c= A \/ B & X misses A /\ B;

theorem :: XBOOLE_1:108 :: ZFMISC_1:89
     X c= A implies X /\ Y c= A;

theorem :: XBOOLE_1:109  :: ZFMISC_1:90
   X c= A implies X \ Y c= A;

theorem :: XBOOLE_1:110 :: ZFMISC_1:91
     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;

begin :: additional

theorem :: XBOOLE_1:113 :: from BORSUK_5
    X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V);
The abstract of the Mizar article:

Boolean Properties of Sets --- Theorems
