:: PZFMISC1 semantic presentation begin theorem Th1: :: PZFMISC1:1 for I, i, X being set for M being ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I proof let I, i, X be set ; ::_thesis: for M being ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I let M be ManySortedSet of I; ::_thesis: ( i in I implies dom (M +* (i .--> X)) = I ) assume A1: i in I ; ::_thesis: dom (M +* (i .--> X)) = I thus dom (M +* (i .--> X)) = (dom M) \/ (dom (i .--> X)) by FUNCT_4:def_1 .= I \/ (dom (i .--> X)) by PARTFUN1:def_2 .= I \/ {i} by FUNCOP_1:13 .= I by A1, ZFMISC_1:40 ; ::_thesis: verum end; theorem :: PZFMISC1:2 for f being Function st f = {} holds f is ManySortedSet of {} by PARTFUN1:def_2, RELAT_1:38, RELAT_1:def_18; theorem :: PZFMISC1:3 for I being set st not I is empty holds for X being ManySortedSet of I holds ( not X is V3() or not X is V2() ) proof let I be set ; ::_thesis: ( not I is empty implies for X being ManySortedSet of I holds ( not X is V3() or not X is V2() ) ) assume A1: not I is empty ; ::_thesis: for X being ManySortedSet of I holds ( not X is V3() or not X is V2() ) given X being ManySortedSet of I such that A2: X is V3() and A3: X is V2() ; ::_thesis: contradiction consider i being set such that A4: i in I by A1, XBOOLE_0:def_1; X . i is empty by A2, A4, PBOOLE:def_12; hence contradiction by A3, A4, PBOOLE:def_13; ::_thesis: verum end; begin definition let I be set ; let A be ManySortedSet of I; func{A} -> ManySortedSet of I means :Def1: :: PZFMISC1:def 1 for i being set st i in I holds it . i = {(A . i)}; existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = {(A . i)} proof deffunc H1( set ) -> set = {(A . $1)}; thus ex M being ManySortedSet of I st for i being set st i in I holds M . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = {(A . i)} ) & ( for i being set st i in I holds b2 . i = {(A . i)} ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = {(A . i)} ) & ( for i being set st i in I holds Y . i = {(A . i)} ) implies X = Y ) assume that A1: for i being set st i in I holds X . i = {(A . i)} and A2: for i being set st i in I holds Y . i = {(A . i)} ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A3: i in I ; ::_thesis: X . i = Y . i hence X . i = {(A . i)} by A1 .= Y . i by A2, A3 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines { PZFMISC1:def_1_:_ for I being set for A, b3 being ManySortedSet of I holds ( b3 = {A} iff for i being set st i in I holds b3 . i = {(A . i)} ); registration let I be set ; let A be ManySortedSet of I; cluster{A} -> V2() V26() ; coherence ( {A} is non-empty & {A} is finite-yielding ) proof thus {A} is V2() ::_thesis: {A} is finite-yielding proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not {A} . i is empty ) assume A1: i in I ; ::_thesis: not {A} . i is empty {(A . i)} <> {} ; hence not {A} . i is empty by A1, Def1; ::_thesis: verum end; let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or {A} . i is finite ) assume A2: i in I ; ::_thesis: {A} . i is finite {(A . i)} is finite ; hence {A} . i is finite by A2, Def1; ::_thesis: verum end; end; definition let I be set ; let A, B be ManySortedSet of I; func{A,B} -> ManySortedSet of I means :Def2: :: PZFMISC1:def 2 for i being set st i in I holds it . i = {(A . i),(B . i)}; existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = {(A . i),(B . i)} proof deffunc H1( set ) -> set = {(A . $1),(B . $1)}; thus ex M being ManySortedSet of I st for i being set st i in I holds M . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = {(A . i),(B . i)} ) & ( for i being set st i in I holds b2 . i = {(A . i),(B . i)} ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = {(A . i),(B . i)} ) & ( for i being set st i in I holds Y . i = {(A . i),(B . i)} ) implies X = Y ) assume that A1: for i being set st i in I holds X . i = {(A . i),(B . i)} and A2: for i being set st i in I holds Y . i = {(A . i),(B . i)} ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A3: i in I ; ::_thesis: X . i = Y . i hence X . i = {(A . i),(B . i)} by A1 .= Y . i by A2, A3 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; commutativity for b1, A, B being ManySortedSet of I st ( for i being set st i in I holds b1 . i = {(A . i),(B . i)} ) holds for i being set st i in I holds b1 . i = {(B . i),(A . i)} ; end; :: deftheorem Def2 defines { PZFMISC1:def_2_:_ for I being set for A, B, b4 being ManySortedSet of I holds ( b4 = {A,B} iff for i being set st i in I holds b4 . i = {(A . i),(B . i)} ); registration let I be set ; let A, B be ManySortedSet of I; cluster{A,B} -> V2() V26() ; coherence ( {A,B} is non-empty & {A,B} is finite-yielding ) proof thus {A,B} is V2() ::_thesis: {A,B} is finite-yielding proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not {A,B} . i is empty ) assume A1: i in I ; ::_thesis: not {A,B} . i is empty {(A . i),(B . i)} <> {} ; hence not {A,B} . i is empty by A1, Def2; ::_thesis: verum end; let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or {A,B} . i is finite ) assume A2: i in I ; ::_thesis: {A,B} . i is finite {(A . i),(B . i)} is finite ; hence {A,B} . i is finite by A2, Def2; ::_thesis: verum end; end; theorem :: PZFMISC1:4 for I being set for X, y being ManySortedSet of I holds ( X = {y} iff for x being ManySortedSet of I holds ( x in X iff x = y ) ) proof let I be set ; ::_thesis: for X, y being ManySortedSet of I holds ( X = {y} iff for x being ManySortedSet of I holds ( x in X iff x = y ) ) let X, y be ManySortedSet of I; ::_thesis: ( X = {y} iff for x being ManySortedSet of I holds ( x in X iff x = y ) ) thus ( X = {y} implies for x being ManySortedSet of I holds ( x in X iff x = y ) ) ::_thesis: ( ( for x being ManySortedSet of I holds ( x in X iff x = y ) ) implies X = {y} ) proof assume A1: X = {y} ; ::_thesis: for x being ManySortedSet of I holds ( x in X iff x = y ) let x be ManySortedSet of I; ::_thesis: ( x in X iff x = y ) thus ( x in X implies x = y ) ::_thesis: ( x = y implies x in X ) proof assume A2: x in X ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . i = y . i ) assume A3: i in I ; ::_thesis: x . i = y . i then A4: x . i in X . i by A2, PBOOLE:def_1; X . i = {(y . i)} by A1, A3, Def1; hence x . i = y . i by A4, TARSKI:def_1; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; assume A5: x = y ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume i in I ; ::_thesis: x . i in X . i then X . i = {(y . i)} by A1, Def1; hence x . i in X . i by A5, TARSKI:def_1; ::_thesis: verum end; assume A6: for x being ManySortedSet of I holds ( x in X iff x = y ) ; ::_thesis: X = {y} then A7: y in X ; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_{y}_._i let i be set ; ::_thesis: ( i in I implies X . i = {y} . i ) assume A8: i in I ; ::_thesis: X . i = {y} . i now__::_thesis:_for_a_being_set_holds_ (_a_in_X_._i_iff_a_=_y_._i_) let a be set ; ::_thesis: ( a in X . i iff a = y . i ) thus ( a in X . i iff a = y . i ) ::_thesis: verum proof thus ( a in X . i implies a = y . i ) ::_thesis: ( a = y . i implies a in X . i ) proof assume A9: a in X . i ; ::_thesis: a = y . i A10: dom (i .--> a) = {i} by FUNCOP_1:13; dom (y +* (i .--> a)) = I by A8, Th1; then reconsider x1 = y +* (i .--> a) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; i in {i} by TARSKI:def_1; then A11: x1 . i = (i .--> a) . i by A10, FUNCT_4:13 .= a by FUNCOP_1:72 ; x1 in X proof let q be set ; :: according to PBOOLE:def_1 ::_thesis: ( not q in I or x1 . q in X . q ) assume A12: q in I ; ::_thesis: x1 . q in X . q percases ( i = q or i <> q ) ; suppose i = q ; ::_thesis: x1 . q in X . q hence x1 . q in X . q by A9, A11; ::_thesis: verum end; suppose i <> q ; ::_thesis: x1 . q in X . q then not q in dom (i .--> a) by A10, TARSKI:def_1; then x1 . q = y . q by FUNCT_4:11; hence x1 . q in X . q by A7, A12, PBOOLE:def_1; ::_thesis: verum end; end; end; hence a = y . i by A6, A11; ::_thesis: verum end; assume a = y . i ; ::_thesis: a in X . i hence a in X . i by A7, A8, PBOOLE:def_1; ::_thesis: verum end; end; then X . i = {(y . i)} by TARSKI:def_1; hence X . i = {y} . i by A8, Def1; ::_thesis: verum end; hence X = {y} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:5 for I being set for X, x1, x2 being ManySortedSet of I st ( for x being ManySortedSet of I holds ( x in X iff ( x = x1 or x = x2 ) ) ) holds X = {x1,x2} proof let I be set ; ::_thesis: for X, x1, x2 being ManySortedSet of I st ( for x being ManySortedSet of I holds ( x in X iff ( x = x1 or x = x2 ) ) ) holds X = {x1,x2} let X, x1, x2 be ManySortedSet of I; ::_thesis: ( ( for x being ManySortedSet of I holds ( x in X iff ( x = x1 or x = x2 ) ) ) implies X = {x1,x2} ) assume A1: for x being ManySortedSet of I holds ( x in X iff ( x = x1 or x = x2 ) ) ; ::_thesis: X = {x1,x2} then A2: x1 in X ; A3: x2 in X by A1; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_{x1,x2}_._i let i be set ; ::_thesis: ( i in I implies X . i = {x1,x2} . i ) assume A4: i in I ; ::_thesis: X . i = {x1,x2} . i now__::_thesis:_for_a_being_set_holds_ (_a_in_X_._i_iff_(_a_=_x1_._i_or_a_=_x2_._i_)_) let a be set ; ::_thesis: ( a in X . i iff ( a = x1 . i or a = x2 . i ) ) thus ( a in X . i iff ( a = x1 . i or a = x2 . i ) ) ::_thesis: verum proof thus ( not a in X . i or a = x1 . i or a = x2 . i ) ::_thesis: ( ( a = x1 . i or a = x2 . i ) implies a in X . i ) proof assume that A5: a in X . i and A6: a <> x1 . i ; ::_thesis: a = x2 . i A7: dom (i .--> a) = {i} by FUNCOP_1:13; dom (x2 +* (i .--> a)) = I by A4, Th1; then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; i in {i} by TARSKI:def_1; then A8: k2 . i = (i .--> a) . i by A7, FUNCT_4:13 .= a by FUNCOP_1:72 ; k2 in X proof let q be set ; :: according to PBOOLE:def_1 ::_thesis: ( not q in I or k2 . q in X . q ) assume A9: q in I ; ::_thesis: k2 . q in X . q percases ( i = q or i <> q ) ; suppose i = q ; ::_thesis: k2 . q in X . q hence k2 . q in X . q by A5, A8; ::_thesis: verum end; suppose i <> q ; ::_thesis: k2 . q in X . q then not q in dom (i .--> a) by A7, TARSKI:def_1; then k2 . q = x2 . q by FUNCT_4:11; hence k2 . q in X . q by A3, A9, PBOOLE:def_1; ::_thesis: verum end; end; end; hence a = x2 . i by A1, A6, A8; ::_thesis: verum end; assume A10: ( a = x1 . i or a = x2 . i ) ; ::_thesis: a in X . i percases ( a = x1 . i or a = x2 . i ) by A10; suppose a = x1 . i ; ::_thesis: a in X . i hence a in X . i by A2, A4, PBOOLE:def_1; ::_thesis: verum end; suppose a = x2 . i ; ::_thesis: a in X . i hence a in X . i by A3, A4, PBOOLE:def_1; ::_thesis: verum end; end; end; end; then X . i = {(x1 . i),(x2 . i)} by TARSKI:def_2; hence X . i = {x1,x2} . i by A4, Def2; ::_thesis: verum end; hence X = {x1,x2} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:6 for I being set for X, x1, x2 being ManySortedSet of I st X = {x1,x2} holds for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds x in X proof let I be set ; ::_thesis: for X, x1, x2 being ManySortedSet of I st X = {x1,x2} holds for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds x in X let X, x1, x2 be ManySortedSet of I; ::_thesis: ( X = {x1,x2} implies for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds x in X ) assume A1: X = {x1,x2} ; ::_thesis: for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds x in X let x be ManySortedSet of I; ::_thesis: ( ( x = x1 or x = x2 ) implies x in X ) assume A2: ( x = x1 or x = x2 ) ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume i in I ; ::_thesis: x . i in X . i then A3: X . i = {(x1 . i),(x2 . i)} by A1, Def2; percases ( x = x1 or x = x2 ) by A2; suppose x = x1 ; ::_thesis: x . i in X . i hence x . i in X . i by A3, TARSKI:def_2; ::_thesis: verum end; suppose x = x2 ; ::_thesis: x . i in X . i hence x . i in X . i by A3, TARSKI:def_2; ::_thesis: verum end; end; end; theorem :: PZFMISC1:7 for I being set for x, A being ManySortedSet of I st x in {A} holds x = A proof let I be set ; ::_thesis: for x, A being ManySortedSet of I st x in {A} holds x = A let x, A be ManySortedSet of I; ::_thesis: ( x in {A} implies x = A ) assume A1: x in {A} ; ::_thesis: x = A now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies x . i = A . i ) assume A2: i in I ; ::_thesis: x . i = A . i then x . i in {A} . i by A1, PBOOLE:def_1; then x . i in {(A . i)} by A2, Def1; hence x . i = A . i by TARSKI:def_1; ::_thesis: verum end; hence x = A by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:8 for I being set for x being ManySortedSet of I holds x in {x} proof let I be set ; ::_thesis: for x being ManySortedSet of I holds x in {x} let x be ManySortedSet of I; ::_thesis: x in {x} let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in {x} . i ) assume A1: i in I ; ::_thesis: x . i in {x} . i x . i in {(x . i)} by TARSKI:def_1; hence x . i in {x} . i by A1, Def1; ::_thesis: verum end; theorem :: PZFMISC1:9 for I being set for x, A, B being ManySortedSet of I st ( x = A or x = B ) holds x in {A,B} proof let I be set ; ::_thesis: for x, A, B being ManySortedSet of I st ( x = A or x = B ) holds x in {A,B} let x, A, B be ManySortedSet of I; ::_thesis: ( ( x = A or x = B ) implies x in {A,B} ) assume A1: ( x = A or x = B ) ; ::_thesis: x in {A,B} percases ( x = A or x = B ) by A1; supposeA2: x = A ; ::_thesis: x in {A,B} let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in {A,B} . i ) assume A3: i in I ; ::_thesis: x . i in {A,B} . i x . i in {(A . i),(B . i)} by A2, TARSKI:def_2; hence x . i in {A,B} . i by A3, Def2; ::_thesis: verum end; supposeA4: x = B ; ::_thesis: x in {A,B} let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in {A,B} . i ) assume A5: i in I ; ::_thesis: x . i in {A,B} . i x . i in {(A . i),(B . i)} by A4, TARSKI:def_2; hence x . i in {A,B} . i by A5, Def2; ::_thesis: verum end; end; end; theorem :: PZFMISC1:10 for I being set for A, B being ManySortedSet of I holds {A} \/ {B} = {A,B} proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds {A} \/ {B} = {A,B} let A, B be ManySortedSet of I; ::_thesis: {A} \/ {B} = {A,B} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({A}_\/_{B})_._i_=_{A,B}_._i let i be set ; ::_thesis: ( i in I implies ({A} \/ {B}) . i = {A,B} . i ) assume A1: i in I ; ::_thesis: ({A} \/ {B}) . i = {A,B} . i hence ({A} \/ {B}) . i = ({A} . i) \/ ({B} . i) by PBOOLE:def_4 .= ({A} . i) \/ {(B . i)} by A1, Def1 .= {(A . i)} \/ {(B . i)} by A1, Def1 .= {(A . i),(B . i)} by ENUMSET1:1 .= {A,B} . i by A1, Def2 ; ::_thesis: verum end; hence {A} \/ {B} = {A,B} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:11 for I being set for x being ManySortedSet of I holds {x,x} = {x} proof let I be set ; ::_thesis: for x being ManySortedSet of I holds {x,x} = {x} let x be ManySortedSet of I; ::_thesis: {x,x} = {x} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ {x,x}_._i_=_{x}_._i let i be set ; ::_thesis: ( i in I implies {x,x} . i = {x} . i ) assume A1: i in I ; ::_thesis: {x,x} . i = {x} . i hence {x,x} . i = {(x . i),(x . i)} by Def2 .= {(x . i)} by ENUMSET1:29 .= {x} . i by A1, Def1 ; ::_thesis: verum end; hence {x,x} = {x} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:12 for I being set for A, B being ManySortedSet of I st {A} c= {B} holds A = B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st {A} c= {B} holds A = B let A, B be ManySortedSet of I; ::_thesis: ( {A} c= {B} implies A = B ) assume A1: {A} c= {B} ; ::_thesis: A = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ A_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies A . i = B . i ) assume A2: i in I ; ::_thesis: A . i = B . i then {A} . i c= {B} . i by A1, PBOOLE:def_2; 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:18; ::_thesis: verum end; hence A = B by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:13 for I being set for x, y being ManySortedSet of I st {x} = {y} holds x = y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st {x} = {y} holds x = y let x, y be ManySortedSet of I; ::_thesis: ( {x} = {y} implies x = y ) assume A1: {x} = {y} ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . i = y . i ) assume A2: i in I ; ::_thesis: x . i = y . i then {(x . i)} = {x} . i by Def1 .= {(y . i)} by A1, A2, Def1 ; hence x . i = y . i by ZFMISC_1:3; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:14 for I being set for x, A, B being ManySortedSet of I st {x} = {A,B} holds ( x = A & x = B ) proof let I be set ; ::_thesis: for x, A, B being ManySortedSet of I st {x} = {A,B} holds ( x = A & x = B ) let x, A, B be ManySortedSet of I; ::_thesis: ( {x} = {A,B} implies ( x = A & x = B ) ) assume A1: {x} = {A,B} ; ::_thesis: ( x = A & x = B ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies x . i = A . i ) assume A2: i in I ; ::_thesis: x . i = A . i then {(x . i)} = {x} . i by Def1 .= {(A . i),(B . i)} by A1, A2, Def2 ; hence x . i = A . i by ZFMISC_1:4; ::_thesis: verum end; hence x = A by PBOOLE:3; ::_thesis: x = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies x . i = B . i ) assume A3: i in I ; ::_thesis: x . i = B . i then {(x . i)} = {x} . i by Def1 .= {(A . i),(B . i)} by A1, A3, Def2 ; hence x . i = B . i by ZFMISC_1:4; ::_thesis: verum end; hence x = B by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:15 for I being set for x, A, B being ManySortedSet of I st {x} = {A,B} holds A = B proof let I be set ; ::_thesis: for x, A, B being ManySortedSet of I st {x} = {A,B} holds A = B let x, A, B be ManySortedSet of I; ::_thesis: ( {x} = {A,B} implies A = B ) assume A1: {x} = {A,B} ; ::_thesis: A = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ A_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies A . i = B . i ) assume A2: i in I ; ::_thesis: A . i = B . i then {(x . i)} = {x} . i by Def1 .= {(A . i),(B . i)} by A1, A2, Def2 ; hence A . i = B . i by ZFMISC_1:5; ::_thesis: verum end; hence A = B by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:16 for I being set for x, y being ManySortedSet of I holds ( {x} c= {x,y} & {y} c= {x,y} ) proof let I be set ; ::_thesis: for x, y being ManySortedSet of I holds ( {x} c= {x,y} & {y} c= {x,y} ) let x, y be ManySortedSet of I; ::_thesis: ( {x} c= {x,y} & {y} c= {x,y} ) thus {x} c= {x,y} ::_thesis: {y} c= {x,y} proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {x} . i c= {x,y} . i ) assume A1: i in I ; ::_thesis: {x} . i c= {x,y} . i {(x . i)} c= {(x . i),(y . i)} by ZFMISC_1:7; then {x} . i c= {(x . i),(y . i)} by A1, Def1; hence {x} . i c= {x,y} . i by A1, Def2; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {y} . i c= {x,y} . i ) assume A2: i in I ; ::_thesis: {y} . i c= {x,y} . i {(y . i)} c= {(x . i),(y . i)} by ZFMISC_1:7; then {y} . i c= {(x . i),(y . i)} by A2, Def1; hence {y} . i c= {x,y} . i by A2, Def2; ::_thesis: verum end; theorem :: PZFMISC1:17 for I being set for x, y being ManySortedSet of I st ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) holds x = y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) holds x = y let x, y be ManySortedSet of I; ::_thesis: ( ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) implies x = y ) assume A1: ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . b1 = y . b1 ) assume A2: i in I ; ::_thesis: x . b1 = y . b1 percases ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) by A1; supposeA3: {x} \/ {y} = {x} ; ::_thesis: x . b1 = y . b1 {(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_4 .= {(x . i)} by A2, A3, Def1 ; hence x . i = y . i by ZFMISC_1:8; ::_thesis: verum end; supposeA4: {x} \/ {y} = {y} ; ::_thesis: x . b1 = y . b1 {(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_4 .= {(y . i)} by A2, A4, Def1 ; hence x . i = y . i by ZFMISC_1:8; ::_thesis: verum end; end; end; hence x = y by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:18 for I being set for x, y being ManySortedSet of I holds {x} \/ {x,y} = {x,y} proof let I be set ; ::_thesis: for x, y being ManySortedSet of I holds {x} \/ {x,y} = {x,y} let x, y be ManySortedSet of I; ::_thesis: {x} \/ {x,y} = {x,y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x}_\/_{x,y})_._i_=_{x,y}_._i let i be set ; ::_thesis: ( i in I implies ({x} \/ {x,y}) . i = {x,y} . i ) assume A1: i in I ; ::_thesis: ({x} \/ {x,y}) . i = {x,y} . i hence ({x} \/ {x,y}) . i = ({x} . i) \/ ({x,y} . i) by PBOOLE:def_4 .= {(x . i)} \/ ({x,y} . i) by A1, Def1 .= {(x . i)} \/ {(x . i),(y . i)} by A1, Def2 .= {(x . i),(y . i)} by ZFMISC_1:9 .= {x,y} . i by A1, Def2 ; ::_thesis: verum end; hence {x} \/ {x,y} = {x,y} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:19 for I being set for x, y being ManySortedSet of I st not I is empty & {x} /\ {y} = [[0]] I holds x <> y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st not I is empty & {x} /\ {y} = [[0]] I holds x <> y let x, y be ManySortedSet of I; ::_thesis: ( not I is empty & {x} /\ {y} = [[0]] I implies x <> y ) assume that A1: not I is empty and A2: {x} /\ {y} = [[0]] I ; ::_thesis: x <> y now__::_thesis:_ex_i_being_set_st_x_._i_<>_y_._i consider i being set such that A3: i in I by A1, XBOOLE_0:def_1; take i = i; ::_thesis: x . i <> y . 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_5 .= {} by A2, PBOOLE:5 ; hence x . i <> y . i ; ::_thesis: verum end; hence x <> y ; ::_thesis: verum end; theorem :: PZFMISC1:20 for I being set for x, y being ManySortedSet of I st ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) holds x = y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) holds x = y let x, y be ManySortedSet of I; ::_thesis: ( ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) implies x = y ) assume A1: ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) ; ::_thesis: x = y percases ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) by A1; supposeA2: {x} /\ {y} = {x} ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . i = y . i ) assume A3: i in I ; ::_thesis: x . i = y . 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_5 .= {(x . i)} by A2, A3, Def1 ; hence x . i = y . i by ZFMISC_1:12; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; supposeA4: {x} /\ {y} = {y} ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . i = y . i ) assume A5: i in I ; ::_thesis: x . i = y . 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_5 .= {(y . i)} by A4, A5, Def1 ; hence x . i = y . i by ZFMISC_1:12; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; end; end; theorem :: PZFMISC1:21 for I being set for x, y being ManySortedSet of I holds ( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} ) proof let I be set ; ::_thesis: for x, y being ManySortedSet of I holds ( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} ) let x, y be ManySortedSet of I; ::_thesis: ( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x}_/\_{x,y})_._i_=_{x}_._i let i be set ; ::_thesis: ( i in I implies ({x} /\ {x,y}) . i = {x} . i ) assume A1: i in I ; ::_thesis: ({x} /\ {x,y}) . i = {x} . i hence ({x} /\ {x,y}) . i = ({x} . i) /\ ({x,y} . i) by PBOOLE:def_5 .= {(x . i)} /\ ({x,y} . i) by A1, Def1 .= {(x . i)} /\ {(x . i),(y . i)} by A1, Def2 .= {(x . i)} by ZFMISC_1:13 .= {x} . i by A1, Def1 ; ::_thesis: verum end; hence {x} /\ {x,y} = {x} by PBOOLE:3; ::_thesis: {y} /\ {x,y} = {y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({y}_/\_{x,y})_._i_=_{y}_._i let i be set ; ::_thesis: ( i in I implies ({y} /\ {x,y}) . i = {y} . i ) assume A2: i in I ; ::_thesis: ({y} /\ {x,y}) . i = {y} . i hence ({y} /\ {x,y}) . i = ({y} . i) /\ ({x,y} . i) by PBOOLE:def_5 .= {(y . i)} /\ ({x,y} . i) by A2, Def1 .= {(y . i)} /\ {(x . i),(y . i)} by A2, Def2 .= {(y . i)} by ZFMISC_1:13 .= {y} . i by A2, Def1 ; ::_thesis: verum end; hence {y} /\ {x,y} = {y} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:22 for I being set for x, y being ManySortedSet of I st not I is empty & {x} \ {y} = {x} holds x <> y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st not I is empty & {x} \ {y} = {x} holds x <> y let x, y be ManySortedSet of I; ::_thesis: ( not I is empty & {x} \ {y} = {x} implies x <> y ) assume that A1: not I is empty and A2: {x} \ {y} = {x} ; ::_thesis: x <> y now__::_thesis:_ex_i_being_set_st_x_._i_<>_y_._i consider i being set such that A3: i in I by A1, XBOOLE_0:def_1; take i = i; ::_thesis: x . i <> y . 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_6 .= {(x . i)} by A2, A3, Def1 ; hence x . i <> y . i by ZFMISC_1:14; ::_thesis: verum end; hence x <> y ; ::_thesis: verum end; theorem :: PZFMISC1:23 for I being set for x, y being ManySortedSet of I st {x} \ {y} = [[0]] I holds x = y proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st {x} \ {y} = [[0]] I holds x = y let x, y be ManySortedSet of I; ::_thesis: ( {x} \ {y} = [[0]] I implies x = y ) assume A1: {x} \ {y} = [[0]] I ; ::_thesis: x = y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_y_._i let i be set ; ::_thesis: ( i in I implies x . i = y . i ) assume A2: i in I ; ::_thesis: x . i = y . 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_6 .= {} by A1, PBOOLE:5 ; hence x . i = y . i by ZFMISC_1:15; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:24 for I being set for x, y being ManySortedSet of I holds ( {x} \ {x,y} = [[0]] I & {y} \ {x,y} = [[0]] I ) proof let I be set ; ::_thesis: for x, y being ManySortedSet of I holds ( {x} \ {x,y} = [[0]] I & {y} \ {x,y} = [[0]] I ) let x, y be ManySortedSet of I; ::_thesis: ( {x} \ {x,y} = [[0]] I & {y} \ {x,y} = [[0]] I ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x}_\_{x,y})_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ({x} \ {x,y}) . i = ([[0]] I) . i ) assume A1: i in I ; ::_thesis: ({x} \ {x,y}) . i = ([[0]] I) . i hence ({x} \ {x,y}) . i = ({x} . i) \ ({x,y} . i) by PBOOLE:def_6 .= {(x . i)} \ ({x,y} . i) by A1, Def1 .= {(x . i)} \ {(x . i),(y . i)} by A1, Def2 .= {} by ZFMISC_1:16 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence {x} \ {x,y} = [[0]] I by PBOOLE:3; ::_thesis: {y} \ {x,y} = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({y}_\_{x,y})_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ({y} \ {x,y}) . i = ([[0]] I) . i ) assume A2: i in I ; ::_thesis: ({y} \ {x,y}) . i = ([[0]] I) . i hence ({y} \ {x,y}) . i = ({y} . i) \ ({x,y} . i) by PBOOLE:def_6 .= {(y . i)} \ ({x,y} . i) by A2, Def1 .= {(y . i)} \ {(x . i),(y . i)} by A2, Def2 .= {} by ZFMISC_1:16 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence {y} \ {x,y} = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:25 for I being set for x, y being ManySortedSet of I st {x} c= {y} holds {x} = {y} proof let I be set ; ::_thesis: for x, y being ManySortedSet of I st {x} c= {y} holds {x} = {y} let x, y be ManySortedSet of I; ::_thesis: ( {x} c= {y} implies {x} = {y} ) assume A1: {x} c= {y} ; ::_thesis: {x} = {y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ {x}_._i_=_{y}_._i let i be set ; ::_thesis: ( i in I implies {x} . i = {y} . i ) assume A2: i in I ; ::_thesis: {x} . i = {y} . i then {x} . i c= {y} . i by A1, PBOOLE:def_2; 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:18 .= {y} . i by A2, Def1 ; ::_thesis: verum end; hence {x} = {y} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:26 for I being set for x, y, A being ManySortedSet of I st {x,y} c= {A} holds ( x = A & y = A ) proof let I be set ; ::_thesis: for x, y, A being ManySortedSet of I st {x,y} c= {A} holds ( x = A & y = A ) let x, y, A be ManySortedSet of I; ::_thesis: ( {x,y} c= {A} implies ( x = A & y = A ) ) assume A1: {x,y} c= {A} ; ::_thesis: ( x = A & y = A ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies x . i = A . i ) assume A2: i in I ; ::_thesis: x . i = A . i then {x,y} . i c= {A} . i by A1, PBOOLE:def_2; 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:20; ::_thesis: verum end; hence x = A by PBOOLE:3; ::_thesis: y = A now__::_thesis:_for_i_being_set_st_i_in_I_holds_ y_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies y . i = A . i ) assume A3: i in I ; ::_thesis: y . i = A . i then {x,y} . i c= {A} . i by A1, PBOOLE:def_2; 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:20; ::_thesis: verum end; hence y = A by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:27 for I being set for x, y, A being ManySortedSet of I st {x,y} c= {A} holds {x,y} = {A} proof let I be set ; ::_thesis: for x, y, A being ManySortedSet of I st {x,y} c= {A} holds {x,y} = {A} let x, y, A be ManySortedSet of I; ::_thesis: ( {x,y} c= {A} implies {x,y} = {A} ) assume A1: {x,y} c= {A} ; ::_thesis: {x,y} = {A} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ {x,y}_._i_=_{A}_._i let i be set ; ::_thesis: ( i in I implies {x,y} . i = {A} . i ) assume A2: i in I ; ::_thesis: {x,y} . i = {A} . i then {x,y} . i c= {A} . i by A1, PBOOLE:def_2; 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:21 .= {A} . i by A2, Def1 ; ::_thesis: verum end; hence {x,y} = {A} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:28 for I being set for x being ManySortedSet of I holds bool {x} = {([[0]] I),{x}} proof let I be set ; ::_thesis: for x being ManySortedSet of I holds bool {x} = {([[0]] I),{x}} let x be ManySortedSet of I; ::_thesis: bool {x} = {([[0]] I),{x}} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (bool_{x})_._i_=_{([[0]]_I),{x}}_._i let i be set ; ::_thesis: ( i in I implies (bool {x}) . i = {([[0]] I),{x}} . i ) assume A1: i in I ; ::_thesis: (bool {x}) . i = {([[0]] I),{x}} . i hence (bool {x}) . i = bool ({x} . i) by MBOOLEAN:def_1 .= bool {(x . i)} by A1, Def1 .= {{},{(x . i)}} by ZFMISC_1:24 .= {(([[0]] I) . i),{(x . i)}} by PBOOLE:5 .= {(([[0]] I) . i),({x} . i)} by A1, Def1 .= {([[0]] I),{x}} . i by A1, Def2 ; ::_thesis: verum end; hence bool {x} = {([[0]] I),{x}} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:29 for I being set for A being ManySortedSet of I holds {A} c= bool A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds {A} c= bool A let A be ManySortedSet of I; ::_thesis: {A} c= bool A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {A} . i c= (bool A) . i ) assume A1: i in I ; ::_thesis: {A} . i c= (bool A) . i {(A . i)} c= bool (A . i) by ZFMISC_1:68; then {A} . i c= bool (A . i) by A1, Def1; hence {A} . i c= (bool A) . i by A1, MBOOLEAN:def_1; ::_thesis: verum end; theorem :: PZFMISC1:30 for I being set for x being ManySortedSet of I holds union {x} = x proof let I be set ; ::_thesis: for x being ManySortedSet of I holds union {x} = x let x be ManySortedSet of I; ::_thesis: union {x} = x now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_{x})_._i_=_x_._i let i be set ; ::_thesis: ( i in I implies (union {x}) . i = x . i ) assume A1: i in I ; ::_thesis: (union {x}) . i = x . i hence (union {x}) . i = union ({x} . i) by MBOOLEAN:def_2 .= union {(x . i)} by A1, Def1 .= x . i by ZFMISC_1:25 ; ::_thesis: verum end; hence union {x} = x by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:31 for I being set for x, y being ManySortedSet of I holds union {{x},{y}} = {x,y} proof let I be set ; ::_thesis: for x, y being ManySortedSet of I holds union {{x},{y}} = {x,y} let x, y be ManySortedSet of I; ::_thesis: union {{x},{y}} = {x,y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_{{x},{y}})_._i_=_{x,y}_._i let i be set ; ::_thesis: ( i in I implies (union {{x},{y}}) . i = {x,y} . i ) assume A1: i in I ; ::_thesis: (union {{x},{y}}) . i = {x,y} . 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:26 .= {x,y} . i by A1, Def2 ; ::_thesis: verum end; hence union {{x},{y}} = {x,y} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:32 for I being set for A, B being ManySortedSet of I holds union {A,B} = A \/ B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union {A,B} = A \/ B let A, B be ManySortedSet of I; ::_thesis: union {A,B} = A \/ B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_{A,B})_._i_=_(A_\/_B)_._i let i be set ; ::_thesis: ( i in I implies (union {A,B}) . i = (A \/ B) . i ) assume A1: i in I ; ::_thesis: (union {A,B}) . i = (A \/ B) . 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:75 .= (A \/ B) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence union {A,B} = A \/ B by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:33 for I being set for x, X being ManySortedSet of I holds ( {x} c= X iff x in X ) proof let I be set ; ::_thesis: for x, X being ManySortedSet of I holds ( {x} c= X iff x in X ) let x, X be ManySortedSet of I; ::_thesis: ( {x} c= X iff x in X ) thus ( {x} c= X implies x in X ) ::_thesis: ( x in X implies {x} c= X ) proof assume A1: {x} c= X ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A2: i in I ; ::_thesis: x . i in X . i then {x} . i c= X . i by A1, PBOOLE:def_2; then {(x . i)} c= X . i by A2, Def1; hence x . i in X . i by ZFMISC_1:31; ::_thesis: verum end; assume A3: x in X ; ::_thesis: {x} c= X let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {x} . i c= X . i ) assume A4: i in I ; ::_thesis: {x} . i c= X . i then x . i in X . i by A3, PBOOLE:def_1; then {(x . i)} c= X . i by ZFMISC_1:31; hence {x} . i c= X . i by A4, Def1; ::_thesis: verum end; theorem :: PZFMISC1:34 for I being set for x1, x2, X being ManySortedSet of I holds ( {x1,x2} c= X iff ( x1 in X & x2 in X ) ) proof let I be set ; ::_thesis: for x1, x2, X being ManySortedSet of I holds ( {x1,x2} c= X iff ( x1 in X & x2 in X ) ) let x1, x2, X be ManySortedSet of I; ::_thesis: ( {x1,x2} c= X iff ( x1 in X & x2 in X ) ) thus ( {x1,x2} c= X implies ( x1 in X & x2 in X ) ) ::_thesis: ( x1 in X & x2 in X implies {x1,x2} c= X ) proof assume A1: {x1,x2} c= X ; ::_thesis: ( x1 in X & x2 in X ) thus x1 in X ::_thesis: x2 in X proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x1 . i in X . i ) assume A2: i in I ; ::_thesis: x1 . i in X . i then {x1,x2} . i c= X . i by A1, PBOOLE:def_2; then {(x1 . i),(x2 . i)} c= X . i by A2, Def2; hence x1 . i in X . i by ZFMISC_1:32; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x2 . i in X . i ) assume A3: i in I ; ::_thesis: x2 . i in X . i then {x1,x2} . i c= X . i by A1, PBOOLE:def_2; then {(x1 . i),(x2 . i)} c= X . i by A3, Def2; hence x2 . i in X . i by ZFMISC_1:32; ::_thesis: verum end; assume that A4: x1 in X and A5: x2 in X ; ::_thesis: {x1,x2} c= X let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {x1,x2} . i c= X . i ) assume A6: i in I ; ::_thesis: {x1,x2} . i c= X . i then A7: x1 . i in X . i by A4, PBOOLE:def_1; x2 . i in X . i by A5, A6, PBOOLE:def_1; then {(x1 . i),(x2 . i)} c= X . i by A7, ZFMISC_1:32; hence {x1,x2} . i c= X . i by A6, Def2; ::_thesis: verum end; theorem :: PZFMISC1:35 for I being set for A, x1, x2 being ManySortedSet of I st ( A = [[0]] I or A = {x1} or A = {x2} or A = {x1,x2} ) holds A c= {x1,x2} proof let I be set ; ::_thesis: for A, x1, x2 being ManySortedSet of I st ( A = [[0]] I or A = {x1} or A = {x2} or A = {x1,x2} ) holds A c= {x1,x2} let A, x1, x2 be ManySortedSet of I; ::_thesis: ( ( A = [[0]] I or A = {x1} or A = {x2} or A = {x1,x2} ) implies A c= {x1,x2} ) assume A1: ( A = [[0]] I or A = {x1} or A = {x2} or A = {x1,x2} ) ; ::_thesis: A c= {x1,x2} let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= {x1,x2} . i ) assume A2: i in I ; ::_thesis: A . i c= {x1,x2} . i percases ( A = [[0]] I or A = {x1} or A = {x2} or A = {x1,x2} ) by A1; suppose A = [[0]] I ; ::_thesis: A . i c= {x1,x2} . i then A . i = {} by PBOOLE:5; then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36; hence A . i c= {x1,x2} . i by A2, Def2; ::_thesis: verum end; suppose A = {x1} ; ::_thesis: A . i c= {x1,x2} . i then A . i = {(x1 . i)} by A2, Def1; then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36; hence A . i c= {x1,x2} . i by A2, Def2; ::_thesis: verum end; suppose A = {x2} ; ::_thesis: A . i c= {x1,x2} . i then A . i = {(x2 . i)} by A2, Def1; then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36; hence A . i c= {x1,x2} . i by A2, Def2; ::_thesis: verum end; suppose A = {x1,x2} ; ::_thesis: A . i c= {x1,x2} . i hence A . i c= {x1,x2} . i ; ::_thesis: verum end; end; end; begin theorem :: PZFMISC1:36 for I being set for x, A, B being ManySortedSet of I st ( x in A or x = B ) holds x in A \/ {B} proof let I be set ; ::_thesis: for x, A, B being ManySortedSet of I st ( x in A or x = B ) holds x in A \/ {B} let x, A, B be ManySortedSet of I; ::_thesis: ( ( x in A or x = B ) implies x in A \/ {B} ) assume A1: ( x in A or x = B ) ; ::_thesis: x in A \/ {B} let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in (A \/ {B}) . i ) assume A2: i in I ; ::_thesis: x . i in (A \/ {B}) . i percases ( x in A or x = B ) by A1; suppose x in A ; ::_thesis: x . i in (A \/ {B}) . i then x . i in A . i by A2, PBOOLE:def_1; then x . i in (A . i) \/ {(B . i)} by ZFMISC_1:136; then x . i in (A . i) \/ ({B} . i) by A2, Def1; hence x . i in (A \/ {B}) . i by A2, PBOOLE:def_4; ::_thesis: verum end; suppose x = B ; ::_thesis: x . i in (A \/ {B}) . i then x . i in (A . i) \/ {(B . i)} by ZFMISC_1:136; then x . i in (A . i) \/ ({B} . i) by A2, Def1; hence x . i in (A \/ {B}) . i by A2, PBOOLE:def_4; ::_thesis: verum end; end; end; theorem :: PZFMISC1:37 for I being set for A, x, B being ManySortedSet of I holds ( A \/ {x} c= B iff ( x in B & A c= B ) ) proof let I be set ; ::_thesis: for A, x, B being ManySortedSet of I holds ( A \/ {x} c= B iff ( x in B & A c= B ) ) let A, x, B be ManySortedSet of I; ::_thesis: ( A \/ {x} c= B iff ( x in B & A c= B ) ) thus ( A \/ {x} c= B implies ( x in B & A c= B ) ) ::_thesis: ( x in B & A c= B implies A \/ {x} c= B ) proof assume A1: A \/ {x} c= B ; ::_thesis: ( x in B & A c= B ) A2: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (A_._i)_\/_{(x_._i)}_c=_B_._i let i be set ; ::_thesis: ( i in I implies (A . i) \/ {(x . i)} c= B . i ) assume A3: i in I ; ::_thesis: (A . i) \/ {(x . i)} c= B . i then (A \/ {x}) . i c= B . i by A1, PBOOLE:def_2; then (A . i) \/ ({x} . i) c= B . i by A3, PBOOLE:def_4; hence (A . i) \/ {(x . i)} c= B . i by A3, Def1; ::_thesis: verum end; thus x in B ::_thesis: A c= B proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in B . i ) assume i in I ; ::_thesis: x . i in B . i then (A . i) \/ {(x . i)} c= B . i by A2; hence x . i in B . i by ZFMISC_1:137; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= B . i ) assume i in I ; ::_thesis: A . i c= B . i then (A . i) \/ {(x . i)} c= B . i by A2; hence A . i c= B . i by ZFMISC_1:137; ::_thesis: verum end; assume that A4: x in B and A5: A c= B ; ::_thesis: A \/ {x} c= B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (A \/ {x}) . i c= B . i ) assume A6: i in I ; ::_thesis: (A \/ {x}) . i c= B . i then A7: x . i in B . i by A4, PBOOLE:def_1; A . i c= B . i by A5, A6, PBOOLE:def_2; then (A . i) \/ {(x . i)} c= B . i by A7, ZFMISC_1:137; then (A . i) \/ ({x} . i) c= B . i by A6, Def1; hence (A \/ {x}) . i c= B . i by A6, PBOOLE:def_4; ::_thesis: verum end; theorem :: PZFMISC1:38 for I being set for x, X being ManySortedSet of I st {x} \/ X = X holds x in X proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st {x} \/ X = X holds x in X let x, X be ManySortedSet of I; ::_thesis: ( {x} \/ X = X implies x in X ) assume A1: {x} \/ X = X ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A2: i in I ; ::_thesis: x . i in X . i then {(x . i)} \/ (X . i) = ({x} . i) \/ (X . i) by Def1 .= X . i by A1, A2, PBOOLE:def_4 ; hence x . i in X . i by ZFMISC_1:39; ::_thesis: verum end; theorem :: PZFMISC1:39 for I being set for x, X being ManySortedSet of I st x in X holds {x} \/ X = X proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st x in X holds {x} \/ X = X let x, X be ManySortedSet of I; ::_thesis: ( x in X implies {x} \/ X = X ) assume A1: x in X ; ::_thesis: {x} \/ X = X now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x}_\/_X)_._i_=_X_._i let i be set ; ::_thesis: ( i in I implies ({x} \/ X) . i = X . i ) assume A2: i in I ; ::_thesis: ({x} \/ X) . i = X . i then A3: x . i in X . i by A1, PBOOLE:def_1; thus ({x} \/ X) . i = ({x} . i) \/ (X . i) by A2, PBOOLE:def_4 .= {(x . i)} \/ (X . i) by A2, Def1 .= X . i by A3, ZFMISC_1:40 ; ::_thesis: verum end; hence {x} \/ X = X by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:40 for I being set for x, y, A being ManySortedSet of I holds ( {x,y} \/ A = A iff ( x in A & y in A ) ) proof let I be set ; ::_thesis: for x, y, A being ManySortedSet of I holds ( {x,y} \/ A = A iff ( x in A & y in A ) ) let x, y, A be ManySortedSet of I; ::_thesis: ( {x,y} \/ A = A iff ( x in A & y in A ) ) thus ( {x,y} \/ A = A implies ( x in A & y in A ) ) ::_thesis: ( x in A & y in A implies {x,y} \/ A = A ) proof assume A1: {x,y} \/ A = A ; ::_thesis: ( x in A & y in A ) thus x in A ::_thesis: y in A proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in A . i ) assume A2: i in I ; ::_thesis: x . i in A . i then {(x . i),(y . i)} \/ (A . i) = ({x,y} . i) \/ (A . i) by Def2 .= A . i by A1, A2, PBOOLE:def_4 ; hence x . i in A . i by ZFMISC_1:41; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or y . i in A . i ) assume A3: i in I ; ::_thesis: y . i in A . i then {(x . i),(y . i)} \/ (A . i) = ({x,y} . i) \/ (A . i) by Def2 .= A . i by A1, A3, PBOOLE:def_4 ; hence y . i in A . i by ZFMISC_1:41; ::_thesis: verum end; assume that A4: x in A and A5: y in A ; ::_thesis: {x,y} \/ A = A now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x,y}_\/_A)_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies ({x,y} \/ A) . i = A . i ) assume A6: i in I ; ::_thesis: ({x,y} \/ A) . i = A . i then A7: x . i in A . i by A4, PBOOLE:def_1; A8: y . i in A . i by A5, A6, PBOOLE:def_1; thus ({x,y} \/ A) . i = ({x,y} . i) \/ (A . i) by A6, PBOOLE:def_4 .= {(x . i),(y . i)} \/ (A . i) by A6, Def2 .= A . i by A7, A8, ZFMISC_1:42 ; ::_thesis: verum end; hence {x,y} \/ A = A by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:41 for I being set for x, X being ManySortedSet of I st not I is empty holds {x} \/ X <> [[0]] I proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st not I is empty holds {x} \/ X <> [[0]] I let x, X be ManySortedSet of I; ::_thesis: ( not I is empty implies {x} \/ X <> [[0]] I ) assume that A1: not I is empty and A2: {x} \/ X = [[0]] I ; ::_thesis: contradiction consider i being set 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_4; hence contradiction by A2, PBOOLE:5; ::_thesis: verum end; theorem :: PZFMISC1:42 for I being set for x, y, X being ManySortedSet of I st not I is empty holds {x,y} \/ X <> [[0]] I proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I st not I is empty holds {x,y} \/ X <> [[0]] I let x, y, X be ManySortedSet of I; ::_thesis: ( not I is empty implies {x,y} \/ X <> [[0]] I ) assume that A1: not I is empty and A2: {x,y} \/ X = [[0]] I ; ::_thesis: contradiction consider i being set 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_4; hence contradiction by A2, PBOOLE:5; ::_thesis: verum end; begin theorem :: PZFMISC1:43 for I being set for X, x being ManySortedSet of I st X /\ {x} = {x} holds x in X proof let I be set ; ::_thesis: for X, x being ManySortedSet of I st X /\ {x} = {x} holds x in X let X, x be ManySortedSet of I; ::_thesis: ( X /\ {x} = {x} implies x in X ) assume A1: X /\ {x} = {x} ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A2: i in I ; ::_thesis: x . i in X . i then (X . i) /\ {(x . i)} = (X . i) /\ ({x} . i) by Def1 .= (X /\ {x}) . i by A2, PBOOLE:def_5 .= {(x . i)} by A1, A2, Def1 ; hence x . i in X . i by ZFMISC_1:45; ::_thesis: verum end; theorem :: PZFMISC1:44 for I being set for x, X being ManySortedSet of I st x in X holds X /\ {x} = {x} proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st x in X holds X /\ {x} = {x} let x, X be ManySortedSet of I; ::_thesis: ( x in X implies X /\ {x} = {x} ) assume A1: x in X ; ::_thesis: X /\ {x} = {x} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (X_/\_{x})_._i_=_{x}_._i let i be set ; ::_thesis: ( i in I implies (X /\ {x}) . i = {x} . i ) assume A2: i in I ; ::_thesis: (X /\ {x}) . i = {x} . i then A3: x . i in X . i by A1, PBOOLE:def_1; thus (X /\ {x}) . i = (X . i) /\ ({x} . i) by A2, PBOOLE:def_5 .= (X . i) /\ {(x . i)} by A2, Def1 .= {(x . i)} by A3, ZFMISC_1:46 .= {x} . i by A2, Def1 ; ::_thesis: verum end; hence X /\ {x} = {x} by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:45 for I being set for x, X, y being ManySortedSet of I holds ( ( x in X & y in X ) iff {x,y} /\ X = {x,y} ) proof let I be set ; ::_thesis: for x, X, y being ManySortedSet of I holds ( ( x in X & y in X ) iff {x,y} /\ X = {x,y} ) let x, X, y be ManySortedSet of I; ::_thesis: ( ( x in X & y in X ) iff {x,y} /\ X = {x,y} ) thus ( x in X & y in X implies {x,y} /\ X = {x,y} ) ::_thesis: ( {x,y} /\ X = {x,y} implies ( x in X & y in X ) ) proof assume that A1: x in X and A2: y in X ; ::_thesis: {x,y} /\ X = {x,y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x,y}_/\_X)_._i_=_{x,y}_._i let i be set ; ::_thesis: ( i in I implies ({x,y} /\ X) . i = {x,y} . i ) assume A3: i in I ; ::_thesis: ({x,y} /\ X) . i = {x,y} . i then A4: x . i in X . i by A1, PBOOLE:def_1; A5: y . i in X . i by A2, A3, PBOOLE:def_1; thus ({x,y} /\ X) . i = ({x,y} . i) /\ (X . i) by A3, PBOOLE:def_5 .= {(x . i),(y . i)} /\ (X . i) by A3, Def2 .= {(x . i),(y . i)} by A4, A5, ZFMISC_1:47 .= {x,y} . i by A3, Def2 ; ::_thesis: verum end; hence {x,y} /\ X = {x,y} by PBOOLE:3; ::_thesis: verum end; assume A6: {x,y} /\ X = {x,y} ; ::_thesis: ( x in X & y in X ) thus x in X ::_thesis: y in X proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A7: i in I ; ::_thesis: x . i in X . i then {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2 .= ({x,y} /\ X) . i by A7, PBOOLE:def_5 .= {(x . i),(y . i)} by A6, A7, Def2 ; hence x . i in X . i by ZFMISC_1:55; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or y . i in X . i ) assume A8: i in I ; ::_thesis: y . i in X . i then {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2 .= ({x,y} /\ X) . i by A8, PBOOLE:def_5 .= {(x . i),(y . i)} by A6, A8, Def2 ; hence y . i in X . i by ZFMISC_1:55; ::_thesis: verum end; theorem :: PZFMISC1:46 for I being set for x, X being ManySortedSet of I st not I is empty & {x} /\ X = [[0]] I holds not x in X proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st not I is empty & {x} /\ X = [[0]] I holds not x in X let x, X be ManySortedSet of I; ::_thesis: ( not I is empty & {x} /\ X = [[0]] I implies not x in X ) assume that A1: not I is empty and A2: {x} /\ X = [[0]] I and A3: x in X ; ::_thesis: contradiction consider i being set 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_5 .= {} by A2, PBOOLE:5 ; then {(x . i)} misses X . i by XBOOLE_0:def_7; then not x . i in X . i by ZFMISC_1:48; hence contradiction by A3, A4, PBOOLE:def_1; ::_thesis: verum end; theorem :: PZFMISC1:47 for I being set for x, y, X being ManySortedSet of I st not I is empty & {x,y} /\ X = [[0]] I holds ( not x in X & not y in X ) proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} /\ X = [[0]] I holds ( not x in X & not y in X ) let x, y, X be ManySortedSet of I; ::_thesis: ( not I is empty & {x,y} /\ X = [[0]] I implies ( not x in X & not y in X ) ) assume that A1: not I is empty and A2: {x,y} /\ X = [[0]] I ; ::_thesis: ( not x in X & not y in X ) A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ {(x_._i),(y_._i)}_/\_(X_._i)_=_{} let i be set ; ::_thesis: ( i in I implies {(x . i),(y . i)} /\ (X . i) = {} ) assume A4: i in I ; ::_thesis: {(x . i),(y . i)} /\ (X . i) = {} hence {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2 .= ({x,y} /\ X) . i by A4, PBOOLE:def_5 .= {} by A2, PBOOLE:5 ; ::_thesis: verum end; thus not x in X ::_thesis: not y in X proof assume A5: x in X ; ::_thesis: contradiction now__::_thesis:_ex_i_being_set_st_ (_i_in_I_&_not_x_._i_in_X_._i_) consider i being set such that A6: i in I by A1, XBOOLE_0:def_1; take i = i; ::_thesis: ( i in I & not x . i in X . 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:49; ::_thesis: verum end; hence contradiction by A5, PBOOLE:def_1; ::_thesis: verum end; assume A7: y in X ; ::_thesis: contradiction now__::_thesis:_ex_i_being_set_st_ (_i_in_I_&_not_y_._i_in_X_._i_) consider i being set such that A8: i in I by A1, XBOOLE_0:def_1; take i = i; ::_thesis: ( i in I & not y . i in X . 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:49; ::_thesis: verum end; hence contradiction by A7, PBOOLE:def_1; ::_thesis: verum end; begin theorem :: PZFMISC1:48 for I being set for y, X, x being ManySortedSet of I st y in X \ {x} holds y in X proof let I be set ; ::_thesis: for y, X, x being ManySortedSet of I st y in X \ {x} holds y in X let y, X, x be ManySortedSet of I; ::_thesis: ( y in X \ {x} implies y in X ) assume A1: y in X \ {x} ; ::_thesis: y in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or y . i in X . i ) assume A2: i in I ; ::_thesis: y . i in X . i then y . i in (X \ {x}) . i by A1, PBOOLE:def_1; then y . i in (X . i) \ ({x} . i) by A2, PBOOLE:def_6; then y . i in (X . i) \ {(x . i)} by A2, Def1; hence y . i in X . i by ZFMISC_1:56; ::_thesis: verum end; theorem :: PZFMISC1:49 for I being set for y, X, x being ManySortedSet of I st not I is empty & y in X \ {x} holds y <> x proof let I be set ; ::_thesis: for y, X, x being ManySortedSet of I st not I is empty & y in X \ {x} holds y <> x let y, X, x be ManySortedSet of I; ::_thesis: ( not I is empty & y in X \ {x} implies y <> x ) assume that A1: not I is empty and A2: y in X \ {x} ; ::_thesis: y <> x consider i being set such that A3: i in I by A1, XBOOLE_0:def_1; now__::_thesis:_ex_i_being_set_st_y_._i_<>_x_._i take i = i; ::_thesis: y . i <> x . i y . i in (X \ {x}) . i by A2, A3, PBOOLE:def_1; then y . i in (X . i) \ ({x} . i) by A3, PBOOLE:def_6; then y . i in (X . i) \ {(x . i)} by A3, Def1; hence y . i <> x . i by ZFMISC_1:56; ::_thesis: verum end; hence y <> x ; ::_thesis: verum end; theorem :: PZFMISC1:50 for I being set for X, x being ManySortedSet of I st not I is empty & X \ {x} = X holds not x in X proof let I be set ; ::_thesis: for X, x being ManySortedSet of I st not I is empty & X \ {x} = X holds not x in X let X, x be ManySortedSet of I; ::_thesis: ( not I is empty & X \ {x} = X implies not x in X ) assume that A1: not I is empty and A2: X \ {x} = X and A3: x in X ; ::_thesis: contradiction A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (X_._i)_\_{(x_._i)}_=_X_._i let i be set ; ::_thesis: ( i in I implies (X . i) \ {(x . i)} = X . i ) assume A5: i in I ; ::_thesis: (X . i) \ {(x . i)} = X . i hence (X . i) \ {(x . i)} = (X . i) \ ({x} . i) by Def1 .= X . i by A2, A5, PBOOLE:def_6 ; ::_thesis: verum end; now__::_thesis:_ex_i_being_set_st_ (_i_in_I_&_not_x_._i_in_X_._i_) consider i being set such that A6: i in I by A1, XBOOLE_0:def_1; take i = i; ::_thesis: ( i in I & not x . i in X . i ) thus i in I by A6; ::_thesis: not x . i in X . i (X . i) \ {(x . i)} = X . i by A4, A6; hence not x . i in X . i by ZFMISC_1:57; ::_thesis: verum end; hence contradiction by A3, PBOOLE:def_1; ::_thesis: verum end; theorem :: PZFMISC1:51 for I being set for x, X being ManySortedSet of I st not I is empty & {x} \ X = {x} holds not x in X proof let I be set ; ::_thesis: for x, X being ManySortedSet of I st not I is empty & {x} \ X = {x} holds not x in X let x, X be ManySortedSet of I; ::_thesis: ( not I is empty & {x} \ X = {x} implies not x in X ) assume that A1: not I is empty and A2: {x} \ X = {x} and A3: x in X ; ::_thesis: contradiction consider i being set 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_6 .= {(x . i)} by A2, A4, Def1 ; then not x . i in X . i by ZFMISC_1:59; hence contradiction by A3, A4, PBOOLE:def_1; ::_thesis: verum end; theorem :: PZFMISC1:52 for I being set for x, X being ManySortedSet of I holds ( {x} \ X = [[0]] I iff x in X ) proof let I be set ; ::_thesis: for x, X being ManySortedSet of I holds ( {x} \ X = [[0]] I iff x in X ) let x, X be ManySortedSet of I; ::_thesis: ( {x} \ X = [[0]] I iff x in X ) thus ( {x} \ X = [[0]] I implies x in X ) ::_thesis: ( x in X implies {x} \ X = [[0]] I ) proof assume A1: {x} \ X = [[0]] I ; ::_thesis: x in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A2: i in I ; ::_thesis: x . i in X . i then {(x . i)} \ (X . i) = ({x} . i) \ (X . i) by Def1 .= ({x} \ X) . i by A2, PBOOLE:def_6 .= {} by A1, PBOOLE:5 ; hence x . i in X . i by ZFMISC_1:60; ::_thesis: verum end; assume A3: x in X ; ::_thesis: {x} \ X = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x}_\_X)_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ({x} \ X) . i = ([[0]] I) . i ) assume A4: i in I ; ::_thesis: ({x} \ X) . i = ([[0]] I) . i then A5: x . i in X . i by A3, PBOOLE:def_1; thus ({x} \ X) . i = ({x} . i) \ (X . i) by A4, PBOOLE:def_6 .= {(x . i)} \ (X . i) by A4, Def1 .= {} by A5, ZFMISC_1:60 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence {x} \ X = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:53 for I being set for x, y, X being ManySortedSet of I st not I is empty & {x,y} \ X = {x} holds not x in X proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} \ X = {x} holds not x in X let x, y, X be ManySortedSet of I; ::_thesis: ( not I is empty & {x,y} \ X = {x} implies not x in X ) assume that A1: not I is empty and A2: {x,y} \ X = {x} ; ::_thesis: not x in X consider i being set 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_6 .= {(x . i)} by A2, A3, Def1 ; then not x . i in X . i by ZFMISC_1:62; hence not x in X by A3, PBOOLE:def_1; ::_thesis: verum end; theorem :: PZFMISC1:54 for I being set for x, y, X being ManySortedSet of I st not I is empty & {x,y} \ X = {x,y} holds ( not x in X & not y in X ) proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} \ X = {x,y} holds ( not x in X & not y in X ) let x, y, X be ManySortedSet of I; ::_thesis: ( not I is empty & {x,y} \ X = {x,y} implies ( not x in X & not y in X ) ) assume not I is empty ; ::_thesis: ( not {x,y} \ X = {x,y} or ( not x in X & not y in X ) ) then consider i being set 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 ) ) ::_thesis: verum proof assume A2: {x,y} \ X = {x,y} ; ::_thesis: ( not x in X & not y in X ) thus not x in X ::_thesis: not y in X proof assume A3: x in X ; ::_thesis: contradiction {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by A1, Def2 .= ({x,y} \ X) . i by A1, PBOOLE:def_6 .= {(x . i),(y . i)} by A1, A2, Def2 ; then not x . i in X . i by ZFMISC_1:63; hence contradiction by A1, A3, PBOOLE:def_1; ::_thesis: verum end; assume A4: y in X ; ::_thesis: contradiction {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by A1, Def2 .= ({x,y} \ X) . i by A1, PBOOLE:def_6 .= {(x . i),(y . i)} by A1, A2, Def2 ; then not y . i in X . i by ZFMISC_1:63; hence contradiction by A1, A4, PBOOLE:def_1; ::_thesis: verum end; end; theorem :: PZFMISC1:55 for I being set for x, y, X being ManySortedSet of I holds ( {x,y} \ X = [[0]] I iff ( x in X & y in X ) ) proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I holds ( {x,y} \ X = [[0]] I iff ( x in X & y in X ) ) let x, y, X be ManySortedSet of I; ::_thesis: ( {x,y} \ X = [[0]] I iff ( x in X & y in X ) ) thus ( {x,y} \ X = [[0]] I implies ( x in X & y in X ) ) ::_thesis: ( x in X & y in X implies {x,y} \ X = [[0]] I ) proof assume A1: {x,y} \ X = [[0]] I ; ::_thesis: ( x in X & y in X ) thus x in X ::_thesis: y in X proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or x . i in X . i ) assume A2: i in I ; ::_thesis: x . i in X . i then {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2 .= ({x,y} \ X) . i by A2, PBOOLE:def_6 .= {} by A1, PBOOLE:5 ; hence x . i in X . i by ZFMISC_1:64; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or y . i in X . i ) assume A3: i in I ; ::_thesis: y . i in X . i then {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2 .= ({x,y} \ X) . i by A3, PBOOLE:def_6 .= {} by A1, PBOOLE:5 ; hence y . i in X . i by ZFMISC_1:64; ::_thesis: verum end; assume that A4: x in X and A5: y in X ; ::_thesis: {x,y} \ X = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ({x,y}_\_X)_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ({x,y} \ X) . i = ([[0]] I) . i ) assume A6: i in I ; ::_thesis: ({x,y} \ X) . i = ([[0]] I) . i then A7: x . i in X . i by A4, PBOOLE:def_1; A8: y . i in X . i by A5, A6, PBOOLE:def_1; thus ({x,y} \ X) . i = ({x,y} . i) \ (X . i) by A6, PBOOLE:def_6 .= {(x . i),(y . i)} \ (X . i) by A6, Def2 .= {} by A7, A8, ZFMISC_1:64 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence {x,y} \ X = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:56 for I being set for X, x, y being ManySortedSet of I st ( X = [[0]] I or X = {x} or X = {y} or X = {x,y} ) holds X \ {x,y} = [[0]] I proof let I be set ; ::_thesis: for X, x, y being ManySortedSet of I st ( X = [[0]] I or X = {x} or X = {y} or X = {x,y} ) holds X \ {x,y} = [[0]] I let X, x, y be ManySortedSet of I; ::_thesis: ( ( X = [[0]] I or X = {x} or X = {y} or X = {x,y} ) implies X \ {x,y} = [[0]] I ) assume A1: ( X = [[0]] I or X = {x} or X = {y} or X = {x,y} ) ; ::_thesis: X \ {x,y} = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (X_\_{x,y})_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies (X \ {x,y}) . b1 = ([[0]] I) . b1 ) assume A2: i in I ; ::_thesis: (X \ {x,y}) . b1 = ([[0]] I) . b1 percases ( X = [[0]] I or X = {x} or X = {y} or X = {x,y} ) by A1; suppose X = [[0]] I ; ::_thesis: (X \ {x,y}) . b1 = ([[0]] I) . b1 then A3: X . i = {} by PBOOLE:5; thus (X \ {x,y}) . i = (X . i) \ ({x,y} . i) by A2, PBOOLE:def_6 .= ([[0]] I) . i by A3, PBOOLE:5 ; ::_thesis: verum end; suppose X = {x} ; ::_thesis: (X \ {x,y}) . b1 = ([[0]] I) . b1 then A4: X . i = {(x . i)} by A2, Def1; thus (X \ {x,y}) . i = (X . i) \ ({x,y} . i) by A2, PBOOLE:def_6 .= (X . i) \ {(x . i),(y . i)} by A2, Def2 .= {} by A4, ZFMISC_1:66 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; suppose X = {y} ; ::_thesis: (X \ {x,y}) . b1 = ([[0]] I) . b1 then A5: X . i = {(y . i)} by A2, Def1; thus (X \ {x,y}) . i = (X . i) \ ({x,y} . i) by A2, PBOOLE:def_6 .= (X . i) \ {(x . i),(y . i)} by A2, Def2 .= {} by A5, ZFMISC_1:66 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; suppose X = {x,y} ; ::_thesis: (X \ {x,y}) . b1 = ([[0]] I) . b1 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_6 .= (X . i) \ {(x . i),(y . i)} by A2, Def2 .= {} by A6, ZFMISC_1:66 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; end; end; hence X \ {x,y} = [[0]] I by PBOOLE:3; ::_thesis: verum end; begin theorem :: PZFMISC1:57 for I being set for X, Y being ManySortedSet of I st ( X = [[0]] I or Y = [[0]] I ) holds [|X,Y|] = [[0]] I proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I st ( X = [[0]] I or Y = [[0]] I ) holds [|X,Y|] = [[0]] I let X, Y be ManySortedSet of I; ::_thesis: ( ( X = [[0]] I or Y = [[0]] I ) implies [|X,Y|] = [[0]] I ) assume A1: ( X = [[0]] I or Y = [[0]] I ) ; ::_thesis: [|X,Y|] = [[0]] I percases ( X = [[0]] I or Y = [[0]] I ) by A1; supposeA2: X = [[0]] I ; ::_thesis: [|X,Y|] = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|X,Y|]_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies [|X,Y|] . i = ([[0]] I) . i ) assume A3: i in I ; ::_thesis: [|X,Y|] . i = ([[0]] I) . i A4: X . i = {} by A2, PBOOLE:5; thus [|X,Y|] . i = [:(X . i),(Y . i):] by A3, PBOOLE:def_16 .= {} by A4, ZFMISC_1:90 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence [|X,Y|] = [[0]] I by PBOOLE:3; ::_thesis: verum end; supposeA5: Y = [[0]] I ; ::_thesis: [|X,Y|] = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|X,Y|]_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies [|X,Y|] . i = ([[0]] I) . i ) assume A6: i in I ; ::_thesis: [|X,Y|] . i = ([[0]] I) . i A7: Y . i = {} by A5, PBOOLE:5; thus [|X,Y|] . i = [:(X . i),(Y . i):] by A6, PBOOLE:def_16 .= {} by A7, ZFMISC_1:90 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence [|X,Y|] = [[0]] I by PBOOLE:3; ::_thesis: verum end; end; end; theorem :: PZFMISC1:58 for I being set for X, Y being ManySortedSet of I st X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] holds X = Y proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] holds X = Y let X, Y be ManySortedSet of I; ::_thesis: ( X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] implies X = Y ) assume that A1: X is V2() and A2: Y is V2() and A3: [|X,Y|] = [|Y,X|] ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A4: i in I ; ::_thesis: X . i = Y . i then A5: not X . i is empty by A1, PBOOLE:def_13; A6: not Y . i is empty by A2, A4, PBOOLE:def_13; [:(X . i),(Y . i):] = [|X,Y|] . i by A4, PBOOLE:def_16 .= [:(Y . i),(X . i):] by A3, A4, PBOOLE:def_16 ; hence X . i = Y . i by A5, A6, ZFMISC_1:91; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:59 for I being set for X, Y being ManySortedSet of I st [|X,X|] = [|Y,Y|] holds X = Y proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I st [|X,X|] = [|Y,Y|] holds X = Y let X, Y be ManySortedSet of I; ::_thesis: ( [|X,X|] = [|Y,Y|] implies X = Y ) assume A1: [|X,X|] = [|Y,Y|] ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A2: i in I ; ::_thesis: X . i = Y . i then [:(X . i),(X . i):] = [|X,X|] . i by PBOOLE:def_16 .= [:(Y . i),(Y . i):] by A1, A2, PBOOLE:def_16 ; hence X . i = Y . i by ZFMISC_1:92; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:60 for I being set for Z, X, Y being ManySortedSet of I st Z is V2() & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) holds X c= Y proof let I be set ; ::_thesis: for Z, X, Y being ManySortedSet of I st Z is V2() & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) holds X c= Y let Z, X, Y be ManySortedSet of I; ::_thesis: ( Z is V2() & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) implies X c= Y ) assume that A1: Z is V2() and A2: ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) ; ::_thesis: X c= Y percases ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) by A2; supposeA3: [|X,Z|] c= [|Y,Z|] ; ::_thesis: X c= Y let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= Y . i ) assume A4: i in I ; ::_thesis: X . i c= Y . i then A5: not Z . i is empty by A1, PBOOLE:def_13; [|X,Z|] . i c= [|Y,Z|] . i by A3, A4, PBOOLE:def_2; then [:(X . i),(Z . i):] c= [|Y,Z|] . i by A4, PBOOLE:def_16; then [:(X . i),(Z . i):] c= [:(Y . i),(Z . i):] by A4, PBOOLE:def_16; hence X . i c= Y . i by A5, ZFMISC_1:94; ::_thesis: verum end; supposeA6: [|Z,X|] c= [|Z,Y|] ; ::_thesis: X c= Y let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= Y . i ) assume A7: i in I ; ::_thesis: X . i c= Y . i then A8: not Z . i is empty by A1, PBOOLE:def_13; [|Z,X|] . i c= [|Z,Y|] . i by A6, A7, PBOOLE:def_2; then [:(Z . i),(X . i):] c= [|Z,Y|] . i by A7, PBOOLE:def_16; then [:(Z . i),(X . i):] c= [:(Z . i),(Y . i):] by A7, PBOOLE:def_16; hence X . i c= Y . i by A8, ZFMISC_1:94; ::_thesis: verum end; end; end; theorem :: PZFMISC1:61 for I being set for X, Y, Z being ManySortedSet of I st X c= Y holds ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y implies ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) ) assume A1: X c= Y ; ::_thesis: ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) thus [|X,Z|] c= [|Y,Z|] ::_thesis: [|Z,X|] c= [|Z,Y|] proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|X,Z|] . i c= [|Y,Z|] . i ) assume A2: i in I ; ::_thesis: [|X,Z|] . i c= [|Y,Z|] . i then X . i c= Y . i by A1, PBOOLE:def_2; then [:(X . i),(Z . i):] c= [:(Y . i),(Z . i):] by ZFMISC_1:95; then [|X,Z|] . i c= [:(Y . i),(Z . i):] by A2, PBOOLE:def_16; hence [|X,Z|] . i c= [|Y,Z|] . i by A2, PBOOLE:def_16; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|Z,X|] . i c= [|Z,Y|] . i ) assume A3: i in I ; ::_thesis: [|Z,X|] . i c= [|Z,Y|] . i then X . i c= Y . i by A1, PBOOLE:def_2; then [:(Z . i),(X . i):] c= [:(Z . i),(Y . i):] by ZFMISC_1:95; then [|Z,X|] . i c= [:(Z . i),(Y . i):] by A3, PBOOLE:def_16; hence [|Z,X|] . i c= [|Z,Y|] . i by A3, PBOOLE:def_16; ::_thesis: verum end; theorem :: PZFMISC1:62 for I being set for x1, A, x2, B being ManySortedSet of I st x1 c= A & x2 c= B holds [|x1,x2|] c= [|A,B|] proof let I be set ; ::_thesis: for x1, A, x2, B being ManySortedSet of I st x1 c= A & x2 c= B holds [|x1,x2|] c= [|A,B|] let x1, A, x2, B be ManySortedSet of I; ::_thesis: ( x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|] ) assume that A1: x1 c= A and A2: x2 c= B ; ::_thesis: [|x1,x2|] c= [|A,B|] let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|x1,x2|] . i c= [|A,B|] . i ) assume A3: i in I ; ::_thesis: [|x1,x2|] . i c= [|A,B|] . i then A4: x1 . i c= A . i by A1, PBOOLE:def_2; x2 . i c= B . i by A2, A3, PBOOLE:def_2; then [:(x1 . i),(x2 . i):] c= [:(A . i),(B . i):] by A4, ZFMISC_1:96; then [|x1,x2|] . i c= [:(A . i),(B . i):] by A3, PBOOLE:def_16; hence [|x1,x2|] . i c= [|A,B|] . i by A3, PBOOLE:def_16; ::_thesis: verum end; theorem :: PZFMISC1:63 for I being set for X, Y, Z being ManySortedSet of I holds ( [|(X \/ Y),Z|] = [|X,Z|] \/ [|Y,Z|] & [|Z,(X \/ Y)|] = [|Z,X|] \/ [|Z,Y|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds ( [|(X \/ Y),Z|] = [|X,Z|] \/ [|Y,Z|] & [|Z,(X \/ Y)|] = [|Z,X|] \/ [|Z,Y|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( [|(X \/ Y),Z|] = [|X,Z|] \/ [|Y,Z|] & [|Z,(X \/ Y)|] = [|Z,X|] \/ [|Z,Y|] ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|(X_\/_Y),Z|]_._i_=_([|X,Z|]_\/_[|Y,Z|])_._i let i be set ; ::_thesis: ( i in I implies [|(X \/ Y),Z|] . i = ([|X,Z|] \/ [|Y,Z|]) . i ) assume A1: i in I ; ::_thesis: [|(X \/ Y),Z|] . i = ([|X,Z|] \/ [|Y,Z|]) . i hence [|(X \/ Y),Z|] . i = [:((X \/ Y) . i),(Z . i):] by PBOOLE:def_16 .= [:((X . i) \/ (Y . i)),(Z . i):] by A1, PBOOLE:def_4 .= [:(X . i),(Z . i):] \/ [:(Y . i),(Z . i):] by ZFMISC_1:97 .= ([|X,Z|] . i) \/ [:(Y . i),(Z . i):] by A1, PBOOLE:def_16 .= ([|X,Z|] . i) \/ ([|Y,Z|] . i) by A1, PBOOLE:def_16 .= ([|X,Z|] \/ [|Y,Z|]) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence [|(X \/ Y),Z|] = [|X,Z|] \/ [|Y,Z|] by PBOOLE:3; ::_thesis: [|Z,(X \/ Y)|] = [|Z,X|] \/ [|Z,Y|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|Z,(X_\/_Y)|]_._i_=_([|Z,X|]_\/_[|Z,Y|])_._i let i be set ; ::_thesis: ( i in I implies [|Z,(X \/ Y)|] . i = ([|Z,X|] \/ [|Z,Y|]) . i ) assume A2: i in I ; ::_thesis: [|Z,(X \/ Y)|] . i = ([|Z,X|] \/ [|Z,Y|]) . i hence [|Z,(X \/ Y)|] . i = [:(Z . i),((X \/ Y) . i):] by PBOOLE:def_16 .= [:(Z . i),((X . i) \/ (Y . i)):] by A2, PBOOLE:def_4 .= [:(Z . i),(X . i):] \/ [:(Z . i),(Y . i):] by ZFMISC_1:97 .= ([|Z,X|] . i) \/ [:(Z . i),(Y . i):] by A2, PBOOLE:def_16 .= ([|Z,X|] . i) \/ ([|Z,Y|] . i) by A2, PBOOLE:def_16 .= ([|Z,X|] \/ [|Z,Y|]) . i by A2, PBOOLE:def_4 ; ::_thesis: verum end; hence [|Z,(X \/ Y)|] = [|Z,X|] \/ [|Z,Y|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:64 for I being set for x1, x2, A, B being ManySortedSet of I holds [|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|] proof let I be set ; ::_thesis: for x1, x2, A, B being ManySortedSet of I holds [|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|] let x1, x2, A, B be ManySortedSet of I; ::_thesis: [|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|(x1_\/_x2),(A_\/_B)|]_._i_=_((([|x1,A|]_\/_[|x1,B|])_\/_[|x2,A|])_\/_[|x2,B|])_._i let i be set ; ::_thesis: ( i in I implies [|(x1 \/ x2),(A \/ B)|] . i = ((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]) . i ) assume A1: i in I ; ::_thesis: [|(x1 \/ x2),(A \/ B)|] . i = ((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]) . i hence [|(x1 \/ x2),(A \/ B)|] . i = [:((x1 \/ x2) . i),((A \/ B) . i):] by PBOOLE:def_16 .= [:((x1 . i) \/ (x2 . i)),((A \/ B) . i):] by A1, PBOOLE:def_4 .= [:((x1 . i) \/ (x2 . i)),((A . i) \/ (B . i)):] by A1, PBOOLE:def_4 .= (([:(x1 . i),(A . i):] \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by ZFMISC_1:98 .= ((([|x1,A|] . i) \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def_16 .= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def_16 .= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def_16 .= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i) by A1, PBOOLE:def_16 .= ((([|x1,A|] \/ [|x1,B|]) . i) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i) by A1, PBOOLE:def_4 .= ((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) . i) \/ ([|x2,B|] . i) by A1, PBOOLE:def_4 .= ((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence [|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:65 for I being set for X, Y, Z being ManySortedSet of I holds ( [|(X /\ Y),Z|] = [|X,Z|] /\ [|Y,Z|] & [|Z,(X /\ Y)|] = [|Z,X|] /\ [|Z,Y|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds ( [|(X /\ Y),Z|] = [|X,Z|] /\ [|Y,Z|] & [|Z,(X /\ Y)|] = [|Z,X|] /\ [|Z,Y|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( [|(X /\ Y),Z|] = [|X,Z|] /\ [|Y,Z|] & [|Z,(X /\ Y)|] = [|Z,X|] /\ [|Z,Y|] ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|(X_/\_Y),Z|]_._i_=_([|X,Z|]_/\_[|Y,Z|])_._i let i be set ; ::_thesis: ( i in I implies [|(X /\ Y),Z|] . i = ([|X,Z|] /\ [|Y,Z|]) . i ) assume A1: i in I ; ::_thesis: [|(X /\ Y),Z|] . i = ([|X,Z|] /\ [|Y,Z|]) . i hence [|(X /\ Y),Z|] . i = [:((X /\ Y) . i),(Z . i):] by PBOOLE:def_16 .= [:((X . i) /\ (Y . i)),(Z . i):] by A1, PBOOLE:def_5 .= [:(X . i),(Z . i):] /\ [:(Y . i),(Z . i):] by ZFMISC_1:99 .= ([|X,Z|] . i) /\ [:(Y . i),(Z . i):] by A1, PBOOLE:def_16 .= ([|X,Z|] . i) /\ ([|Y,Z|] . i) by A1, PBOOLE:def_16 .= ([|X,Z|] /\ [|Y,Z|]) . i by A1, PBOOLE:def_5 ; ::_thesis: verum end; hence [|(X /\ Y),Z|] = [|X,Z|] /\ [|Y,Z|] by PBOOLE:3; ::_thesis: [|Z,(X /\ Y)|] = [|Z,X|] /\ [|Z,Y|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|Z,(X_/\_Y)|]_._i_=_([|Z,X|]_/\_[|Z,Y|])_._i let i be set ; ::_thesis: ( i in I implies [|Z,(X /\ Y)|] . i = ([|Z,X|] /\ [|Z,Y|]) . i ) assume A2: i in I ; ::_thesis: [|Z,(X /\ Y)|] . i = ([|Z,X|] /\ [|Z,Y|]) . i hence [|Z,(X /\ Y)|] . i = [:(Z . i),((X /\ Y) . i):] by PBOOLE:def_16 .= [:(Z . i),((X . i) /\ (Y . i)):] by A2, PBOOLE:def_5 .= [:(Z . i),(X . i):] /\ [:(Z . i),(Y . i):] by ZFMISC_1:99 .= ([|Z,X|] . i) /\ [:(Z . i),(Y . i):] by A2, PBOOLE:def_16 .= ([|Z,X|] . i) /\ ([|Z,Y|] . i) by A2, PBOOLE:def_16 .= ([|Z,X|] /\ [|Z,Y|]) . i by A2, PBOOLE:def_5 ; ::_thesis: verum end; hence [|Z,(X /\ Y)|] = [|Z,X|] /\ [|Z,Y|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:66 for I being set for x1, x2, A, B being ManySortedSet of I holds [|(x1 /\ x2),(A /\ B)|] = [|x1,A|] /\ [|x2,B|] proof let I be set ; ::_thesis: for x1, x2, A, B being ManySortedSet of I holds [|(x1 /\ x2),(A /\ B)|] = [|x1,A|] /\ [|x2,B|] let x1, x2, A, B be ManySortedSet of I; ::_thesis: [|(x1 /\ x2),(A /\ B)|] = [|x1,A|] /\ [|x2,B|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|(x1_/\_x2),(A_/\_B)|]_._i_=_([|x1,A|]_/\_[|x2,B|])_._i let i be set ; ::_thesis: ( i in I implies [|(x1 /\ x2),(A /\ B)|] . i = ([|x1,A|] /\ [|x2,B|]) . i ) assume A1: i in I ; ::_thesis: [|(x1 /\ x2),(A /\ B)|] . i = ([|x1,A|] /\ [|x2,B|]) . i hence [|(x1 /\ x2),(A /\ B)|] . i = [:((x1 /\ x2) . i),((A /\ B) . i):] by PBOOLE:def_16 .= [:((x1 . i) /\ (x2 . i)),((A /\ B) . i):] by A1, PBOOLE:def_5 .= [:((x1 . i) /\ (x2 . i)),((A . i) /\ (B . i)):] by A1, PBOOLE:def_5 .= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by ZFMISC_1:100 .= ([|x1,A|] . i) /\ [:(x2 . i),(B . i):] by A1, PBOOLE:def_16 .= ([|x1,A|] . i) /\ ([|x2,B|] . i) by A1, PBOOLE:def_16 .= ([|x1,A|] /\ [|x2,B|]) . i by A1, PBOOLE:def_5 ; ::_thesis: verum end; hence [|(x1 /\ x2),(A /\ B)|] = [|x1,A|] /\ [|x2,B|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:67 for I being set for A, X, B, Y being ManySortedSet of I st A c= X & B c= Y holds [|A,Y|] /\ [|X,B|] = [|A,B|] proof let I be set ; ::_thesis: for A, X, B, Y being ManySortedSet of I st A c= X & B c= Y holds [|A,Y|] /\ [|X,B|] = [|A,B|] let A, X, B, Y be ManySortedSet of I; ::_thesis: ( A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|] ) assume that A1: A c= X and A2: B c= Y ; ::_thesis: [|A,Y|] /\ [|X,B|] = [|A,B|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ([|A,Y|]_/\_[|X,B|])_._i_=_[|A,B|]_._i let i be set ; ::_thesis: ( i in I implies ([|A,Y|] /\ [|X,B|]) . i = [|A,B|] . i ) assume A3: i in I ; ::_thesis: ([|A,Y|] /\ [|X,B|]) . i = [|A,B|] . i then A4: A . i c= X . i by A1, PBOOLE:def_2; A5: B . i c= Y . i by A2, A3, PBOOLE:def_2; thus ([|A,Y|] /\ [|X,B|]) . i = ([|A,Y|] . i) /\ ([|X,B|] . i) by A3, PBOOLE:def_5 .= [:(A . i),(Y . i):] /\ ([|X,B|] . i) by A3, PBOOLE:def_16 .= [:(A . i),(Y . i):] /\ [:(X . i),(B . i):] by A3, PBOOLE:def_16 .= [:(A . i),(B . i):] by A4, A5, ZFMISC_1:101 .= [|A,B|] . i by A3, PBOOLE:def_16 ; ::_thesis: verum end; hence [|A,Y|] /\ [|X,B|] = [|A,B|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:68 for I being set for X, Y, Z being ManySortedSet of I holds ( [|(X \ Y),Z|] = [|X,Z|] \ [|Y,Z|] & [|Z,(X \ Y)|] = [|Z,X|] \ [|Z,Y|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds ( [|(X \ Y),Z|] = [|X,Z|] \ [|Y,Z|] & [|Z,(X \ Y)|] = [|Z,X|] \ [|Z,Y|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( [|(X \ Y),Z|] = [|X,Z|] \ [|Y,Z|] & [|Z,(X \ Y)|] = [|Z,X|] \ [|Z,Y|] ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|(X_\_Y),Z|]_._i_=_([|X,Z|]_\_[|Y,Z|])_._i let i be set ; ::_thesis: ( i in I implies [|(X \ Y),Z|] . i = ([|X,Z|] \ [|Y,Z|]) . i ) assume A1: i in I ; ::_thesis: [|(X \ Y),Z|] . i = ([|X,Z|] \ [|Y,Z|]) . i hence [|(X \ Y),Z|] . i = [:((X \ Y) . i),(Z . i):] by PBOOLE:def_16 .= [:((X . i) \ (Y . i)),(Z . i):] by A1, PBOOLE:def_6 .= [:(X . i),(Z . i):] \ [:(Y . i),(Z . i):] by ZFMISC_1:102 .= ([|X,Z|] . i) \ [:(Y . i),(Z . i):] by A1, PBOOLE:def_16 .= ([|X,Z|] . i) \ ([|Y,Z|] . i) by A1, PBOOLE:def_16 .= ([|X,Z|] \ [|Y,Z|]) . i by A1, PBOOLE:def_6 ; ::_thesis: verum end; hence [|(X \ Y),Z|] = [|X,Z|] \ [|Y,Z|] by PBOOLE:3; ::_thesis: [|Z,(X \ Y)|] = [|Z,X|] \ [|Z,Y|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|Z,(X_\_Y)|]_._i_=_([|Z,X|]_\_[|Z,Y|])_._i let i be set ; ::_thesis: ( i in I implies [|Z,(X \ Y)|] . i = ([|Z,X|] \ [|Z,Y|]) . i ) assume A2: i in I ; ::_thesis: [|Z,(X \ Y)|] . i = ([|Z,X|] \ [|Z,Y|]) . i hence [|Z,(X \ Y)|] . i = [:(Z . i),((X \ Y) . i):] by PBOOLE:def_16 .= [:(Z . i),((X . i) \ (Y . i)):] by A2, PBOOLE:def_6 .= [:(Z . i),(X . i):] \ [:(Z . i),(Y . i):] by ZFMISC_1:102 .= ([|Z,X|] . i) \ [:(Z . i),(Y . i):] by A2, PBOOLE:def_16 .= ([|Z,X|] . i) \ ([|Z,Y|] . i) by A2, PBOOLE:def_16 .= ([|Z,X|] \ [|Z,Y|]) . i by A2, PBOOLE:def_6 ; ::_thesis: verum end; hence [|Z,(X \ Y)|] = [|Z,X|] \ [|Z,Y|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:69 for I being set for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] \ [|A,B|] = [|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|] proof let I be set ; ::_thesis: for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] \ [|A,B|] = [|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|] let x1, x2, A, B be ManySortedSet of I; ::_thesis: [|x1,x2|] \ [|A,B|] = [|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ([|x1,x2|]_\_[|A,B|])_._i_=_([|(x1_\_A),x2|]_\/_[|x1,(x2_\_B)|])_._i let i be set ; ::_thesis: ( i in I implies ([|x1,x2|] \ [|A,B|]) . i = ([|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|]) . i ) assume A1: i in I ; ::_thesis: ([|x1,x2|] \ [|A,B|]) . i = ([|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|]) . i hence ([|x1,x2|] \ [|A,B|]) . i = ([|x1,x2|] . i) \ ([|A,B|] . i) by PBOOLE:def_6 .= [:(x1 . i),(x2 . i):] \ ([|A,B|] . i) by A1, PBOOLE:def_16 .= [:(x1 . i),(x2 . i):] \ [:(A . i),(B . i):] by A1, PBOOLE:def_16 .= [:((x1 . i) \ (A . i)),(x2 . i):] \/ [:(x1 . i),((x2 . i) \ (B . i)):] by ZFMISC_1:103 .= [:((x1 \ A) . i),(x2 . i):] \/ [:(x1 . i),((x2 . i) \ (B . i)):] by A1, PBOOLE:def_6 .= [:((x1 \ A) . i),(x2 . i):] \/ [:(x1 . i),((x2 \ B) . i):] by A1, PBOOLE:def_6 .= ([|(x1 \ A),x2|] . i) \/ [:(x1 . i),((x2 \ B) . i):] by A1, PBOOLE:def_16 .= ([|(x1 \ A),x2|] . i) \/ ([|x1,(x2 \ B)|] . i) by A1, PBOOLE:def_16 .= ([|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|]) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence [|x1,x2|] \ [|A,B|] = [|(x1 \ A),x2|] \/ [|x1,(x2 \ B)|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:70 for I being set for x1, x2, A, B being ManySortedSet of I st ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) holds [|x1,A|] /\ [|x2,B|] = [[0]] I proof let I be set ; ::_thesis: for x1, x2, A, B being ManySortedSet of I st ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) holds [|x1,A|] /\ [|x2,B|] = [[0]] I let x1, x2, A, B be ManySortedSet of I; ::_thesis: ( ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) implies [|x1,A|] /\ [|x2,B|] = [[0]] I ) assume A1: ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) ; ::_thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I percases ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) by A1; supposeA2: x1 /\ x2 = [[0]] I ; ::_thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ([|x1,A|]_/\_[|x2,B|])_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i ) assume A3: i in I ; ::_thesis: ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i then (x1 . i) /\ (x2 . i) = (x1 /\ x2) . i by PBOOLE:def_5 .= {} by A2, 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:104; thus ([|x1,A|] /\ [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A3, PBOOLE:def_5 .= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A3, PBOOLE:def_16 .= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A3, PBOOLE:def_16 .= {} by A4, XBOOLE_0:def_7 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence [|x1,A|] /\ [|x2,B|] = [[0]] I by PBOOLE:3; ::_thesis: verum end; supposeA5: A /\ B = [[0]] I ; ::_thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ([|x1,A|]_/\_[|x2,B|])_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i ) assume A6: i in I ; ::_thesis: ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i then (A . i) /\ (B . i) = (A /\ B) . i by PBOOLE:def_5 .= {} by A5, 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:104; thus ([|x1,A|] /\ [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A6, PBOOLE:def_5 .= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A6, PBOOLE:def_16 .= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A6, PBOOLE:def_16 .= {} by A7, XBOOLE_0:def_7 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence [|x1,A|] /\ [|x2,B|] = [[0]] I by PBOOLE:3; ::_thesis: verum end; end; end; theorem :: PZFMISC1:71 for I being set for X, x being ManySortedSet of I st X is V2() holds ( [|{x},X|] is V2() & [|X,{x}|] is V2() ) proof let I be set ; ::_thesis: for X, x being ManySortedSet of I st X is V2() holds ( [|{x},X|] is V2() & [|X,{x}|] is V2() ) let X, x be ManySortedSet of I; ::_thesis: ( X is V2() implies ( [|{x},X|] is V2() & [|X,{x}|] is V2() ) ) assume A1: X is V2() ; ::_thesis: ( [|{x},X|] is V2() & [|X,{x}|] is V2() ) thus [|{x},X|] is V2() ::_thesis: [|X,{x}|] is V2() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not [|{x},X|] . i is empty ) assume A2: i in I ; ::_thesis: not [|{x},X|] . i is empty then not X . i is empty by A1, PBOOLE:def_13; then not [:{(x . i)},(X . i):] is empty by ZFMISC_1:107; then not [:({x} . i),(X . i):] is empty by A2, Def1; hence not [|{x},X|] . i is empty by A2, PBOOLE:def_16; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not [|X,{x}|] . i is empty ) assume A3: i in I ; ::_thesis: not [|X,{x}|] . i is empty then not X . i is empty by A1, PBOOLE:def_13; then not [:(X . i),{(x . i)}:] is empty by ZFMISC_1:107; then not [:(X . i),({x} . i):] is empty by A3, Def1; hence not [|X,{x}|] . i is empty by A3, PBOOLE:def_16; ::_thesis: verum end; theorem :: PZFMISC1:72 for I being set for x, y, X being ManySortedSet of I holds ( [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] ) proof let I be set ; ::_thesis: for x, y, X being ManySortedSet of I holds ( [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] ) let x, y, X be ManySortedSet of I; ::_thesis: ( [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|{x,y},X|]_._i_=_([|{x},X|]_\/_[|{y},X|])_._i let i be set ; ::_thesis: ( i in I implies [|{x,y},X|] . i = ([|{x},X|] \/ [|{y},X|]) . i ) assume A1: i in I ; ::_thesis: [|{x,y},X|] . i = ([|{x},X|] \/ [|{y},X|]) . i hence [|{x,y},X|] . i = [:({x,y} . i),(X . i):] by PBOOLE:def_16 .= [:{(x . i),(y . i)},(X . i):] by A1, Def2 .= [:{(x . i)},(X . i):] \/ [:{(y . i)},(X . i):] by ZFMISC_1:109 .= [:({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, PBOOLE:def_16 .= ([|{x},X|] . i) \/ ([|{y},X|] . i) by A1, PBOOLE:def_16 .= ([|{x},X|] \/ [|{y},X|]) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence [|{x,y},X|] = [|{x},X|] \/ [|{y},X|] by PBOOLE:3; ::_thesis: [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] now__::_thesis:_for_i_being_set_st_i_in_I_holds_ [|X,{x,y}|]_._i_=_([|X,{x}|]_\/_[|X,{y}|])_._i let i be set ; ::_thesis: ( i in I implies [|X,{x,y}|] . i = ([|X,{x}|] \/ [|X,{y}|]) . i ) assume A2: i in I ; ::_thesis: [|X,{x,y}|] . i = ([|X,{x}|] \/ [|X,{y}|]) . i hence [|X,{x,y}|] . i = [:(X . i),({x,y} . i):] by PBOOLE:def_16 .= [:(X . i),{(x . i),(y . i)}:] by A2, Def2 .= [:(X . i),{(x . i)}:] \/ [:(X . i),{(y . i)}:] by ZFMISC_1:109 .= [:(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, PBOOLE:def_16 .= ([|X,{x}|] . i) \/ ([|X,{y}|] . i) by A2, PBOOLE:def_16 .= ([|X,{x}|] \/ [|X,{y}|]) . i by A2, PBOOLE:def_4 ; ::_thesis: verum end; hence [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:73 for I being set for x1, A, x2, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds ( x1 = x2 & A = B ) proof let I be set ; ::_thesis: for x1, A, x2, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds ( x1 = x2 & A = B ) let x1, A, x2, B be ManySortedSet of I; ::_thesis: ( x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] implies ( x1 = x2 & A = B ) ) assume that A1: x1 is V2() and A2: A is V2() and A3: [|x1,A|] = [|x2,B|] ; ::_thesis: ( x1 = x2 & A = B ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x1_._i_=_x2_._i let i be set ; ::_thesis: ( i in I implies x1 . i = x2 . i ) assume A4: i in I ; ::_thesis: x1 . i = x2 . i then A5: not x1 . i is empty by A1, PBOOLE:def_13; A6: not A . i is empty by A2, A4, PBOOLE:def_13; [:(x1 . i),(A . i):] = [|x1,A|] . i by A4, PBOOLE:def_16 .= [:(x2 . i),(B . i):] by A3, A4, PBOOLE:def_16 ; hence x1 . i = x2 . i by A5, A6, ZFMISC_1:110; ::_thesis: verum end; hence x1 = x2 by PBOOLE:3; ::_thesis: A = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ A_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies A . i = B . i ) assume A7: i in I ; ::_thesis: A . i = B . i then A8: not x1 . i is empty by A1, PBOOLE:def_13; A9: not A . i is empty by A2, A7, PBOOLE:def_13; [:(x1 . i),(A . i):] = [|x1,A|] . i by A7, PBOOLE:def_16 .= [:(x2 . i),(B . i):] by A3, A7, PBOOLE:def_16 ; hence A . i = B . i by A8, A9, ZFMISC_1:110; ::_thesis: verum end; hence A = B by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:74 for I being set for X, Y being ManySortedSet of I st ( X c= [|X,Y|] or X c= [|Y,X|] ) holds X = [[0]] I proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I st ( X c= [|X,Y|] or X c= [|Y,X|] ) holds X = [[0]] I let X, Y be ManySortedSet of I; ::_thesis: ( ( X c= [|X,Y|] or X c= [|Y,X|] ) implies X = [[0]] I ) assume A1: ( X c= [|X,Y|] or X c= [|Y,X|] ) ; ::_thesis: X = [[0]] I percases ( X c= [|X,Y|] or X c= [|Y,X|] ) by A1; supposeA2: X c= [|X,Y|] ; ::_thesis: X = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies X . i = ([[0]] I) . i ) assume A3: i in I ; ::_thesis: X . i = ([[0]] I) . i then X . i c= [|X,Y|] . i by A2, PBOOLE:def_2; then X . i c= [:(X . i),(Y . i):] by A3, PBOOLE:def_16; hence X . i = {} by ZFMISC_1:111 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence X = [[0]] I by PBOOLE:3; ::_thesis: verum end; supposeA4: X c= [|Y,X|] ; ::_thesis: X = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies X . i = ([[0]] I) . i ) assume A5: i in I ; ::_thesis: X . i = ([[0]] I) . i then X . i c= [|Y,X|] . i by A4, PBOOLE:def_2; then X . i c= [:(Y . i),(X . i):] by A5, PBOOLE:def_16; hence X . i = {} by ZFMISC_1:111 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence X = [[0]] I by PBOOLE:3; ::_thesis: verum end; end; end; theorem :: PZFMISC1:75 for I being set for A, x, y, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds A in [|(x /\ X),(y /\ Y)|] proof let I be set ; ::_thesis: for A, x, y, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds A in [|(x /\ X),(y /\ Y)|] let A, x, y, X, Y be ManySortedSet of I; ::_thesis: ( A in [|x,y|] & A in [|X,Y|] implies A in [|(x /\ X),(y /\ Y)|] ) assume that A1: A in [|x,y|] and A2: A in [|X,Y|] ; ::_thesis: A in [|(x /\ X),(y /\ Y)|] let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in [|(x /\ X),(y /\ Y)|] . i ) assume A3: i in I ; ::_thesis: A . i in [|(x /\ X),(y /\ Y)|] . i then A4: A . i in [|x,y|] . i by A1, PBOOLE:def_1; A5: A . i in [|X,Y|] . i by A2, A3, PBOOLE:def_1; A6: A . i in [:(x . i),(y . i):] by A3, A4, PBOOLE:def_16; A . i in [:(X . i),(Y . i):] by A3, A5, PBOOLE:def_16; then A . i in [:((x . i) /\ (X . i)),((y . i) /\ (Y . i)):] by A6, ZFMISC_1:113; then A . i in [:((x /\ X) . i),((y . i) /\ (Y . i)):] by A3, PBOOLE:def_5; then A . i in [:((x /\ X) . i),((y /\ Y) . i):] by A3, PBOOLE:def_5; hence A . i in [|(x /\ X),(y /\ Y)|] . i by A3, PBOOLE:def_16; ::_thesis: verum end; theorem :: PZFMISC1:76 for I being set for x, X, y, Y being ManySortedSet of I st [|x,X|] c= [|y,Y|] & [|x,X|] is V2() holds ( x c= y & X c= Y ) proof let I be set ; ::_thesis: for x, X, y, Y being ManySortedSet of I st [|x,X|] c= [|y,Y|] & [|x,X|] is V2() holds ( x c= y & X c= Y ) let x, X, y, Y be ManySortedSet of I; ::_thesis: ( [|x,X|] c= [|y,Y|] & [|x,X|] is V2() implies ( x c= y & X c= Y ) ) assume that A1: [|x,X|] c= [|y,Y|] and A2: [|x,X|] is V2() ; ::_thesis: ( x c= y & X c= Y ) thus x c= y ::_thesis: X c= Y proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or x . i c= y . i ) assume A3: i in I ; ::_thesis: x . i c= y . i then [|x,X|] . i c= [|y,Y|] . i by A1, PBOOLE:def_2; then [:(x . i),(X . i):] c= [|y,Y|] . i by A3, PBOOLE:def_16; then A4: [:(x . i),(X . i):] c= [:(y . i),(Y . i):] by A3, PBOOLE:def_16; not [|x,X|] . i is empty by A2, A3, PBOOLE:def_13; then not [:(x . i),(X . i):] is empty by A3, PBOOLE:def_16; hence x . i c= y . i by A4, ZFMISC_1:114; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= Y . i ) assume A5: i in I ; ::_thesis: X . i c= Y . i then [|x,X|] . i c= [|y,Y|] . i by A1, PBOOLE:def_2; then [:(x . i),(X . i):] c= [|y,Y|] . i by A5, PBOOLE:def_16; then A6: [:(x . i),(X . i):] c= [:(y . i),(Y . i):] by A5, PBOOLE:def_16; not [|x,X|] . i is empty by A2, A5, PBOOLE:def_13; then not [:(x . i),(X . i):] is empty by A5, PBOOLE:def_16; hence X . i c= Y . i by A6, ZFMISC_1:114; ::_thesis: verum end; theorem :: PZFMISC1:77 for I being set for A, X being ManySortedSet of I st A c= X holds [|A,A|] c= [|X,X|] proof let I be set ; ::_thesis: for A, X being ManySortedSet of I st A c= X holds [|A,A|] c= [|X,X|] let A, X be ManySortedSet of I; ::_thesis: ( A c= X implies [|A,A|] c= [|X,X|] ) assume A1: A c= X ; ::_thesis: [|A,A|] c= [|X,X|] let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|A,A|] . i c= [|X,X|] . i ) assume A2: i in I ; ::_thesis: [|A,A|] . i c= [|X,X|] . i then A . i c= X . i by A1, PBOOLE:def_2; then [:(A . i),(A . i):] c= [:(X . i),(X . i):] by ZFMISC_1:96; then [|A,A|] . i c= [:(X . i),(X . i):] by A2, PBOOLE:def_16; hence [|A,A|] . i c= [|X,X|] . i by A2, PBOOLE:def_16; ::_thesis: verum end; theorem :: PZFMISC1:78 for I being set for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds [|X,Y|] /\ [|Y,X|] = [[0]] I proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds [|X,Y|] /\ [|Y,X|] = [[0]] I let X, Y be ManySortedSet of I; ::_thesis: ( X /\ Y = [[0]] I implies [|X,Y|] /\ [|Y,X|] = [[0]] I ) assume A1: X /\ Y = [[0]] I ; ::_thesis: [|X,Y|] /\ [|Y,X|] = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ([|X,Y|]_/\_[|Y,X|])_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ([|X,Y|] /\ [|Y,X|]) . i = ([[0]] I) . i ) assume A2: i in I ; ::_thesis: ([|X,Y|] /\ [|Y,X|]) . i = ([[0]] I) . i then (X . i) /\ (Y . i) = (X /\ Y) . i by PBOOLE:def_5 .= {} by A1, 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:104; thus ([|X,Y|] /\ [|Y,X|]) . i = ([|X,Y|] . i) /\ ([|Y,X|] . i) by A2, PBOOLE:def_5 .= [:(X . i),(Y . i):] /\ ([|Y,X|] . i) by A2, PBOOLE:def_16 .= [:(X . i),(Y . i):] /\ [:(Y . i),(X . i):] by A2, PBOOLE:def_16 .= {} by A3, XBOOLE_0:def_7 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence [|X,Y|] /\ [|Y,X|] = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: PZFMISC1:79 for I being set for A, B, X, Y being ManySortedSet of I st A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds B c= Y proof let I be set ; ::_thesis: for A, B, X, Y being ManySortedSet of I st A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds B c= Y let A, B, X, Y be ManySortedSet of I; ::_thesis: ( A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) implies B c= Y ) assume that A1: A is V2() and A2: ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) ; ::_thesis: B c= Y percases ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) by A2; supposeA3: [|A,B|] c= [|X,Y|] ; ::_thesis: B c= Y let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or B . i c= Y . i ) assume A4: i in I ; ::_thesis: B . i c= Y . i then [|A,B|] . i c= [|X,Y|] . i by A3, PBOOLE:def_2; then [:(A . i),(B . i):] c= [|X,Y|] . i by A4, PBOOLE:def_16; then A5: [:(A . i),(B . i):] c= [:(X . i),(Y . i):] by A4, PBOOLE:def_16; not A . i is empty by A1, A4, PBOOLE:def_13; hence B . i c= Y . i by A5, ZFMISC_1:115; ::_thesis: verum end; supposeA6: [|B,A|] c= [|Y,X|] ; ::_thesis: B c= Y let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or B . i c= Y . i ) assume A7: i in I ; ::_thesis: B . i c= Y . i then [|B,A|] . i c= [|Y,X|] . i by A6, PBOOLE:def_2; then [:(B . i),(A . i):] c= [|Y,X|] . i by A7, PBOOLE:def_16; then A8: [:(B . i),(A . i):] c= [:(Y . i),(X . i):] by A7, PBOOLE:def_16; not A . i is empty by A1, A7, PBOOLE:def_13; hence B . i c= Y . i by A8, ZFMISC_1:115; ::_thesis: verum end; end; end; theorem :: PZFMISC1:80 for I being set for x, A, B, y, X, Y being ManySortedSet of I st x c= [|A,B|] & y c= [|X,Y|] holds x \/ y c= [|(A \/ X),(B \/ Y)|] proof let I be set ; ::_thesis: for x, A, B, y, X, Y being ManySortedSet of I st x c= [|A,B|] & y c= [|X,Y|] holds x \/ y c= [|(A \/ X),(B \/ Y)|] let x, A, B, y, X, Y be ManySortedSet of I; ::_thesis: ( x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|(A \/ X),(B \/ Y)|] ) assume that A1: x c= [|A,B|] and A2: y c= [|X,Y|] ; ::_thesis: x \/ y c= [|(A \/ X),(B \/ Y)|] let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i ) assume A3: i in I ; ::_thesis: (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i then A4: x . i c= [|A,B|] . i by A1, PBOOLE:def_2; A5: y . i c= [|X,Y|] . i by A2, A3, PBOOLE:def_2; A6: x . i c= [:(A . i),(B . i):] by A3, A4, PBOOLE:def_16; y . i c= [:(X . i),(Y . i):] by A3, A5, PBOOLE:def_16; then (x . i) \/ (y . i) c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A6, ZFMISC_1:119; then (x \/ y) . i c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A3, PBOOLE:def_4; then (x \/ y) . i c= [:((A \/ X) . i),((B . i) \/ (Y . i)):] by A3, PBOOLE:def_4; then (x \/ y) . i c= [:((A \/ X) . i),((B \/ Y) . i):] by A3, PBOOLE:def_4; hence (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i by A3, PBOOLE:def_16; ::_thesis: verum end; begin definition let I be set ; let A, B be ManySortedSet of I; predA is_transformable_to B means :: PZFMISC1:def 3 for i being set st i in I & B . i = {} holds A . i = {} ; reflexivity for A being ManySortedSet of I for i being set st i in I & A . i = {} holds A . i = {} ; end; :: deftheorem defines is_transformable_to PZFMISC1:def_3_:_ for I being set for A, B being ManySortedSet of I holds ( A is_transformable_to B iff for i being set st i in I & B . i = {} holds A . i = {} );