:: Boolean Domains :: by Andrzej Trybulec and Agata Darmochwa\l :: :: Received April 14, 1989 :: Copyright (c) 1990-2017 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 XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, FINSET_1, FINSUB_1, MATRIX_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1; constructors TARSKI, SUBSET_1, FINSET_1; registrations XBOOLE_0, SUBSET_1, FINSET_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; equalities XBOOLE_0; expansions TARSKI, XBOOLE_0; theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; begin :: Auxiliary theorems reserve X,Y,x for set; definition let IT be set; attr IT is cup-closed means :Def1: for X,Y being set st X in IT & Y in IT holds X \/ Y in IT; attr IT is cap-closed means for X,Y being set st X in IT & Y in IT holds X /\ Y in IT; attr IT is diff-closed means :Def3: for X,Y being set st X in IT & Y in IT holds X \ Y in IT; end; definition let IT be set; attr IT is preBoolean means IT is cup-closed diff-closed; end; registration cluster preBoolean -> cup-closed diff-closed for set; coherence; cluster cup-closed diff-closed -> preBoolean for set; coherence; end; registration cluster non empty cup-closed cap-closed diff-closed for set; existence proof take {{}}; thus {{}} is non empty; thus {{}} is cup-closed proof let X,Y be set; assume that A1: X in {{}} and A2: Y in {{}}; X = {} by A1,TARSKI:def 1; hence thesis by A2; end; thus {{}} is cap-closed proof let X,Y be set; assume that A3: X in {{}} and Y in {{}}; X = {} by A3,TARSKI:def 1; hence thesis by TARSKI:def 1; end; thus {{}} is diff-closed proof let X,Y be set; assume that A4: X in {{}} and Y in {{}}; X = {} by A4,TARSKI:def 1; hence thesis by TARSKI:def 1; end; end; end; theorem Th1: for A being set holds A is preBoolean iff for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A proof let A be set; thus A is preBoolean implies for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A by Def1,Def3; assume A1: for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A; A2: A is diff-closed by A1; A is cup-closed by A1; hence thesis by A2; end; reserve A for non empty preBoolean set; definition let A; let X,Y be Element of A; redefine func X \/ Y -> Element of A; correctness by Th1; redefine func X \ Y -> Element of A; correctness by Th1; end; theorem Th2: X is Element of A & Y is Element of A implies X /\ Y is Element of A proof assume X is Element of A & Y is Element of A; then reconsider X,Y as Element of A; X /\ Y = X \ (X \ Y) by XBOOLE_1:48; hence thesis; end; theorem Th3: X is Element of A & Y is Element of A implies X \+\ Y is Element of A proof assume X is Element of A & Y is Element of A; then reconsider X,Y as Element of A; X \+\ Y = (X \ Y) \/ (Y \ X); hence thesis; end; theorem for A being non empty set st for X,Y being Element of A holds X \+\ Y in A & X \ Y in A holds A is preBoolean proof let A be non empty set such that A1: for X,Y being Element of A holds X \+\ Y in A & X \ Y in A; now let X,Y be set; assume that A2: X in A and A3: Y in A; reconsider Z = Y \ X as Element of A by A1,A2,A3; X \/ Y = X \+\ Z by XBOOLE_1:98; hence X \/ Y in A by A1,A2; thus X \ Y in A by A1,A2,A3; end; hence thesis by Th1; end; theorem for A being non empty set st for X,Y being Element of A holds X \+\ Y in A & X /\ Y in A holds A is preBoolean proof let A be non empty set such that A1: for X,Y being Element of A holds X \+\ Y in A & X /\ Y in A; now let X,Y be set; assume that A2: X in A and A3: Y in A; reconsider Z1 = X \+\ Y, Z2 = X /\ Y as Element of A by A1,A2,A3; X \/ Y = Z1 \+\ Z2 by XBOOLE_1:94; hence X \/ Y in A by A1; X \ Y = X \+\ Z2 by XBOOLE_1:100; hence X \ Y in A by A1,A2; end; hence thesis by Th1; end; theorem for A being non empty set st for X,Y being Element of A holds X \+\ Y in A & X \/ Y in A holds A is preBoolean proof let A be non empty set such that A1: for X,Y being Element of A holds X \+\ Y in A & X \/ Y in A; now let X,Y be set; assume that A2: X in A and A3: Y in A; thus X \/ Y in A by A1,A2,A3; reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1,A2,A3; X /\ Y = Z1 \+\ Z2 by XBOOLE_1:95; then reconsider Z = X /\ Y as Element of A by A1; X \ Y = X \+\ Z by XBOOLE_1:100; hence X \ Y in A by A1,A2; end; hence thesis by Th1; end; definition let A; let X,Y be Element of A; redefine func X /\ Y -> Element of A; coherence by Th2; redefine func X \+\ Y -> Element of A; coherence by Th3; end; theorem Th7: {} in A proof set x = the Element of A; x \ x = {} by XBOOLE_1:37; hence thesis; end; theorem Th8: for A being set holds bool A is preBoolean proof let A be set; now let X,Y be set; assume X in bool A & Y in bool A; then reconsider X9=X,Y9=Y as Subset of A; X9 \/ Y9 in bool A & X9 \ Y9 in bool A; hence X \/ Y in bool A & X \ Y in bool A; end; hence thesis by Th1; end; registration let A be set; cluster bool A -> preBoolean; coherence by Th8; end; theorem for A,B being non empty preBoolean set holds A /\ B is non empty preBoolean proof let A,B be non empty preBoolean set; {} in A & {} in B by Th7; then reconsider C = A /\ B as non empty set by XBOOLE_0:def 4; now let X,Y be set; assume A1: X in C & Y in C; then A2: X in B & Y in B by XBOOLE_0:def 4; then A3: X \/ Y in B by Th1; A4: X \ Y in B by A2,Th1; A5: X in A & Y in A by A1,XBOOLE_0:def 4; then X \/ Y in A by Th1; hence X \/ Y in C by A3,XBOOLE_0:def 4; X \ Y in A by A5,Th1; hence X \ Y in C by A4,XBOOLE_0:def 4; end; hence thesis by Th1; end; :: The set of all finite subsets of a set definition let A be set; func Fin A -> preBoolean set means :Def5: for X being set holds X in it iff X c= A & X is finite; existence proof defpred P[object] means ex y being set st y=\$1 & y c= A & y is finite; consider P being set such that A1: for x being object holds x in P iff x in bool A & P[x] from XBOOLE_0:sch 1; {} c= A; then reconsider Q=P as non empty set by A1; for X,Y being set st X in Q & Y in Q holds X \/ Y in Q & X \ Y in Q proof let X,Y be set; assume that A2: X in Q and A3: Y in Q; consider Z1 being set such that A4: Z1=X and A5: Z1 c=A and A6: Z1 is finite by A1,A2; consider Z2 being set such that A7: Z2=Y and A8: Z2 c= A and A9: Z2 is finite by A1,A3; A10: Z1 \ Z2 c= A by A5; Z1 \/ Z2 c= A by A5,A8,XBOOLE_1:8; hence thesis by A1,A4,A6,A7,A9,A10; end; then reconsider R=Q as non empty preBoolean set by Th1; for X being set holds X in R iff X c= A & X is finite proof let X be set; thus X in R implies X c= A & X is finite proof assume X in R; then ex Y being set st Y=X & Y c= A & Y is finite by A1; hence thesis; end; thus thesis by A1; end; hence thesis; end; uniqueness proof let P,Q be preBoolean set; assume that A11: for X being set holds X in P iff X c= A & X is finite and A12: for X being set holds X in Q iff X c= A & X is finite; for x being object holds x in P iff x in Q proof let x be object; reconsider xx=x as set by TARSKI:1; thus x in P implies x in Q proof assume x in P; then xx c= A & xx is finite by A11; hence thesis by A12; end; thus x in Q implies x in P proof assume x in Q; then xx c= A & xx is finite by A12; hence thesis by A11; end; end; hence thesis by TARSKI:2; end; end; registration let A be set; cluster Fin A -> non empty; coherence proof {} c= A; hence thesis by Def5; end; end; registration let A be set; cluster -> finite for Element of Fin A; coherence by Def5; end; theorem Th10: for A, B being set st A c= B holds Fin A c= Fin B proof let A,B be set; assume A1: A c= B; let X be object; reconsider XX=X as set by TARSKI:1; assume A2: X in Fin A; then XX c= A by Def5; then XX c= B by A1; hence X in Fin B by A2,Def5; end; theorem for A, B being set holds Fin (A /\ B) = Fin A /\ Fin B proof let A, B be set; Fin (A /\ B) c= Fin A & Fin (A /\ B) c= Fin B by Th10,XBOOLE_1:17; hence Fin (A /\ B) c= Fin A /\ Fin B by XBOOLE_1:19; let X be object; reconsider XX=X as set by TARSKI:1; assume A1: X in Fin A /\ Fin B; then X in Fin B by XBOOLE_0:def 4; then A2: XX c= B by Def5; A3: X in Fin A by A1,XBOOLE_0:def 4; then XX c= A by Def5; then XX c= A /\ B by A2,XBOOLE_1:19; hence X in Fin (A /\ B) by A3,Def5; end; theorem for A, B being set holds Fin A \/ Fin B c= Fin (A \/ B) proof let A, B be set; Fin A c= Fin (A \/ B) & Fin B c= Fin(A \/ B) by Th10,XBOOLE_1:7; hence thesis by XBOOLE_1:8; end; theorem Th13: for A being set holds Fin A c= bool A proof let A be set; let x be object; reconsider xx=x as set by TARSKI:1; assume x in Fin A; then xx c= A by Def5; hence thesis; end; theorem Th14: for A being set st A is finite holds Fin A = bool A proof let A be set; assume A1: A is finite; A2: bool A c= Fin A by A1,Def5; Fin A c= bool A by Th13; hence thesis by A2; end; theorem Fin {} = { {} } by Th14,ZFMISC_1:1; theorem for A being set, X being Element of Fin A holds X is Subset of A by Def5; theorem for A being set, X being Subset of A st A is finite holds X is Element of Fin A by Def5;