:: Properties of Subsets :: by Zinaida Trybulec :: :: Received March 4, 1989 :: Copyright (c) 1990-2018 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 ZFMISC_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_7; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; registrations XBOOLE_0, ZFMISC_1; requirements BOOLE; begin reserve E,X,Y,x,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 for set; registration let X be set; cluster bool X -> non empty; end; registration let x1, x2, x3 be object; cluster { x1, x2, x3 } -> non empty; let x4 be object; cluster { x1, x2, x3, x4 } -> non empty; let x5 be object; cluster { x1, x2, x3, x4, x5 } -> non empty; let x6 be object; cluster { x1, x2, x3, x4, x5, x6 } -> non empty; let x7 be object; cluster { x1, x2, x3, x4, x5, x6, x7 } -> non empty; let x8 be object; cluster { x1, x2, x3, x4, x5, x6, x7, x8 } -> non empty; let x9 be object; cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9 } -> non empty; let x10 be object; cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 } -> non empty; end; definition let X; mode Element of X -> set means :: SUBSET_1:def 1 it in X if X is non empty otherwise it is empty; sethood; end; definition let X; mode Subset of X is Element of bool X; end; registration let X be non empty set; cluster non empty for Subset of X; end; registration let X1,X2 be non empty set; cluster [: X1,X2 :] -> non empty; end; registration let X1,X2,X3 be non empty set; cluster [: X1,X2,X3 :] -> non empty; end; registration let X1,X2,X3,X4 be non empty set; cluster [: X1,X2,X3,X4 :] -> non empty; end; definition let D be non empty set, X be non empty Subset of D; redefine mode Element of X -> Element of D; end; registration let E; cluster empty for Subset of E; end; definition let E; func {}E -> Subset of E equals :: SUBSET_1:def 2 {}; func [#] E -> Subset of E equals :: SUBSET_1:def 3 E; end; registration let E; cluster {}E -> empty; end; theorem :: SUBSET_1:1 {} is Subset of X; reserve A,B,C for Subset of E; theorem :: SUBSET_1:2 (for x being Element of E holds x in A implies x in B) implies A c= B; theorem :: SUBSET_1:3 (for x being Element of E holds x in A iff x in B) implies A = B; theorem :: SUBSET_1:4 A <> {} implies ex x being Element of E st x in A; definition let E,A; func A` -> Subset of E equals :: SUBSET_1:def 4 E \ A; involutiveness; let B; redefine func A \/ B -> Subset of E; redefine func A \+\ B -> Subset of E; end; definition let X,Y be set; redefine func X \ Y -> Subset of X; end; definition let E,A,X; redefine func A \ X -> Subset of E; end; definition let E,A,X; redefine func A /\ X -> Subset of E; end; definition let E,X,A; redefine func X /\ A -> Subset of E; end; theorem :: SUBSET_1:5 (for x being Element of E holds x in A iff x in B or x in C) implies A = B \/ C; theorem :: SUBSET_1:6 (for x being Element of E holds x in A iff x in B & x in C) implies A = B /\ C; theorem :: SUBSET_1:7 (for x being Element of E holds x in A iff x in B & not x in C) implies A = B \ C; theorem :: SUBSET_1:8 (for x being Element of E holds x in A iff not(x in B iff x in C)) implies A = B \+\ C; theorem :: SUBSET_1:9 [#] E = ({} E)`; theorem :: SUBSET_1:10 A \/ A` = [#]E; theorem :: SUBSET_1:11 A \/ [#]E = [#]E; theorem :: SUBSET_1:12 A c= B iff B` c= A`; theorem :: SUBSET_1:13 A \ B = A /\ B`; theorem :: SUBSET_1:14 (A \ B)` = A` \/ B; theorem :: SUBSET_1:15 (A \+\ B)` = A /\ B \/ A` /\ B`; theorem :: SUBSET_1:16 A c= B` implies B c= A`; theorem :: SUBSET_1:17 A` c= B implies B` c= A; theorem :: SUBSET_1:18 A c= A` iff A = {}E; theorem :: SUBSET_1:19 A` c= A iff A = [#]E; theorem :: SUBSET_1:20 X c= A & X c= A` implies X = {}; theorem :: SUBSET_1:21 (A \/ B)` c= A`; theorem :: SUBSET_1:22 A` c= (A /\ B)`; theorem :: SUBSET_1:23 A misses B iff A c= B`; theorem :: SUBSET_1:24 A misses B` iff A c= B; theorem :: SUBSET_1:25 A misses B & A` misses B` implies A = B`; theorem :: SUBSET_1:26 A c= B & C misses B implies A c= C`; :: :: ADDITIONAL THEOREMS :: theorem :: SUBSET_1:27 (for a being Element of A holds a in B) implies A c= B; theorem :: SUBSET_1:28 (for x being Element of E holds x in A) implies E = A; theorem :: SUBSET_1:29 E <> {} implies for B for x being Element of E st not x in B holds x in B`; theorem :: SUBSET_1:30 for A,B st for x being Element of E holds x in A iff not x in B holds A = B`; theorem :: SUBSET_1:31 for A,B st for x being Element of E holds not x in A iff x in B holds A = B`; theorem :: SUBSET_1:32 for A,B st for x being Element of E holds not(x in A iff x in B) holds A = B` ; reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X; theorem :: SUBSET_1:33 X <> {} implies {x1} is Subset of X; theorem :: SUBSET_1:34 X <> {} implies {x1,x2} is Subset of X; theorem :: SUBSET_1:35 X <> {} implies {x1,x2,x3} is Subset of X; theorem :: SUBSET_1:36 X <> {} implies {x1,x2,x3,x4} is Subset of X; theorem :: SUBSET_1:37 X <> {} implies {x1,x2,x3,x4,x5} is Subset of X; theorem :: SUBSET_1:38 X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X; theorem :: SUBSET_1:39 X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X; theorem :: SUBSET_1:40 X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X; theorem :: SUBSET_1:41 x in X implies {x} is Subset of X; scheme :: SUBSET_1:sch 1 SubsetEx { A()-> set, P[object] } : ex X being Subset of A() st for x holds x in X iff x in A() & P[x]; scheme :: SUBSET_1:sch 2 SubsetEq {X() -> set, X1,X2()-> Subset of X(), P[set]}: X1() = X2() provided for y being Element of X() holds y in X1() iff P[y] and for y being Element of X() holds y in X2() iff P[y]; definition let X, Y be non empty set; redefine pred X misses Y; irreflexivity; end; definition let X, Y be non empty set; redefine pred X meets Y; reflexivity; end; definition ::\$CD end; begin :: from SETWISEO, 2005.6.11 , A.T. scheme :: SUBSET_1:sch 3 SubsetEx { A() -> non empty set, P[object] } : ex B being Subset of A() st for x being Element of A() holds x in B iff P[x]; :: from GROUP_2, 2005.6.14 , A.T. scheme :: SUBSET_1:sch 4 SubComp{A() -> set, F1,F2() -> Subset of A(), P[set]}: F1() = F2() provided for X being Element of A() holds X in F1() iff P[X] and for X being Element of A() holds X in F2() iff P[X]; :: from FIN_TOPO, 2006.11.07. A.T. theorem :: SUBSET_1:42 A` = B` implies A = B; :: from SGRAPH1, 2008.06.02 registration let X be empty set; cluster -> empty for Subset of X; end; :: from TEX_2, 2006.06.18, A.T. (simplified) definition let E be set; let A be Subset of E; attr A is proper means :: SUBSET_1:def 6 A <> E; end; registration let E be set; cluster [#]E -> non proper; end; registration let E be set; cluster non proper for Subset of E; end; registration let E be non empty set; cluster non proper -> non empty for Subset of E; cluster empty -> proper for Subset of E; end; registration let E be non empty set; cluster proper for Subset of E; end; registration let E be empty set; cluster -> non proper for Subset of E; end; :: from GRCAT_1, 2010.02.18, A.T. theorem :: SUBSET_1:43 for X,Y,A being set, z being set st z in A & A c= [:X,Y:] ex x being Element of X, y being Element of Y st z = [x,y]; :: from BORSUK_4, 2011.03.04, A.T. theorem :: SUBSET_1:44 for X being non empty set, A, B being non empty Subset of X st A c< B ex p being Element of X st p in B & A c= B \ {p}; definition let X be set; redefine attr X is trivial means :: SUBSET_1:def 7 for x,y being Element of X holds x = y; end; registration let X be non empty set; cluster non empty trivial for Subset of X; end; registration let X be trivial set; cluster -> trivial for Subset of X; end; registration let X be non trivial set; cluster non trivial for Subset of X; end; theorem :: SUBSET_1:45 for D being set, A being Subset of D st A is non trivial ex d1,d2 being Element of D st d1 in A & d2 in A & d1 <> d2; theorem :: SUBSET_1:46 for X being trivial non empty set ex x being Element of X st X = {x}; :: from BORSUK_4, 2011.07.31, A.T. theorem :: SUBSET_1:47 for X being non empty set, A being non empty Subset of X holds A is trivial implies ex x being Element of X st A = {x}; theorem :: SUBSET_1:48 for X be non trivial set, x being Element of X ex y be object st y in X & x <> y; :: from FUNCT_7, 3.20.2012, A.T. reserve x for object; definition let x,X; assume x in X; func In(x,X) -> Element of X equals :: SUBSET_1:def 8 x; end; registration let X be non empty set, x be Element of X; reduce In(x,X) to x; end; theorem :: SUBSET_1:49 x in X /\ Y implies In(x,X) = In(x,Y); :: from BORSUK_4, 2012.08.12, A.T. theorem :: SUBSET_1:50 for X being non trivial set, p being set ex q being Element of X st q <> p; theorem :: SUBSET_1:51 for T being non trivial set, X being non trivial Subset of T, p being set ex q being Element of T st q in X & q <> p; :: 2012.12.16, A.T. scheme :: SUBSET_1:sch 5 Union1 { A()-> set, a()-> Element of A(), F(object) -> set }: union { F(j) where j is Element of A() : j in {a()}} = F(a()); scheme :: SUBSET_1:sch 6 Union2 { A()-> set, a,b()-> Element of A(), F(object) -> set }: union { F(j) where j is Element of A() : j in {a(),b()}} = F(a()) \/ F(b());