### The Mizar article:

### Properties of Subsets

**by****Zinaida Trybulec**

- Received March 4, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: SUBSET_1
- [ MML identifier index ]

environ vocabulary BOOLE, SUBSET_1, NEWTON; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; clusters XBOOLE_0; requirements BOOLE; definitions TARSKI, XBOOLE_0; theorems XBOOLE_0, TARSKI, ENUMSET1, ZFMISC_1, XBOOLE_1; schemes XBOOLE_0; begin reserve E,X,x,y for set; definition let X be set; cluster bool X -> non empty; coherence by ZFMISC_1:def 1; end; definition let x; cluster { x } -> non empty; coherence by TARSKI:def 1; let y; cluster { x, y } -> non empty; coherence by TARSKI:def 2; end; definition let X; canceled; mode Element of X means :Def2: it in X if X is non empty otherwise it is empty; existence by XBOOLE_0:def 1; consistency; end; definition let X; mode Subset of X is Element of bool X; end; definition let X be non empty set; cluster non empty Subset of X; existence proof X in bool X by ZFMISC_1:def 1; then X is Subset of X by Def2; hence thesis; end; end; definition let X1,X2 be non empty set; cluster [: X1,X2 :] -> non empty; coherence proof consider x1 being set such that A1: x1 in X1 by XBOOLE_0:def 1; consider x2 being set such that A2: x2 in X2 by XBOOLE_0:def 1; [x1,x2] in [:X1,X2:] by A1,A2,ZFMISC_1:def 2; hence thesis; end; end; definition let X1,X2,X3 be non empty set; cluster [: X1,X2,X3 :] -> non empty; coherence proof consider x12 being set such that A1: x12 in [:X1,X2:] by XBOOLE_0:def 1; consider x3 being set such that A2: x3 in X3 by XBOOLE_0:def 1; [x12,x3] in [:[:X1,X2:],X3:] by A1,A2,ZFMISC_1:def 2; hence thesis by ZFMISC_1:def 3; end; end; definition let X1,X2,X3,X4 be non empty set; cluster [: X1,X2,X3,X4 :] -> non empty; coherence proof consider x123 being set such that A1: x123 in [:X1,X2,X3:] by XBOOLE_0:def 1; consider x4 being set such that A2: x4 in X4 by XBOOLE_0:def 1; [x123,x4] in [:[:X1,X2,X3:],X4:] by A1,A2,ZFMISC_1:def 2; hence thesis by ZFMISC_1:def 4; end; end; definition let D be non empty set, X be non empty Subset of D; redefine mode Element of X -> Element of D; coherence proof let x be Element of X; A1: x in X by Def2; X in bool D by Def2; then X c= D by ZFMISC_1:def 1; then x in D by A1,TARSKI:def 3; hence x is Element of D by Def2; end; end; Lm1: for X being Subset of E, x being set st x in X holds x in E proof let X be Subset of E, x be set such that A1: x in X; X in bool E by Def2; then X c= E by ZFMISC_1:def 1; hence x in E by A1,TARSKI:def 3; end; definition let E; cluster empty Subset of E; existence proof {} c= E by XBOOLE_1:2; then {} in bool E by ZFMISC_1:def 1; then {} is Subset of E by Def2; hence thesis; end; end; definition let E; func {} E -> empty Subset of E equals {}; coherence proof {} c= E by XBOOLE_1:2; then {} in bool E by ZFMISC_1:def 1; hence thesis by Def2; end; correctness; func [#] E -> Subset of E equals :Def4: E; coherence proof E in bool E by ZFMISC_1:def 1; hence E is Subset of E by Def2; end; correctness; end; canceled 3; theorem {} is Subset of X proof {}X = {}; hence {} is Subset of X; end; reserve A,B,C for Subset of E; canceled 2; theorem Th7: (for x being Element of E holds x in A implies x in B) implies A c= B proof assume A1: for x being Element of E holds x in A implies x in B; let x be set; assume A2: x in A; then x in E by Lm1; then x is Element of E by Def2; hence thesis by A1,A2; end; theorem Th8: (for x being Element of E holds x in A iff x in B) implies A = B proof assume for x being Element of E holds x in A iff x in B; hence A c= B & B c= A by Th7; end; canceled; theorem A <> {} implies ex x being Element of E st x in A proof assume A <> {}; then consider x being set such that A1: x in A by XBOOLE_0:def 1; x in E by A1,Lm1; then x is Element of E by Def2; hence thesis by A1; end; definition let E,A; func A` -> Subset of E equals :Def5: E \ A; coherence proof E \ A c= E by XBOOLE_1:36; then E \ A in bool E by ZFMISC_1:def 1; hence thesis by Def2; end; correctness; involutiveness proof let S,T be Subset of E; assume A1: S = E \ T; T in bool E by Def2; then T c= E by ZFMISC_1:def 1; hence T = {} \/ E /\ T by XBOOLE_1:28 .= (E \ E) \/ E /\ T by XBOOLE_1:37 .= E \ S by A1,XBOOLE_1:52; end; let B; redefine func A \/ B -> Subset of E; coherence proof A in bool E & B in bool E by Def2; then A c= E & B c= E by ZFMISC_1:def 1; then A \/ B c= E by XBOOLE_1:8; then A \/ B in bool E by ZFMISC_1:def 1; hence thesis by Def2; end; func A /\ B -> Subset of E; coherence proof A2: A in bool E by Def2; A3: A /\ B c= A by XBOOLE_1:17; A c= E by A2,ZFMISC_1:def 1; then A /\ B c= E by A3,XBOOLE_1:1; then A /\ B in bool E by ZFMISC_1:def 1; hence A /\ B is Subset of E by Def2; end; func A \ B -> Subset of E; coherence proof A4: A in bool E by Def2; A5: A \ B c= A by XBOOLE_1:36; A c= E by A4,ZFMISC_1:def 1; then A \ B c= E by A5,XBOOLE_1:1; then A \ B in bool E by ZFMISC_1:def 1; hence A \ B is Subset of E by Def2; end; func A \+\ B -> Subset of E; coherence proof A6: A in bool E & B in bool E by Def2; A7: A \ B c= A & B \ A c= B by XBOOLE_1:36; A c= E & B c= E by A6,ZFMISC_1:def 1; then A \ B c= E & B \ A c= E by A7,XBOOLE_1:1; then (A \ B) \/ (B \ A) c= E by XBOOLE_1:8; then A \+\ B c= E by XBOOLE_0:def 6; then A \+\ B in bool E by ZFMISC_1:def 1; hence A \+\ B is Subset of E by Def2; end; end; canceled 4; theorem (for x being Element of E holds x in A iff x in B or x in C) implies A = B \/ C proof assume A1: for x being Element of E holds x in A iff x in B or x in C; now let x be Element of E; assume x in A; then x in B or x in C by A1; hence x in B \/ C by XBOOLE_0:def 2; end; hence A c= B \/ C by Th7; now let x be Element of E; assume x in B \/ C; then x in B or x in C by XBOOLE_0:def 2; hence x in A by A1; end; hence thesis by Th7; end; theorem (for x being Element of E holds x in A iff x in B & x in C) implies A = B /\ C proof assume A1: for x being Element of E holds x in A iff x in B & x in C; now let x be Element of E; assume x in A; then x in B & x in C by A1; hence x in B /\ C by XBOOLE_0:def 3; end; hence A c= B /\ C by Th7; now let x be Element of E; assume x in B /\ C; then x in B & x in C by XBOOLE_0:def 3; hence x in A by A1; end; hence thesis by Th7; end; theorem (for x being Element of E holds x in A iff x in B & not x in C) implies A = B \ C proof assume A1: for x being Element of E holds x in A iff x in B & not x in C; now let x be Element of E; assume x in A; then x in B & not x in C by A1; hence x in B \ C by XBOOLE_0:def 4; end; hence A c= B \ C by Th7; now let x be Element of E; assume x in B \ C; then x in B & not x in C by XBOOLE_0:def 4; hence x in A by A1; end; hence B \ C c= A by Th7; end; theorem (for x being Element of E holds x in A iff not(x in B iff x in C)) implies A = B \+\ C proof assume A1: for x being Element of E holds x in A iff not(x in B iff x in C); now let x be Element of E; assume x in A; then x in B & not x in C or x in C & not x in B by A1; then x in B \ C or x in C \ B by XBOOLE_0:def 4; then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 2; hence x in B \+\ C by XBOOLE_0:def 6; end; hence A c= B \+\ C by Th7; now let x be Element of E; assume x in B \+\ C; then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 6; then x in B \ C or x in C \ B by XBOOLE_0:def 2; then x in B & not x in C or x in C & not x in B by XBOOLE_0:def 4; hence x in A by A1; end; hence thesis by Th7; end; canceled 2; theorem Th21: {} E = ([#] E)` proof thus ([#]E)` = E \ [#]E by Def5 .= E \ E by Def4 .= {}E by XBOOLE_1:37; end; theorem Th22: [#] E = ({} E)` proof thus [#]E = E \ {} by Def4 .= ({}E)` by Def5; end; canceled 2; theorem Th25: A \/ A` = [#]E proof A in bool E by Def2; then A1: A c= E by ZFMISC_1:def 1; thus A \/ A` = A \/ (E \ A) by Def5 .= E by A1,XBOOLE_1:45 .= [#] E by Def4; end; theorem Th26: A misses A` proof A1:A misses (E \ A) by XBOOLE_1:79; A /\ A` = A /\ (E \ A) by Def5 .= {} by A1,XBOOLE_0:def 7; hence thesis by XBOOLE_0:def 7; end; canceled; theorem A \/ [#]E = [#]E proof A in bool E by Def2; then A1: A c= E by ZFMISC_1:def 1; thus A \/ [#]E = A \/ E by Def4 .= E by A1,XBOOLE_1:12 .= [#]E by Def4; end; theorem (A \/ B)` = A` /\ B` proof thus (A \/ B)` = E \ (A \/ B) by Def5 .= (E \ A) /\ (E \ B) by XBOOLE_1:53 .= A` /\ (E \ B) by Def5 .= A` /\ B` by Def5; end; theorem (A /\ B)` = A` \/ B` proof thus (A /\ B)` = E \ (A /\ B) by Def5 .= (E \ A) \/ (E \ B) by XBOOLE_1:54 .= A` \/ (E \ B) by Def5 .= A` \/ B` by Def5; end; theorem Th31: A c= B iff B` c= A` proof E \ A = A` & E \ B = B` by Def5; hence A c= B implies B` c= A` by XBOOLE_1:34; A1: E \ A` = A`` by Def5 .= A; E \ B` = B`` by Def5 .= B; hence thesis by A1,XBOOLE_1:34; end; theorem A \ B = A /\ B` proof A in bool E by Def2; then A1: A c= E by ZFMISC_1:def 1; thus A /\ B` = A /\ (E \ B) by Def5 .= (A /\ E) \ B by XBOOLE_1:49 .= A \ B by A1,XBOOLE_1:28; end; theorem (A \ B)` = A` \/ B proof A in bool E & B in bool E by Def2; then A1: A c= E & B c= E by ZFMISC_1:def 1; thus (A \ B)` = E \ (A \ B) by Def5 .= (E \ A) \/ E /\ B by XBOOLE_1:52 .= A` \/ E /\ B by Def5 .= A` \/ B by A1,XBOOLE_1:28; end; theorem (A \+\ B)` = A /\ B \/ A` /\ B` proof A in bool E by Def2; then A1: A c= E by ZFMISC_1:def 1; thus (A \+\ B)` = E \ (A \+\ B) by Def5 .= E \ (A \/ B) \/ E /\ A /\ B by XBOOLE_1:102 .= A /\ B \/ (E \ (A \/ B)) by A1,XBOOLE_1:28 .= A /\ B \/ (E \ A) /\ (E \ B) by XBOOLE_1:53 .= A /\ B \/ A` /\ (E \ B) by Def5 .= A /\ B \/ (A`) /\ (B`) by Def5; end; theorem A c= B` implies B c= A` proof assume A c= B`; then B``c= A` by Th31; hence thesis; end; theorem A` c= B implies B` c= A proof assume A` c= B; then B` c= A`` by Th31; hence thesis; end; canceled; theorem A c= A` iff A = {}E proof thus A c= A` implies A = {}E proof assume A c= A`; then A c= E \ A by Def5; hence thesis by XBOOLE_1:38; end; A1: A in bool E by Def2; assume A = {}E; then A` = [#]E by Th22 .= E by Def4; hence A c= A` by A1,ZFMISC_1:def 1; end; theorem A` c= A iff A = [#]E proof thus A` c= A implies A = [#]E proof assume A` c= A; hence A = A \/ A` by XBOOLE_1:12 .= [#]E by Th25; end; assume A = [#]E; then A` = {}E by Th21 .= {}; hence A` c= A by XBOOLE_1:2; end; theorem X c= A & X c= A` implies X = {} proof A misses A` by Th26; hence thesis by XBOOLE_1:67; end; theorem (A \/ B)` c= A` proof A c= A \/ B by XBOOLE_1:7; hence thesis by Th31; end; theorem A` c= (A /\ B)` proof A /\ B c= A by XBOOLE_1:17; hence thesis by Th31; end; theorem Th43: A misses B iff A c= B` proof thus A misses B implies A c= B` proof assume A1: A misses B; let x; assume A2: x in A; then A3: x in E by Lm1; not x in B by A1,A2,XBOOLE_0:3; then x in E \ B by A3,XBOOLE_0:def 4; hence x in B` by Def5; end; assume A4: A c= B`; assume A meets B; then consider x such that A5: x in A & x in B by XBOOLE_0:3; A c= E \ B by A4,Def5; then x in E \ B by A5,TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 4; end; theorem A misses B` iff A c= B proof B``= B; hence thesis by Th43; end; canceled; theorem A misses B & A` misses B` implies A = B` proof A1: A in bool E by Def2; assume that A2: A misses B and A3: A` misses B`; thus A c= B` proof let x; assume A4: x in A; A c= E by A1,ZFMISC_1:def 1; then A5: x in E by A4,TARSKI:def 3; not x in B by A2,A4,XBOOLE_0:3; then x in E \ B by A5,XBOOLE_0:def 4; hence thesis by Def5; end; let x; assume x in B`; then x in E \ B by Def5; then A6: x in E & not x in B by XBOOLE_0:def 4; x in A` implies not x in B` by A3,XBOOLE_0:3; then x in E \ A implies not x in E \ B by Def5; hence thesis by A6,XBOOLE_0:def 4; end; theorem A c= B & C misses B implies A c= C` proof assume A c= B & C misses B; then A misses C by XBOOLE_1:63; hence thesis by Th43; end; :: :: ADDITIONAL THEOREMS :: theorem (for a being Element of A holds a in B) implies A c= B proof assume A1: for a being Element of A holds a in B; let a be set; assume a in A; then a is Element of A by Def2; hence thesis by A1; end; theorem (for x being Element of E holds x in A) implies E = A proof assume A1: for x being Element of E holds x in A; thus E c= A proof let a be set; assume a in E; then a is Element of E by Def2; hence thesis by A1; end; A in bool E by Def2; hence A c= E by ZFMISC_1:def 1; end; theorem E <> {} implies for B for x being Element of E st not x in B holds x in B` proof assume A1: E <> {}; let B be Subset of E; let x be Element of E; assume A2: not x in B; x in E by A1,Def2; then x in E \ B by A2,XBOOLE_0:def 4; hence x in B` by Def5; end; theorem Th51: for A,B st for x being Element of E holds x in A iff not x in B holds A = B` proof let A,B be Subset of E; assume A1: for x being Element of E holds x in A iff not x in B; thus A c= B` proof let x be set; assume A2: x in A; A in bool E by Def2; then A c= E by ZFMISC_1:def 1; then x in E by A2,TARSKI:def 3; then x is Element of E by Def2; then x in E & not x in B by A1,A2,Lm1; then x in E \ B by XBOOLE_0:def 4; hence thesis by Def5; end; let x be set; A3: B` in bool E by Def2; assume A4: x in B`; B` c= E by A3,ZFMISC_1:def 1; then x in E by A4,TARSKI:def 3; then reconsider x as Element of E by Def2; x in E \ B by A4,Def5; then not x in B by XBOOLE_0:def 4; hence thesis by A1; end; theorem for A,B st for x being Element of E holds not x in A iff x in B holds A = B` proof let A,B; assume for x being Element of E holds not x in A iff x in B; then for x being Element of E holds x in A iff not x in B; hence A = B` by Th51; end; theorem for A,B st for x being Element of E holds not(x in A iff x in B) holds A = B` proof let A,B; assume for x being Element of E holds not(x in A iff x in B); then for x being Element of E holds x in A iff not x in B; hence A = B` by Th51; end; theorem x in A` implies not x in A proof assume x in A`; then x in E \ A by Def5; hence thesis by XBOOLE_0:def 4; end; reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X; theorem X <> {} implies {x1} is Subset of X proof assume X <> {}; then A1: x1 in X by Def2; {x1} c= X proof let x; assume x in {x1}; hence x in X by A1,TARSKI:def 1; end; then {x1} in bool X by ZFMISC_1:def 1; hence {x1} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2} is Subset of X proof assume X <> {}; then A1: x1 in X & x2 in X by Def2; {x1,x2} c= X proof let x; assume x in {x1,x2}; hence x in X by A1,TARSKI:def 2; end; then {x1,x2} in bool X by ZFMISC_1:def 1; hence {x1,x2} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3} is Subset of X proof assume X <> {}; then A1: x1 in X & x2 in X & x3 in X by Def2; {x1,x2,x3} c= X proof let x; assume x in {x1,x2,x3}; hence x in X by A1,ENUMSET1:def 1; end; then {x1,x2,x3} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3,x4} is Subset of X proof assume X <> {}; then A1: x1 in X & x2 in X & x3 in X & x4 in X by Def2; {x1,x2,x3,x4} c= X proof let x; assume x in {x1,x2,x3,x4}; hence x in X by A1,ENUMSET1:18; end; then {x1,x2,x3,x4} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3,x4} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3,x4,x5} is Subset of X proof assume A1: X <> {}; {x1,x2,x3,x4,x5} c= X proof let x; assume A2: x in {x1,x2,x3,x4,x5}; x in { x1,x2,x3,x4,x5 } implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 by ENUMSET1:23; hence x in X by A1,A2,Def2; end; then {x1,x2,x3,x4,x5} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3,x4,x5} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X proof assume A1: X <> {}; {x1,x2,x3,x4,x5,x6} c= X proof let x; assume A2: x in {x1,x2,x3,x4,x5,x6}; x in { x1,x2,x3,x4,x5,x6} implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 by ENUMSET1:28; hence x in X by A1,A2,Def2; end; then {x1,x2,x3,x4,x5,x6} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3,x4,x5,x6} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X proof assume A1: X <> {}; {x1,x2,x3,x4,x5,x6,x7} c= X proof let x; assume A2: x in {x1,x2,x3,x4,x5,x6,x7}; x in { x1,x2,x3,x4,x5,x6,x7} implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 by ENUMSET1:33; hence x in X by A1,A2,Def2; end; then {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def2; end; theorem X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X proof assume A1: X <> {}; {x1,x2,x3,x4,x5,x6,x7,x8} c= X proof let x; assume A2: x in {x1,x2,x3,x4,x5,x6,x7,x8}; x in { x1,x2,x3,x4,x5,x6,x7,x8} implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 by ENUMSET1:38; hence x in X by A1,A2,Def2; end; then {x1,x2,x3,x4,x5,x6,x7,x8} in bool X by ZFMISC_1:def 1; hence {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X by Def2; end; theorem x in X implies {x} is Subset of X proof assume x in X; then {x} c= X by ZFMISC_1:37; then {x} in bool X by ZFMISC_1:def 1; hence thesis by Def2; end; scheme Subset_Ex { A()-> set, P[set] } : ex X being Subset of A() st for x holds x in X iff x in A() & P[x] proof defpred X[set] means P[$1]; consider X being set such that A1: for x holds x in X iff x in A() & X[x] from Separation; X c= A() proof let x; thus thesis by A1; end; then X in bool A() by ZFMISC_1:def 1; then reconsider X as Subset of A() by Def2; take X; thus thesis by A1; end; scheme Subset_Eq {X() -> set, P[set]}: for X1,X2 being Subset of X() st (for y being Element of X() holds y in X1 iff P[y]) & (for y being Element of X() holds y in X2 iff P[y]) holds X1 = X2 proof let X1,X2 be Subset of X() such that A1:for y being Element of X() holds y in X1 iff P[y] and A2:for y being Element of X() holds y in X2 iff P[y]; for x being Element of X() holds x in X1 iff x in X2 proof let x be Element of X(); hereby assume x in X1; then P[x] by A1; hence x in X2 by A2; end; assume x in X2; then P[x] by A2; hence thesis by A1; end; hence thesis by Th8; end; definition let X, Y be non empty set; redefine pred X misses Y; irreflexivity proof let A be non empty set; consider x being set such that A1: x in A by XBOOLE_0:def 1; thus thesis by A1,XBOOLE_0:3; end; antonym X meets Y; end; definition let S be set; assume A1: contradiction; func choose S -> Element of S means not contradiction; correctness by A1; end;

Back to top