:: 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 = {} );