### The Mizar article:

### Some Basic Properties of Many Sorted Sets

**by****Artur Kornilowicz**

- Received September 29, 1995
Copyright (c) 1995 Association of Mizar Users

- MML identifier: PZFMISC1
- [ MML identifier index ]

environ vocabulary FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, CAT_1, BOOLE, MATRIX_1, ZF_REFLE, PRE_CIRC, FINSET_1, CAT_4, TARSKI, PRALG_2; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1, CQC_LANG, PBOOLE, PRE_CIRC, PRALG_2, MBOOLEAN; constructors CQC_LANG, PRE_CIRC, PRALG_2, MBOOLEAN; clusters FINSET_1, PBOOLE, CQC_LANG, XBOOLE_0; requirements BOOLE; definitions PRE_CIRC, PBOOLE; theorems ALTCAT_1, BORSUK_1, CQC_LANG, ENUMSET1, FUNCT_4, MBOOLEAN, PARTFUN1, PBOOLE, PRALG_2, SETWISEO, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0; schemes MSUALG_1; begin :: Preliminaries reserve i, I for set, f for Function, x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I, J for non empty set, NJ for ManySortedSet of J; theorem Th1: for X be set for M be ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I proof let X be set, M be ManySortedSet of I such that A1: i in I; thus dom (M +* (i .--> X)) = dom M \/ dom (i .--> X) by FUNCT_4:def 1 .= I \/ dom (i .--> X) by PBOOLE:def 3 .= I \/ {i} by CQC_LANG:5 .= I by A1,ZFMISC_1:46; end; theorem f = {} implies f is ManySortedSet of {} by PBOOLE:def 3,RELAT_1:60; theorem I is non empty implies not ex X st X is empty-yielding & X is non-empty proof assume A1: I is non empty; given X such that A2: X is empty-yielding and A3: X is non-empty; consider i such that A4: i in I by A1,XBOOLE_0:def 1; X.i is empty & X.i is non empty by A2,A3,A4,PBOOLE:def 15,def 16; hence contradiction; end; begin :: Singelton and unordered pairs definition let I, A; func {A} -> ManySortedSet of I means :Def1: for i st i in I holds it.i = {A.i}; existence proof deffunc F(set) = {A.$1}; thus ex M be ManySortedSet of I st for i st i in I holds M.i = F(i) from MSSLambda; end; uniqueness proof let X, Y be ManySortedSet of I such that A1: (for i st i in I holds X.i = {A.i}) and A2: for i st i in I holds Y.i = {A.i}; now let i; assume A3: i in I; hence X.i = {A.i} by A1 .= Y.i by A2,A3; end; hence X = Y by PBOOLE:3; end; end; definition let I, A; cluster {A} -> non-empty locally-finite; coherence proof thus {A} is non-empty proof let i such that A1: i in I; {A.i} <> {}; hence {A}.i is non empty by A1,Def1; end; let i such that A2: i in I; {A.i} is finite; hence {A}.i is finite by A2,Def1; end; end; definition let I, A, B; func {A,B} -> ManySortedSet of I means :Def2: for i st i in I holds it.i = {A.i,B.i}; existence proof deffunc F(set) = {A.$1,B.$1}; thus ex M be ManySortedSet of I st for i st i in I holds M.i = F(i) from MSSLambda; end; uniqueness proof let X, Y be ManySortedSet of I such that A1: (for i st i in I holds X.i = {A.i,B.i}) and A2: for i st i in I holds Y.i = {A.i,B.i}; now let i; assume A3: i in I; hence X.i = {A.i,B.i} by A1 .= Y.i by A2,A3; end; hence X = Y by PBOOLE:3; end; commutativity; end; definition let I, A, B; cluster {A,B} -> non-empty locally-finite; coherence proof thus {A,B} is non-empty proof let i such that A1: i in I; {A.i,B.i} <> {}; hence {A,B}.i is non empty by A1,Def2; end; let i such that A2: i in I; {A.i,B.i} is finite; hence {A,B}.i is finite by A2,Def2; end; end; theorem :: Tarski:3 X = { y } iff for x holds x in X iff x = y proof thus X = { y } implies for x holds x in X iff x = y proof assume A1: X = {y}; let x; thus x in X implies x = y proof assume A2: x in X; now let i; assume A3: i in I; then A4: x.i in X.i by A2,PBOOLE:def 4; X.i = {y.i} by A1,A3,Def1; hence x.i = y.i by A4,TARSKI:def 1; end; hence thesis by PBOOLE:3; end; assume A5: x = y; let i; assume i in I; then X.i = {y.i} by A1,Def1; hence x.i in X.i by A5,TARSKI:def 1; end; assume A6: for x holds x in X iff x = y; then A7: y in X; now let i such that A8: i in I; now let a be set; thus a in X.i iff a = y.i proof thus a in X.i implies a = y.i proof assume A9: a in X.i; A10: dom (i .--> a) = {i} by CQC_LANG:5; dom (y +* (i .--> a)) = I by A8,Th1; then reconsider x1 = y +* (i .--> a) as ManySortedSet of I by PBOOLE:def 3; i in {i} by TARSKI:def 1; then A11: x1.i = (i .--> a).i by A10,FUNCT_4:14 .= a by CQC_LANG:6; x1 in X proof let q be set such that A12: q in I; per cases; suppose i = q; hence x1.q in X.q by A9,A11; suppose i <> q; then not q in dom (i .--> a) by A10,TARSKI:def 1; then x1.q = y.q by FUNCT_4:12; hence x1.q in X.q by A7,A12,PBOOLE:def 4; end; hence a = y.i by A6,A11; end; assume a = y.i; hence a in X.i by A7,A8,PBOOLE:def 4; end; end; then X.i = {y.i} by TARSKI:def 1; hence X.i = {y}.i by A8,Def1; end; hence thesis by PBOOLE:3; end; theorem :: Tarski:4 a (for x holds x in X iff x = x1 or x = x2) implies X = { x1,x2 } proof assume A1: for x holds x in X iff x = x1 or x = x2; then A2: x1 in X; A3: x2 in X by A1; now let i such that A4: i in I; now let a be set; thus a in X.i iff a = x1.i or a = x2.i proof thus a in X.i implies a = x1.i or a = x2.i proof assume that A5: a in X.i and A6: a <> x1.i; A7: dom (i .--> a) = {i} by CQC_LANG:5; dom (x2 +* (i .--> a)) = I by A4,Th1; then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I by PBOOLE:def 3; i in {i} by TARSKI:def 1; then A8: k2.i = (i .--> a).i by A7,FUNCT_4:14 .= a by CQC_LANG:6; k2 in X proof let q be set such that A9: q in I; per cases; suppose i = q; hence k2.q in X.q by A5,A8; suppose i <> q; then not q in dom (i .--> a) by A7,TARSKI:def 1; then k2.q = x2.q by FUNCT_4:12; hence k2.q in X.q by A3,A9,PBOOLE:def 4; end; hence a = x2.i by A1,A6,A8; end; assume A10: a = x1.i or a = x2.i; per cases by A10; suppose a = x1.i; hence a in X.i by A2,A4,PBOOLE:def 4; suppose a = x2.i; hence a in X.i by A3,A4,PBOOLE:def 4; end; end; then X.i = {x1.i,x2.i} by TARSKI:def 2; hence X.i = { x1,x2 }.i by A4,Def2; end; hence thesis by PBOOLE:3; end; theorem :: Tarski:4 b X = { x1,x2 } implies for x holds x = x1 or x = x2 implies x in X proof assume A1: X = { x1,x2 }; let x; assume A2: x = x1 or x = x2; let i; assume i in I; then A3: X.i = {x1.i,x2.i} by A1,Def2; per cases by A2; suppose x = x1; hence x.i in X.i by A3,TARSKI:def 2; suppose x = x2; hence x.i in X.i by A3,TARSKI:def 2; end; theorem { NJ } <> [0]I proof assume { NJ } = [0]I; hence contradiction by PBOOLE:141; end; theorem :: ENUMSET1:3 x in { A } implies x = A proof assume A1: x in { A }; now let i; assume A2: i in I; then x.i in {A}.i by A1,PBOOLE:def 4; then x.i in {A.i} by A2,Def1; hence x.i = A.i by TARSKI:def 1; end; hence thesis by PBOOLE:3; end; theorem :: ENUMSET1:4 x in { x } proof let i such that A1: i in I; x.i in {x.i} by TARSKI:def 1; hence x.i in {x}.i by A1,Def1; end; theorem :: ENUMSET1:9 x = A or x = B implies x in { A,B } proof assume A1: x=A or x=B; per cases by A1; suppose A2: x=A; let i such that A3: i in I; x.i in {A.i,B.i} by A2,TARSKI:def 2; hence x.i in { A,B }.i by A3,Def2; suppose A4: x=B; let i such that A5: i in I; x.i in {A.i,B.i} by A4,TARSKI:def 2; hence x.i in { A,B }.i by A5,Def2; end; theorem ::ENUMSET1:41 {A} \/ {B} = {A,B} proof now let i; assume A1: i in I; hence ({A} \/ {B}).i = {A}.i \/ {B}.i by PBOOLE:def 7 .= {A}.i \/ {B.i} by A1,Def1 .= {A.i} \/ {B.i} by A1,Def1 .= {A.i,B.i} by ENUMSET1:41 .= {A,B}.i by A1,Def2; end; hence thesis by PBOOLE:3; end; theorem :: ENUMSET1:69 { x,x } = { x } proof now let i; assume A1: i in I; hence { x,x }.i = {x.i,x.i} by Def2 .= {x.i} by ENUMSET1:69 .= { x }.i by A1,Def1; end; hence thesis by PBOOLE:3; end; canceled; theorem :: SETWISEO:1 {A} c= {B} implies A = B proof assume A1: {A} c= {B}; now let i; assume A2: i in I; then {A}.i c= {B}.i by A1,PBOOLE:def 5; then {A}.i c= {B.i} by A2,Def1; then {A.i} c= {B.i} by A2,Def1; hence A.i = B.i by ZFMISC_1:24; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:6 {x} = {y} implies x = y proof assume A1: {x} = {y}; now let i; assume A2: i in I; then {x.i} = {x}.i by Def1 .= {y.i} by A1,A2,Def1; hence x.i = y.i by ZFMISC_1:6; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:8 {x} = {A,B} implies x = A & x = B proof assume A1: {x} = {A,B}; now let i; assume A2: i in I; then {x.i} = {x}.i by Def1 .= {A.i,B.i} by A1,A2,Def2; hence x.i = A.i by ZFMISC_1:8; end; hence x = A by PBOOLE:3; now let i; assume A3: i in I; then {x.i} = {x}.i by Def1 .= {A.i,B.i} by A1,A3,Def2; hence x.i = B.i by ZFMISC_1:8; end; hence x = B by PBOOLE:3; end; theorem :: ZFMISC_1:9 {x} = {A,B} implies A = B proof assume A1: {x} = {A,B}; now let i; assume A2: i in I; then {x.i} = {x}.i by Def1 .= {A.i,B.i} by A1,A2,Def2; hence A.i = B.i by ZFMISC_1:9; end; hence A = B by PBOOLE:3; end; theorem :: ZFMISC_1:12 {x} c= {x,y} & {y} c= {x,y} proof thus {x} c= {x,y} proof let i such that A1: i in I; {x.i} c= {x.i,y.i} by ZFMISC_1:12; then {x}.i c= {x.i,y.i} by A1,Def1; hence {x}.i c= {x,y}.i by A1,Def2; end; let i such that A2: i in I; {y.i} c= {x.i,y.i} by ZFMISC_1:12; then {y}.i c= {x.i,y.i} by A2,Def1; hence {y}.i c= {x,y}.i by A2,Def2; end; theorem :: ZFMISC_1:13 {x} \/ {y} = {x} or {x} \/ {y} = {y} implies x = y proof assume A1: {x} \/ {y} = {x} or {x} \/ {y} = {y}; now let i such that A2: i in I; per cases by A1; suppose A3: {x} \/ {y} = {x}; {x.i} \/ {y.i} = {x.i} \/ {y}.i by A2,Def1 .= {x}.i \/ {y}.i by A2,Def1 .= ({x} \/ {y}).i by A2,PBOOLE:def 7 .= {x.i} by A2,A3,Def1; hence x.i = y.i by ZFMISC_1:13; suppose A4: {x} \/ {y} = {y}; {x.i} \/ {y.i} = {x.i} \/ {y}.i by A2,Def1 .= {x}.i \/ {y}.i by A2,Def1 .= ({x} \/ {y}).i by A2,PBOOLE:def 7 .= {y.i} by A2,A4,Def1; hence x.i = y.i by ZFMISC_1:13; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:14 {x} \/ {x,y} = {x,y} proof now let i; assume A1: i in I; hence ({x} \/ {x,y}).i = {x}.i \/ {x,y}.i by PBOOLE:def 7 .= {x.i} \/ {x,y}.i by A1,Def1 .= {x.i} \/ {x.i,y.i} by A1,Def2 .= {x.i,y.i} by ZFMISC_1:14 .= {x,y}.i by A1,Def2; end; hence thesis by PBOOLE:3; end; canceled; theorem :: ZFMISC_1:16 I is non empty & {x} /\ {y} = [0]I implies x <> y proof assume that A1: I is non empty and A2: {x} /\ {y} = [0]I; now consider i such that A3: i in I by A1,XBOOLE_0:def 1; take i; {x.i} /\ {y.i} = {x}.i /\ {y.i} by A3,Def1 .= {x}.i /\ {y}.i by A3,Def1 .= ({x} /\ {y}).i by A3,PBOOLE:def 8 .= {} by A2,A3,PBOOLE:5; hence x.i <> y.i; end; hence thesis; end; theorem :: ZFMISC_1:18 {x} /\ {y} = {x} or {x} /\ {y} = {y} implies x = y proof assume A1: {x} /\ {y} = {x} or {x} /\ {y} = {y}; per cases by A1; suppose A2: {x} /\ {y} = {x}; now let i; assume A3: i in I; then {x.i} /\ {y.i} = {x.i} /\ {y}.i by Def1 .= {x}.i /\ {y}.i by A3,Def1 .= ({x} /\ {y}).i by A3,PBOOLE:def 8 .= {x.i} by A2,A3,Def1; hence x.i = y.i by ZFMISC_1:18; end; hence thesis by PBOOLE:3; suppose A4: {x} /\ {y} = {y}; now let i; assume A5: i in I; then {x.i} /\ {y.i} = {x.i} /\ {y}.i by Def1 .= {x}.i /\ {y}.i by A5,Def1 .= ({x} /\ {y}).i by A5,PBOOLE:def 8 .= {y.i} by A4,A5,Def1; hence x.i = y.i by ZFMISC_1:18; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:19 {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} proof thus {x} /\ {x,y} = {x} proof now let i; assume A1: i in I; hence ({x} /\ {x,y}).i = {x}.i /\ {x,y}.i by PBOOLE:def 8 .= {x.i} /\ {x,y}.i by A1,Def1 .= {x.i} /\ {x.i,y.i} by A1,Def2 .= {x.i} by ZFMISC_1:19 .= {x}.i by A1,Def1; end; hence thesis by PBOOLE:3; end; thus {y} /\ {x,y} = {y} proof now let i; assume A2: i in I; hence ({y} /\ {x,y}).i = {y}.i /\ {x,y}.i by PBOOLE:def 8 .= {y.i} /\ {x,y}.i by A2,Def1 .= {y.i} /\ {x.i,y.i} by A2,Def2 .= {y.i} by ZFMISC_1:19 .= {y}.i by A2,Def1; end; hence thesis by PBOOLE:3; end; end; theorem :: ZFMISC_1:20 I is non empty & {x} \ {y} = {x} implies x <> y proof assume that A1: I is non empty and A2: {x} \ {y} = {x}; now consider i such that A3: i in I by A1,XBOOLE_0:def 1; take i; {x.i} \ {y.i} = {x}.i \ {y.i} by A3,Def1 .= {x}.i \ {y}.i by A3,Def1 .= ({x} \ {y}).i by A3,PBOOLE:def 9 .= {x.i} by A2,A3,Def1; hence x.i <> y.i by ZFMISC_1:20; end; hence thesis; end; theorem :: ZFMISC_1:21 {x} \ {y} = [0]I implies x = y proof assume A1: {x} \ {y} = [0]I; now let i; assume A2: i in I; then {x.i} \ {y.i} = {x}.i \ {y.i} by Def1 .= {x}.i \ {y}.i by A2,Def1 .= ({x} \ {y}).i by A2,PBOOLE:def 9 .= {} by A1,A2,PBOOLE:5; hence x.i = y.i by ZFMISC_1:21; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:22 {x} \ {x,y} = [0]I & {y} \ {x,y} = [0]I proof thus {x} \ {x,y} = [0]I proof now let i; assume A1: i in I; hence ({x} \ {x,y}).i = {x}.i \ {x,y}.i by PBOOLE:def 9 .= {x.i} \ {x,y}.i by A1,Def1 .= {x.i} \ {x.i,y.i} by A1,Def2 .= {} by ZFMISC_1:22 .= [0]I.i by A1,PBOOLE:5; end; hence thesis by PBOOLE:3; end; now let i; assume A2: i in I; hence ({y} \ {x,y}).i = {y}.i \ {x,y}.i by PBOOLE:def 9 .= {y.i} \ {x,y}.i by A2,Def1 .= {y.i} \ {x.i,y.i} by A2,Def2 .= {} by ZFMISC_1:22 .= [0]I.i by A2,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:24 {x} c= {y} implies {x} = {y} proof assume A1: {x} c= {y}; now let i; assume A2: i in I; then {x}.i c= {y}.i by A1,PBOOLE:def 5; then {x.i} c= {y}.i by A2,Def1; then A3: {x.i} c= {y.i} by A2,Def1; thus {x}.i = {x.i} by A2,Def1 .= {y.i} by A3,ZFMISC_1:24 .= {y}.i by A2,Def1; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:26 {x,y} c= {A} implies x = A & y = A proof assume A1: {x,y} c= {A}; thus x = A proof now let i; assume A2: i in I; then {x,y}.i c= {A}.i by A1,PBOOLE:def 5; then {x,y}.i c= {A.i} by A2,Def1; then {x.i,y.i} c= {A.i} by A2,Def2; hence x.i = A.i by ZFMISC_1:26; end; hence thesis by PBOOLE:3; end; now let i; assume A3: i in I; then {x,y}.i c= {A}.i by A1,PBOOLE:def 5; then {x,y}.i c= {A.i} by A3,Def1; then {x.i,y.i} c= {A.i} by A3,Def2; hence y.i = A.i by ZFMISC_1:26; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:27 {x,y} c= {A} implies {x,y} = {A} proof assume A1: {x,y} c= {A}; now let i; assume A2: i in I; then {x,y}.i c= {A}.i by A1,PBOOLE:def 5; then {x.i,y.i} c= {A}.i by A2,Def2; then A3: {x.i,y.i} c= {A.i} by A2,Def1; thus {x,y}.i = {x.i,y.i} by A2,Def2 .= {A.i} by A3,ZFMISC_1:27 .= {A}.i by A2,Def1; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:30 bool { x } = { [0]I, {x} } proof now let i; assume A1: i in I; hence (bool {x}).i = bool ({x}.i) by MBOOLEAN:def 1 .= bool ({x.i}) by A1,Def1 .= {{}, {x.i}} by ZFMISC_1:30 .= {[0]I.i, {x.i}} by A1,PBOOLE:5 .= {[0]I.i, {x}.i} by A1,Def1 .= { [0]I, {x} }.i by A1,Def2; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:80 { A } c= bool A proof let i such that A1: i in I; {A.i} c= bool (A.i) by ZFMISC_1:80; then {A}.i c= bool (A.i) by A1,Def1; hence {A}.i c= (bool A).i by A1,MBOOLEAN:def 1; end; theorem :: ZFMISC_1:31 union { x } = x proof now let i; assume A1: i in I; hence (union { x }).i = union ({x}.i) by MBOOLEAN:def 2 .= union {x.i} by A1,Def1 .= x.i by ZFMISC_1:31; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:32 union { {x},{y} } = {x,y} proof now let i; assume A1: i in I; hence (union { {x},{y} }).i = union ({{x},{y}}.i) by MBOOLEAN:def 2 .= union {{x}.i,{y}.i} by A1,Def2 .= union {{x.i},{y}.i} by A1,Def1 .= union {{x.i},{y.i}} by A1,Def1 .= {x.i,y.i} by ZFMISC_1:32 .= {x,y}.i by A1,Def2; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:93 union { A,B } = A \/ B proof now let i; assume A1: i in I; hence (union { A,B }).i = union ({A,B}.i) by MBOOLEAN:def 2 .= union {A.i,B.i} by A1,Def2 .= A.i \/ B.i by ZFMISC_1:93 .= (A \/ B).i by A1,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:37 {x} c= X iff x in X proof thus {x} c= X implies x in X proof assume A1: {x} c= X; let i; assume A2: i in I; then {x}.i c= X.i by A1,PBOOLE:def 5; then {x.i} c= X.i by A2,Def1; hence x.i in X.i by ZFMISC_1:37; end; assume A3: x in X; let i; assume A4: i in I; then x.i in X.i by A3,PBOOLE:def 4; then {x.i} c= X.i by ZFMISC_1:37; hence {x}.i c= X.i by A4,Def1; end; theorem :: ZFMISC_1:38 {x1,x2} c= X iff x1 in X & x2 in X proof thus {x1,x2} c= X implies x1 in X & x2 in X proof assume A1: {x1,x2} c= X; thus x1 in X proof let i; assume A2: i in I; then {x1,x2}.i c= X.i by A1,PBOOLE:def 5; then {x1.i,x2.i} c= X.i by A2,Def2; hence thesis by ZFMISC_1:38; end; let i; assume A3: i in I; then {x1,x2}.i c= X.i by A1,PBOOLE:def 5; then {x1.i,x2.i} c= X.i by A3,Def2; hence thesis by ZFMISC_1:38; end; assume A4: x1 in X & x2 in X; let i; assume A5: i in I; then x1.i in X.i & x2.i in X.i by A4,PBOOLE:def 4; then {x1.i,x2.i} c= X.i by ZFMISC_1:38; hence thesis by A5,Def2; end; theorem :: ZFMISC_1:42 A = [0]I or A = {x1} or A = {x2} or A = {x1,x2} implies A c= {x1,x2} proof assume A1: A = [0]I or A = {x1} or A = {x2} or A = {x1,x2}; let i such that A2: i in I; per cases by A1; suppose A = [0]I; then A.i = {} by A2,PBOOLE:5; then A.i c= {x1.i,x2.i} by ZFMISC_1:42; hence A.i c= {x1,x2}.i by A2,Def2; suppose A = {x1}; then A.i = {x1.i} by A2,Def1; then A.i c= {x1.i,x2.i} by ZFMISC_1:42; hence A.i c= {x1,x2}.i by A2,Def2; suppose A = {x2}; then A.i = {x2.i} by A2,Def1; then A.i c= {x1.i,x2.i} by ZFMISC_1:42; hence A.i c= {x1,x2}.i by A2,Def2; suppose A = {x1,x2}; hence A.i c= {x1,x2}.i; end; begin :: Sum of an unordered pairs (or a singelton) and a set theorem :: SETWISEO:6 x in A or x = B implies x in A \/ {B} proof assume A1: x in A or x = B; let i such that A2: i in I; per cases by A1; suppose x in A; then x.i in A.i by A2,PBOOLE:def 4; then x.i in A.i \/ {B.i} by SETWISEO:6; then x.i in A.i \/ {B}.i by A2,Def1; hence x.i in (A \/ {B}).i by A2,PBOOLE:def 7; suppose x = B; then x.i in A.i \/ {B.i} by SETWISEO:6; then x.i in A.i \/ {B}.i by A2,Def1; hence x.i in (A \/ {B}).i by A2,PBOOLE:def 7; end; theorem :: SETWISEO:8 A \/ {x} c= B iff x in B & A c= B proof thus A \/ {x} c= B implies x in B & A c= B proof assume A1: A \/ {x} c= B; A2: now let i; assume A3: i in I; then (A \/ {x}).i c= B.i by A1,PBOOLE:def 5; then A.i \/ {x}.i c= B.i by A3,PBOOLE:def 7; hence A.i \/ {x.i} c= B.i by A3,Def1; end; thus x in B proof let i; assume i in I; then A.i \/ {x.i} c= B.i by A2; hence x.i in B.i by SETWISEO:8; end; let i; assume i in I; then A.i \/ {x.i} c= B.i by A2; hence A.i c= B.i by SETWISEO:8; end; assume A4: x in B & A c= B; let i; assume A5: i in I; then x.i in B.i & A.i c= B.i by A4,PBOOLE:def 4,def 5; then A.i \/ {x.i} c= B.i by SETWISEO:8; then A.i \/ {x}.i c= B.i by A5,Def1; hence (A \/ {x}).i c= B.i by A5,PBOOLE:def 7; end; theorem :: ZFMISC_1:45 {x} \/ X = X implies x in X proof assume A1: {x} \/ X = X; let i; assume A2: i in I; then {x.i} \/ X.i = {x}.i \/ X.i by Def1 .= X.i by A1,A2,PBOOLE:def 7; hence thesis by ZFMISC_1:45; end; theorem :: ZFMISC_1:46 x in X implies {x} \/ X = X proof assume A1: x in X; now let i; assume A2: i in I; then A3: x.i in X.i by A1,PBOOLE:def 4; thus ({x} \/ X).i = {x}.i \/ X.i by A2,PBOOLE:def 7 .= {x.i} \/ X.i by A2,Def1 .= X.i by A3,ZFMISC_1:46; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:47, 48 {x,y} \/ A = A iff x in A & y in A proof thus {x,y} \/ A = A implies x in A & y in A proof assume A1: {x,y} \/ A = A; thus x in A proof let i; assume A2: i in I; then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2 .= A.i by A1,A2,PBOOLE:def 7; hence x.i in A.i by ZFMISC_1:47; end; let i; assume A3: i in I; then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2 .= A.i by A1,A3,PBOOLE:def 7; hence y.i in A.i by ZFMISC_1:47; end; assume A4: x in A & y in A; now let i; assume A5: i in I; then A6: x.i in A.i & y.i in A.i by A4,PBOOLE:def 4; thus ({x,y} \/ A).i = {x,y}.i \/ A.i by A5,PBOOLE:def 7 .= {x.i,y.i} \/ A.i by A5,Def2 .= A.i by A6,ZFMISC_1:48; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:49 I is non empty implies {x} \/ X <> [0]I proof assume that A1: I is non empty and A2: {x} \/ X = [0]I; consider i such that A3: i in I by A1,XBOOLE_0:def 1; {x.i} \/ X.i <> {}; then {x}.i \/ X.i <> {} by A3,Def1; then ({x} \/ X).i <> {} by A3,PBOOLE:def 7; hence contradiction by A2,A3,PBOOLE:5; end; theorem :: ZFMISC_1:50 I is non empty implies {x,y} \/ X <> [0]I proof assume that A1: I is non empty and A2: {x,y} \/ X = [0]I; consider i such that A3: i in I by A1,XBOOLE_0:def 1; {x.i,y.i} \/ X.i <> {}; then {x,y}.i \/ X.i <> {} by A3,Def2; then ({x,y} \/ X).i <> {} by A3,PBOOLE:def 7; hence contradiction by A2,A3,PBOOLE:5; end; begin :: Intersection of an unordered pairs (or a singelton) and a set theorem :: ZFMISC_1:51 X /\ {x} = {x} implies x in X proof assume A1: X /\ {x} = {x}; let i; assume A2: i in I; then X.i /\ {x.i} = X.i /\ {x}.i by Def1 .= (X /\ {x}).i by A2,PBOOLE:def 8 .= {x.i} by A1,A2,Def1; hence x.i in X.i by ZFMISC_1:51; end; theorem :: ZFMISC_1:52 x in X implies X /\ {x} = {x} proof assume A1: x in X; thus X /\ {x} = {x} proof now let i; assume A2: i in I; then A3: x.i in X.i by A1,PBOOLE:def 4; thus (X /\ {x}).i = X.i /\ {x}.i by A2,PBOOLE:def 8 .= X.i /\ {x.i} by A2,Def1 .= {x.i} by A3,ZFMISC_1:52 .= {x}.i by A2,Def1; end; hence thesis by PBOOLE:3; end; end; theorem :: ZFMISC_1:53, 63 x in X & y in X iff {x,y} /\ X = {x,y} proof thus x in X & y in X implies {x,y} /\ X = {x,y} proof assume A1: x in X & y in X; now let i; assume A2: i in I; then A3: x.i in X.i & y.i in X.i by A1,PBOOLE:def 4; thus ({x,y} /\ X).i = {x,y}.i /\ X.i by A2,PBOOLE:def 8 .= {x.i,y.i} /\ X.i by A2,Def2 .= {x.i,y.i} by A3,ZFMISC_1:53 .= {x,y}.i by A2,Def2; end; hence thesis by PBOOLE:3; end; assume A4: {x,y} /\ X = {x,y}; thus x in X proof let i; assume A5: i in I; then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2 .= ({x,y} /\ X).i by A5,PBOOLE:def 8 .= {x.i,y.i} by A4,A5,Def2; hence thesis by ZFMISC_1:63; end; let i; assume A6: i in I; then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2 .= ({x,y} /\ X).i by A6,PBOOLE:def 8 .= {x.i,y.i} by A4,A6,Def2; hence thesis by ZFMISC_1:63; end; theorem :: ZFMISC_1:54 I is non empty & {x} /\ X = [0]I implies not x in X proof assume that A1: I is non empty and A2: {x} /\ X = [0]I and A3: x in X; consider i such that A4: i in I by A1,XBOOLE_0:def 1; {x.i} /\ X.i = {x}.i /\ X.i by A4,Def1 .= ({x} /\ X).i by A4,PBOOLE:def 8 .= {} by A2,A4,PBOOLE:5; then {x.i} misses X.i by XBOOLE_0:def 7; then not x.i in X.i by ZFMISC_1:54; hence contradiction by A3,A4,PBOOLE:def 4; end; theorem :: ZFMISC_1:55 I is non empty & {x,y} /\ X = [0]I implies not x in X & not y in X proof assume that A1: I is non empty and A2: {x,y} /\ X = [0]I; A3: now let i; assume A4: i in I; hence {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2 .= ({x,y} /\ X).i by A4,PBOOLE:def 8 .= {} by A2,A4,PBOOLE:5; end; thus not x in X proof assume A5: x in X; now consider i such that A6: i in I by A1,XBOOLE_0:def 1; take i; {x.i,y.i} /\ X.i = {} by A3,A6; then {x.i,y.i} misses X.i by XBOOLE_0:def 7; hence i in I & not x.i in X.i by A6,ZFMISC_1:55; end; hence contradiction by A5,PBOOLE:def 4; end; assume A7: y in X; now consider i such that A8: i in I by A1,XBOOLE_0:def 1; take i; {x.i,y.i} /\ X.i = {} by A3,A8; then {x.i,y.i} misses X.i by XBOOLE_0:def 7; hence i in I & not y.i in X.i by A8,ZFMISC_1:55; end; hence contradiction by A7,PBOOLE:def 4; end; begin :: Difference of an unordered pairs (or a singelton) and a set theorem :: ZFMISC_1:64 a y in X \ {x} implies y in X proof assume A1: y in X \ {x}; let i; assume A2: i in I; then y.i in (X \ {x}).i by A1,PBOOLE:def 4; then y.i in X.i \ {x}.i by A2,PBOOLE:def 9; then y.i in X.i \ {x.i} by A2,Def1; hence y.i in X.i by ZFMISC_1:64; end; theorem :: ZFMISC_1:64 b I is non empty & y in X \ {x} implies y <> x proof assume that A1: I is non empty and A2: y in X \ {x}; consider i such that A3: i in I by A1,XBOOLE_0:def 1; now take i; y.i in (X \ {x}).i by A2,A3,PBOOLE:def 4; then y.i in X.i \ {x}.i by A3,PBOOLE:def 9; then y.i in X.i \ {x.i} by A3,Def1; hence y.i <> x.i by ZFMISC_1:64; end; hence thesis; end; theorem :: ZFMISC_1:65 I is non empty & X \ {x} = X implies not x in X proof assume that A1: I is non empty and A2: X \ {x} = X and A3: x in X; A4: now let i; assume A5: i in I; hence X.i \ {x.i} = X.i \ {x}.i by Def1 .= X.i by A2,A5,PBOOLE:def 9; end; now consider i such that A6: i in I by A1,XBOOLE_0:def 1; take i; thus i in I by A6; X.i \ {x.i} = X.i by A4,A6; hence not x.i in X.i by ZFMISC_1:65; end; hence contradiction by A3,PBOOLE:def 4; end; theorem :: ZFMISC_1:67 I is non empty & {x} \ X = {x} implies not x in X proof assume that A1: I is non empty and A2: {x} \ X = {x} and A3: x in X; consider i such that A4: i in I by A1,XBOOLE_0:def 1; {x.i} \ X.i = {x}.i \ X.i by A4,Def1 .= ({x} \ X).i by A4,PBOOLE:def 9 .= {x.i} by A2,A4,Def1; then not x.i in X.i by ZFMISC_1:67; hence contradiction by A3,A4,PBOOLE:def 4; end; theorem :: ZFMISC_1:68 {x} \ X = [0]I iff x in X proof thus {x} \ X = [0]I implies x in X proof assume A1: {x} \ X = [0]I; let i; assume A2: i in I; then {x.i} \ X.i = {x}.i \ X.i by Def1 .= ({x} \ X).i by A2,PBOOLE:def 9 .= {} by A1,A2,PBOOLE:5; hence x.i in X.i by ZFMISC_1:68; end; assume A3: x in X; now let i; assume A4: i in I; then A5: x.i in X.i by A3,PBOOLE:def 4; thus ({x} \ X).i = {x}.i \ X.i by A4,PBOOLE:def 9 .= {x.i} \ X.i by A4,Def1 .= {} by A5,ZFMISC_1:68 .= [0]I.i by A4,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:70 I is non empty & {x,y} \ X = {x} implies not x in X proof assume that A1: I is non empty and A2: {x,y} \ X = {x}; consider i such that A3: i in I by A1,XBOOLE_0:def 1; {x.i,y.i} \ X.i = {x,y}.i \ X.i by A3,Def2 .= ({x,y} \ X).i by A3,PBOOLE:def 9 .= {x.i} by A2,A3,Def1; then not x.i in X.i by ZFMISC_1:70; hence thesis by A3,PBOOLE:def 4; end; canceled; theorem :: ZFMISC_1:72 I is non empty & {x,y} \ X = {x,y} implies not x in X & not y in X proof assume I is non empty; then consider i such that A1: i in I by XBOOLE_0:def 1; thus {x,y} \ X = {x,y} implies not x in X & not y in X proof assume A2: {x,y} \ X = {x,y}; thus not x in X proof assume A3: x in X; {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2 .= ({x,y} \ X).i by A1,PBOOLE:def 9 .= {x.i,y.i} by A1,A2,Def2; then not x.i in X.i by ZFMISC_1:72; hence contradiction by A1,A3,PBOOLE:def 4; end; assume A4: y in X; {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2 .= ({x,y} \ X).i by A1,PBOOLE:def 9 .= {x.i,y.i} by A1,A2,Def2; then not y.i in X.i by ZFMISC_1:72; hence contradiction by A1,A4,PBOOLE:def 4; end; end; theorem :: ZFMISC_1:73 {x,y} \ X = [0]I iff x in X & y in X proof thus {x,y} \ X = [0]I implies x in X & y in X proof assume A1: {x,y} \ X = [0]I; thus x in X proof let i; assume A2: i in I; then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2 .= ({x,y} \ X).i by A2,PBOOLE:def 9 .= {} by A1,A2,PBOOLE:5; hence x.i in X.i by ZFMISC_1:73; end; let i; assume A3: i in I; then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2 .= ({x,y} \ X).i by A3,PBOOLE:def 9 .= {} by A1,A3,PBOOLE:5; hence y.i in X.i by ZFMISC_1:73; end; assume A4: x in X & y in X; now let i; assume A5: i in I; then A6: x.i in X.i & y.i in X.i by A4,PBOOLE:def 4; thus ({x,y} \ X).i = {x,y}.i \ X.i by A5,PBOOLE:def 9 .= {x.i,y.i} \ X.i by A5,Def2 .= {} by A6,ZFMISC_1:73 .= [0]I.i by A5,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:75 X = [0]I or X = {x} or X = {y} or X = {x,y} implies X \ {x,y} = [0]I proof assume A1: X = [0]I or X = {x} or X = {y} or X = {x,y}; now let i such that A2: i in I; per cases by A1; suppose X = [0]I; then A3: X.i = {} by A2,PBOOLE:5; thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9 .= [0]I.i by A2,A3,PBOOLE:5; suppose X = {x}; then A4: X.i = {x.i} by A2,Def1; thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9 .= X.i \ {x.i,y.i} by A2,Def2 .= {} by A4,ZFMISC_1:75 .= [0]I.i by A2,PBOOLE:5; suppose X = {y}; then A5: X.i = {y.i} by A2,Def1; thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9 .= X.i \ {x.i,y.i} by A2,Def2 .= {} by A5,ZFMISC_1:75 .= [0]I.i by A2,PBOOLE:5; suppose X = {x,y}; then A6: X.i = {x.i,y.i} by A2,Def2; thus (X \ {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 9 .= X.i \ {x.i,y.i} by A2,Def2 .= {} by A6,ZFMISC_1:75 .= [0]I.i by A2,PBOOLE:5; end; hence thesis by PBOOLE:3; end; begin :: Cartesian product theorem :: ZFMISC_1:113 X = [0]I or Y = [0]I implies [|X,Y|] = [0]I proof assume A1: X = [0]I or Y = [0]I; per cases by A1; suppose A2: X = [0]I; now let i; assume A3: i in I; then A4: X.i = {} by A2,PBOOLE:5; thus [|X,Y|].i = [:X.i,Y.i:] by A3,PRALG_2:def 9 .= {} by A4,ZFMISC_1:113 .= [0]I.i by A3,PBOOLE:5; end; hence thesis by PBOOLE:3; suppose A5: Y = [0]I; now let i; assume A6: i in I; then A7: Y.i = {} by A5,PBOOLE:5; thus [|X,Y|].i = [:X.i,Y.i:] by A6,PRALG_2:def 9 .= {} by A7,ZFMISC_1:113 .= [0]I.i by A6,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:114 X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y proof assume that A1: X is non-empty & Y is non-empty and A2: [|X,Y|] = [|Y,X|]; now let i; assume A3: i in I; then A4: X.i is non empty & Y.i is non empty by A1,PBOOLE:def 16; [:X.i,Y.i:] = [|X,Y|].i by A3,PRALG_2:def 9 .= [:Y.i,X.i:] by A2,A3,PRALG_2:def 9; hence X.i = Y.i by A4,ZFMISC_1:114; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:115 [|X,X|] = [|Y,Y|] implies X = Y proof assume A1: [|X,X|] = [|Y,Y|]; now let i; assume A2: i in I; then [:X.i,X.i:] = [|X,X|].i by PRALG_2:def 9 .= [:Y.i,Y.i:] by A1,A2,PRALG_2:def 9; hence X.i = Y.i by ZFMISC_1:115; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:117 Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y proof assume that A1: Z is non-empty and A2: [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]; per cases by A2; suppose A3: [|X,Z|] c= [|Y,Z|]; let i; assume A4: i in I; then A5: Z.i is non empty by A1,PBOOLE:def 16; [|X,Z|].i c= [|Y,Z|].i by A3,A4,PBOOLE:def 5; then [:X.i,Z.i:] c= [|Y,Z|].i by A4,PRALG_2:def 9; then [:X.i,Z.i:] c= [:Y.i,Z.i:] by A4,PRALG_2:def 9; hence X.i c= Y.i by A5,ZFMISC_1:117; suppose A6: [|Z,X|] c= [|Z,Y|]; let i; assume A7: i in I; then A8: Z.i is non empty by A1,PBOOLE:def 16; [|Z,X|].i c= [|Z,Y|].i by A6,A7,PBOOLE:def 5; then [:Z.i,X.i:] c= [|Z,Y|].i by A7,PRALG_2:def 9; then [:Z.i,X.i:] c= [:Z.i,Y.i:] by A7,PRALG_2:def 9; hence X.i c= Y.i by A8,ZFMISC_1:117; end; theorem :: ZFMISC_1:118 X c= Y implies [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] proof assume A1: X c= Y; thus [|X,Z|] c= [|Y,Z|] proof let i; assume A2: i in I; then X.i c= Y.i by A1,PBOOLE:def 5; then [:X.i,Z.i:] c= [:Y.i,Z.i:] by ZFMISC_1:118; then [|X,Z|].i c= [:Y.i,Z.i:] by A2,PRALG_2:def 9; hence [|X,Z|].i c= [|Y,Z|].i by A2,PRALG_2:def 9; end; let i; assume A3: i in I; then X.i c= Y.i by A1,PBOOLE:def 5; then [:Z.i,X.i:] c= [:Z.i,Y.i:] by ZFMISC_1:118; then [|Z,X|].i c= [:Z.i,Y.i:] by A3,PRALG_2:def 9; hence [|Z,X|].i c= [|Z,Y|].i by A3,PRALG_2:def 9; end; theorem :: ZFMISC_1:119 x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|] proof assume A1: x1 c= A & x2 c= B; let i; assume A2: i in I; then x1.i c= A.i & x2.i c= B.i by A1,PBOOLE:def 5; then [:x1.i,x2.i:] c= [:A.i,B.i:] by ZFMISC_1:119; then [|x1,x2|].i c= [:A.i,B.i:] by A2,PRALG_2:def 9; hence [|x1,x2|].i c= [|A,B|].i by A2,PRALG_2:def 9; end; theorem :: ZFMISC_1:120 [|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|] & [|Z, X \/ Y|] = [|Z, X|] \/ [|Z, Y|] proof thus [|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|] proof now let i; assume A1: i in I; hence [|X \/ Y, Z|].i = [:(X \/ Y).i, Z.i:] by PRALG_2:def 9 .= [:X.i \/ Y.i, Z.i:] by A1,PBOOLE:def 7 .= [:X.i, Z.i:] \/ [:Y.i, Z.i:] by ZFMISC_1:120 .= [|X,Z|].i \/ [:Y.i, Z.i:] by A1,PRALG_2:def 9 .= [|X,Z|].i \/ [|Y,Z|].i by A1,PRALG_2:def 9 .= ([|X, Z|] \/ [|Y, Z|]).i by A1,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; now let i; assume A2: i in I; hence [|Z, X \/ Y|].i = [:Z.i, (X \/ Y).i:] by PRALG_2:def 9 .= [:Z.i, X.i \/ Y.i:] by A2,PBOOLE:def 7 .= [:Z.i,X.i:] \/ [:Z.i,Y.i:] by ZFMISC_1:120 .= [|Z,X|].i \/ [:Z.i,Y.i:] by A2,PRALG_2:def 9 .= [|Z,X|].i \/ [|Z,Y|].i by A2,PRALG_2:def 9 .= ([|Z,X|] \/ [|Z,Y|]).i by A2,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:121 [|x1 \/ x2, A \/ B|] = [|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|] proof now let i; assume A1: i in I; hence [|x1 \/ x2, A \/ B|].i = [:(x1 \/ x2).i,(A \/ B).i:] by PRALG_2:def 9 .= [:x1.i \/ x2.i, (A \/ B).i:] by A1,PBOOLE:def 7 .= [:x1.i \/ x2.i, A.i \/ B.i:] by A1,PBOOLE:def 7 .= [:x1.i,A.i:] \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:] by ZFMISC_1:121 .= [|x1,A|].i \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:] by A1,PRALG_2:def 9 .= [|x1,A|].i \/ [|x1,B|].i \/ [:x2.i,A.i:] \/ [:x2.i,B.i:] by A1,PRALG_2:def 9 .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [:x2.i,B.i:] by A1,PRALG_2:def 9 .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [|x2,B|].i by A1,PRALG_2:def 9 .= ([|x1,A|] \/ [|x1,B|]).i \/ [|x2,A|].i \/ [|x2,B|].i by A1,PBOOLE:def 7 .= ([|x1,A|] \/ [|x1,B|] \/ [|x2,A|]).i \/ [|x2,B|].i by A1,PBOOLE:def 7 .= ([|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|]).i by A1,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:122 [|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|] & [|Z, X /\ Y|] = [|Z, X|] /\ [|Z, Y|] proof thus [|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|] proof now let i; assume A1: i in I; hence [|X /\ Y, Z|].i = [:(X /\ Y).i,Z.i:] by PRALG_2:def 9 .= [:X.i /\ Y.i,Z.i:] by A1,PBOOLE:def 8 .= [:X.i,Z.i:] /\ [:Y.i,Z.i:] by ZFMISC_1:122 .= [|X,Z|].i /\ [:Y.i,Z.i:] by A1,PRALG_2:def 9 .= [|X,Z|].i /\ [|Y,Z|].i by A1,PRALG_2:def 9 .= ([|X, Z|] /\ [|Y, Z|]).i by A1,PBOOLE:def 8; end; hence thesis by PBOOLE:3; end; now let i; assume A2: i in I; hence [|Z,X /\ Y|].i = [:Z.i,(X /\ Y).i:] by PRALG_2:def 9 .= [:Z.i,X.i /\ Y.i:] by A2,PBOOLE:def 8 .= [:Z.i,X.i:] /\ [:Z.i,Y.i:] by ZFMISC_1:122 .= [|Z,X|].i /\ [:Z.i,Y.i:] by A2,PRALG_2:def 9 .= [|Z,X|].i /\ [|Z,Y|].i by A2,PRALG_2:def 9 .= ([|Z,X|] /\ [|Z,Y|]).i by A2,PBOOLE:def 8; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:123 [|x1 /\ x2, A /\ B|] = [|x1,A|] /\ [|x2, B|] proof now let i; assume A1: i in I; hence [|x1 /\ x2, A /\ B|].i = [:(x1 /\ x2).i,(A /\ B).i:] by PRALG_2:def 9 .= [:x1.i /\ x2.i,(A /\ B).i:] by A1,PBOOLE:def 8 .= [:x1.i /\ x2.i,A.i /\ B.i:] by A1,PBOOLE:def 8 .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by ZFMISC_1:123 .= [|x1,A|].i /\ [:x2.i,B.i:] by A1,PRALG_2:def 9 .= [|x1,A|].i /\ [|x2,B|].i by A1,PRALG_2:def 9 .= ([|x1,A|] /\ [|x2, B|]).i by A1,PBOOLE:def 8; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:124 A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|] proof assume A1: A c= X & B c= Y; now let i; assume A2: i in I; then A3: A.i c= X.i & B.i c= Y.i by A1,PBOOLE:def 5; thus ([|A,Y|] /\ [|X,B|]).i = [|A,Y|].i /\ [|X,B|].i by A2,PBOOLE:def 8 .= [:A.i,Y.i:] /\ [|X,B|].i by A2,PRALG_2:def 9 .= [:A.i,Y.i:] /\ [:X.i,B.i:] by A2,PRALG_2:def 9 .= [:A.i,B.i:] by A3,ZFMISC_1:124 .= [|A,B|].i by A2,PRALG_2:def 9; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:125 [|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|] & [|Z, X \ Y|] = [|Z, X|] \ [|Z, Y|] proof thus [|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|] proof now let i; assume A1: i in I; hence [|X \ Y, Z|].i = [:(X \ Y).i,Z.i:] by PRALG_2:def 9 .= [:X.i \ Y.i,Z.i:] by A1,PBOOLE:def 9 .= [:X.i,Z.i:] \ [:Y.i,Z.i:] by ZFMISC_1:125 .= [|X,Z|].i \ [:Y.i,Z.i:] by A1,PRALG_2:def 9 .= [|X,Z|].i \ [|Y,Z|].i by A1,PRALG_2:def 9 .= ([|X, Z|] \ [|Y, Z|]).i by A1,PBOOLE:def 9; end; hence thesis by PBOOLE:3; end; now let i; assume A2: i in I; hence [|Z,X \ Y|].i = [:Z.i,(X \ Y).i:] by PRALG_2:def 9 .= [:Z.i,X.i \ Y.i:] by A2,PBOOLE:def 9 .= [:Z.i,X.i:] \ [:Z.i,Y.i:] by ZFMISC_1:125 .= [|Z,X|].i \ [:Z.i,Y.i:] by A2,PRALG_2:def 9 .= [|Z,X|].i \ [|Z,Y|].i by A2,PRALG_2:def 9 .= ([|Z,X|] \ [|Z,Y|]).i by A2,PBOOLE:def 9; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:126 [|x1,x2|] \ [|A,B|] = [|x1\A,x2|] \/ [|x1,x2\B|] proof now let i; assume A1: i in I; hence ([|x1,x2|] \ [|A,B|]).i = [|x1,x2|].i \ [|A,B|].i by PBOOLE:def 9 .= [:x1.i,x2.i:] \ [|A,B|].i by A1,PRALG_2:def 9 .= [:x1.i,x2.i:] \ [:A.i,B.i:] by A1,PRALG_2:def 9 .= [:x1.i\A.i,x2.i:] \/ [:x1.i,x2.i\B.i:] by ZFMISC_1:126 .= [:(x1\A).i,x2.i:] \/ [:x1.i,x2.i\B.i:] by A1,PBOOLE:def 9 .= [:(x1\A).i,x2.i:] \/ [:x1.i,(x2\B).i:] by A1,PBOOLE:def 9 .= [|x1\A,x2|].i \/ [:x1.i,(x2\B).i:] by A1,PRALG_2:def 9 .= [|x1\A,x2|].i \/ [|x1,x2\B|].i by A1,PRALG_2:def 9 .= ([|x1\A,x2|] \/ [|x1,x2\B|]).i by A1,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:127 x1 /\ x2 = [0]I or A /\ B = [0]I implies [|x1,A|] /\ [|x2,B|] = [0]I proof assume A1: x1 /\ x2 = [0]I or A /\ B= [0]I; per cases by A1; suppose A2: x1 /\ x2 = [0]I; now let i; assume A3: i in I; then x1.i /\ x2.i = (x1 /\ x2).i by PBOOLE:def 8 .= {} by A2,A3,PBOOLE:5; then x1.i misses x2.i by XBOOLE_0:def 7; then A4: [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:127; thus ([|x1,A|] /\ [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i by A3,PBOOLE:def 8 .= [:x1.i,A.i:] /\ [|x2,B|].i by A3,PRALG_2:def 9 .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A3,PRALG_2:def 9 .= {} by A4,XBOOLE_0:def 7 .= [0]I.i by A3,PBOOLE:5; end; hence thesis by PBOOLE:3; suppose A5: A /\ B = [0]I; now let i; assume A6: i in I; then A.i /\ B.i = (A /\ B).i by PBOOLE:def 8 .= {} by A5,A6,PBOOLE:5; then A.i misses B.i by XBOOLE_0:def 7; then A7: [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:127; thus ([|x1,A|] /\ [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i by A6,PBOOLE:def 8 .= [:x1.i,A.i:] /\ [|x2,B|].i by A6,PRALG_2:def 9 .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A6,PRALG_2:def 9 .= {} by A7,XBOOLE_0:def 7 .= [0]I.i by A6,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:130 X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty proof assume A1: X is non-empty; thus [|{x},X|] is non-empty proof let i; assume A2: i in I; then X.i is non empty by A1,PBOOLE:def 16; then [:{x.i},X.i:] is non empty by ZFMISC_1:130; then [:{x}.i,X.i:] is non empty by A2,Def1; hence [|{x},X|].i is non empty by A2,PRALG_2:def 9; end; let i; assume A3: i in I; then X.i is non empty by A1,PBOOLE:def 16; then [:X.i,{x.i}:] is non empty by ZFMISC_1:130; then [:X.i,{x}.i:] is non empty by A3,Def1; hence [|X,{x}|].i is non empty by A3,PRALG_2:def 9; end; theorem :: ZFMISC_1:132 [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] proof thus [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] proof now let i; assume A1: i in I; hence [|{x,y},X|].i = [:{x,y}.i,X.i:] by PRALG_2:def 9 .= [:{x.i,y.i},X.i:] by A1,Def2 .= [:{x.i},X.i:] \/ [:{y.i},X.i:] by ZFMISC_1:132 .= [:{x}.i,X.i:] \/ [:{y.i},X.i:] by A1,Def1 .= [:{x}.i,X.i:] \/ [:{y}.i,X.i:] by A1,Def1 .= [|{x},X|].i \/ [:{y}.i,X.i:] by A1,PRALG_2:def 9 .= [|{x},X|].i \/ [|{y},X|].i by A1,PRALG_2:def 9 .= ([|{x},X|] \/ [|{y},X|]).i by A1,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; now let i; assume A2: i in I; hence [|X,{x,y}|].i = [:X.i,{x,y}.i:] by PRALG_2:def 9 .= [:X.i,{x.i,y.i}:] by A2,Def2 .= [:X.i,{x.i}:] \/ [:X.i,{y.i}:] by ZFMISC_1:132 .= [:X.i,{x}.i:] \/ [:X.i,{y.i}:] by A2,Def1 .= [:X.i,{x}.i:] \/ [:X.i,{y}.i:] by A2,Def1 .= [|X,{x}|].i \/ [:X.i,{y}.i:] by A2,PRALG_2:def 9 .= [|X,{x}|].i \/ [|X,{y}|].i by A2,PRALG_2:def 9 .= ([|X,{x}|] \/ [|X,{y}|]).i by A2,PBOOLE:def 7; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:134 x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|] implies x1 = x2 & A = B proof assume that A1: x1 is non-empty & A is non-empty and A2: [|x1,A|] = [|x2,B|]; thus x1 = x2 proof now let i; assume A3: i in I; then A4: x1.i is non empty & A.i is non empty by A1,PBOOLE:def 16; [:x1.i,A.i:] = [|x1,A|].i by A3,PRALG_2:def 9 .= [:x2.i,B.i:] by A2,A3,PRALG_2:def 9; hence x1.i = x2.i by A4,ZFMISC_1:134; end; hence thesis by PBOOLE:3; end; now let i; assume A5: i in I; then A6: x1.i is non empty & A.i is non empty by A1,PBOOLE:def 16; [:x1.i,A.i:] = [|x1,A|].i by A5,PRALG_2:def 9 .= [:x2.i,B.i:] by A2,A5,PRALG_2:def 9; hence A.i = B.i by A6,ZFMISC_1:134; end; hence thesis by PBOOLE:3; end; theorem :: ZFMISC_1:116, 135 X c= [|X,Y|] or X c= [|Y,X|] implies X = [0]I proof assume A1: X c= [|X,Y|] or X c= [|Y,X|]; per cases by A1; suppose A2: X c= [|X,Y|]; now let i; assume A3: i in I; then X.i c= [|X,Y|].i by A2,PBOOLE:def 5; then X.i c= [:X.i,Y.i:] by A3,PRALG_2:def 9; hence X.i = {} by ZFMISC_1:135 .= [0]I.i by A3,PBOOLE:5; end; hence thesis by PBOOLE:3; suppose A4: X c= [|Y,X|]; now let i; assume A5: i in I; then X.i c= [|Y,X|].i by A4,PBOOLE:def 5; then X.i c= [:Y.i,X.i:] by A5,PRALG_2:def 9; hence X.i = {} by ZFMISC_1:135 .= [0]I.i by A5,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: BORSUK_1:2 A in [|x,y|] & A in [|X,Y|] implies A in [|x /\ X, y /\ Y|] proof assume A1: A in [|x,y|] & A in [|X,Y|]; let i; assume A2: i in I; then A.i in [|x,y|].i & A.i in [|X,Y|].i by A1,PBOOLE:def 4; then A.i in [:x.i,y.i:] & A.i in [:X.i,Y.i:] by A2,PRALG_2:def 9; then A.i in [:x.i /\ X.i, y.i /\ Y.i:] by BORSUK_1:2; then A.i in [:(x /\ X).i, y.i /\ Y.i:] by A2,PBOOLE:def 8; then A.i in [:(x /\ X).i, (y /\ Y).i:] by A2,PBOOLE:def 8; hence thesis by A2,PRALG_2:def 9; end; theorem :: BORSUK_1:7 [|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y proof assume that A1: [|x,X|] c= [|y,Y|] and A2: [|x,X|] is non-empty; thus x c= y proof let i; assume A3: i in I; then [|x,X|].i c= [|y,Y|].i by A1,PBOOLE:def 5; then [:x.i,X.i:] c= [|y,Y|].i by A3,PRALG_2:def 9; then A4: [:x.i,X.i:] c= [:y.i,Y.i:] by A3,PRALG_2:def 9; [|x,X|].i is non empty by A2,A3,PBOOLE:def 16; then [:x.i,X.i:] is non empty by A3,PRALG_2:def 9; hence x.i c= y.i by A4,BORSUK_1:7; end; let i; assume A5: i in I; then [|x,X|].i c= [|y,Y|].i by A1,PBOOLE:def 5; then [:x.i,X.i:] c= [|y,Y|].i by A5,PRALG_2:def 9; then A6: [:x.i,X.i:] c= [:y.i,Y.i:] by A5,PRALG_2:def 9; [|x,X|].i is non empty by A2,A5,PBOOLE:def 16; then [:x.i,X.i:] is non empty by A5,PRALG_2:def 9; hence X.i c= Y.i by A6,BORSUK_1:7; end; theorem :: REALSET1:4 A c= X implies [|A,A|] c= [|X,X|] proof assume A1: A c= X; let i; assume A2: i in I; then A.i c= X.i by A1,PBOOLE:def 5; then [:A.i,A.i:] c= [:X.i,X.i:] by ZFMISC_1:119; then [|A,A|].i c= [:X.i,X.i:] by A2,PRALG_2:def 9; hence [|A,A|].i c= [|X,X|].i by A2,PRALG_2:def 9; end; theorem :: SYSREL:17 X /\ Y = [0]I implies [|X,Y|] /\ [|Y,X|] = [0]I proof assume A1: X /\ Y = [0]I; now let i; assume A2: i in I; then X.i /\ Y.i = (X /\ Y).i by PBOOLE:def 8 .= {} by A1,A2,PBOOLE:5; then X.i misses Y.i by XBOOLE_0:def 7; then A3: [:X.i,Y.i:] misses [:Y.i,X.i:] by ZFMISC_1:127; thus ([|X,Y|] /\ [|Y,X|]).i = [|X,Y|].i /\ [|Y,X|].i by A2,PBOOLE:def 8 .= [:X.i,Y.i:] /\ [|Y,X|].i by A2,PRALG_2:def 9 .= [:X.i,Y.i:] /\ [:Y.i,X.i:] by A2,PRALG_2:def 9 .= {} by A3,XBOOLE_0:def 7 .= [0]I.i by A2,PBOOLE:5; end; hence thesis by PBOOLE:3; end; theorem :: ALTCAT_1:1 A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y proof assume that A1: A is non-empty and A2: [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]; per cases by A2; suppose A3: [|A,B|] c= [|X,Y|]; let i; assume A4: i in I; then [|A,B|].i c= [|X,Y|].i by A3,PBOOLE:def 5; then [:A.i,B.i:] c= [|X,Y|].i by A4,PRALG_2:def 9; then A5: [:A.i,B.i:] c= [:X.i,Y.i:] by A4,PRALG_2:def 9; A.i is non empty by A1,A4,PBOOLE:def 16; hence B.i c= Y.i by A5,ALTCAT_1:1; suppose A6: [|B,A|] c= [|Y,X|]; let i; assume A7: i in I; then [|B,A|].i c= [|Y,X|].i by A6,PBOOLE:def 5; then [:B.i,A.i:] c= [|Y,X|].i by A7,PRALG_2:def 9; then A8: [:B.i,A.i:] c= [:Y.i,X.i:] by A7,PRALG_2:def 9; A.i is non empty by A1,A7,PBOOLE:def 16; hence B.i c= Y.i by A8,ALTCAT_1:1; end; theorem :: PARTFUN1:1 x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|A \/ X,B \/ Y|] proof assume A1: x c= [|A,B|] & y c= [|X,Y|]; let i; assume A2: i in I; then x.i c= [|A,B|].i & y.i c= [|X,Y|].i by A1,PBOOLE:def 5; then x.i c= [:A.i,B.i:] & y.i c= [:X.i,Y.i:] by A2,PRALG_2:def 9; then x.i \/ y.i c= [:A.i \/ X.i,B.i \/ Y.i:] by PARTFUN1:1; then (x \/ y).i c= [:A.i \/ X.i,B.i \/ Y.i:] by A2,PBOOLE:def 7; then (x \/ y).i c= [:(A \/ X).i,B.i \/ Y.i:] by A2,PBOOLE:def 7; then (x \/ y).i c= [:(A \/ X).i,(B \/ Y).i:] by A2,PBOOLE:def 7; hence thesis by A2,PRALG_2:def 9; end;

Back to top