:: PZFMISC1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: PZFMISC1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, i, X being set
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
proof end;

theorem :: PZFMISC1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st f = {} holds
f is ManySortedSet of {} by PBOOLE:def 3, RELAT_1:60;

theorem :: PZFMISC1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set st not I is empty holds
for X being ManySortedSet of I holds
( not X is empty-yielding or not X is non-empty )
proof end;

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 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 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} -> V3 locally-finite ;
coherence
( {A} is non-empty & {A} is locally-finite )
proof 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 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 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} -> V3 locally-finite ;
coherence
( {A,B} is non-empty & {A,B} is locally-finite )
proof end;
end;

theorem :: PZFMISC1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PZFMISC1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, A being ManySortedSet of I st x in {A} holds
x = A
proof end;

theorem :: PZFMISC1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x being ManySortedSet of I holds x in {x}
proof end;

theorem :: PZFMISC1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, A, B being ManySortedSet of I st ( x = A or x = B ) holds
x in {A,B}
proof end;

theorem :: PZFMISC1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds {A} \/ {B} = {A,B}
proof end;

theorem :: PZFMISC1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x being ManySortedSet of I holds {x,x} = {x}
proof end;

theorem :: PZFMISC1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PZFMISC1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st {A} c= {B} holds
A = B
proof end;

theorem :: PZFMISC1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st {x} = {y} holds
x = y
proof end;

theorem :: PZFMISC1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, A, B being ManySortedSet of I st {x} = {A,B} holds
( x = A & x = B )
proof end;

theorem :: PZFMISC1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, A, B being ManySortedSet of I st {x} = {A,B} holds
A = B
proof end;

theorem :: PZFMISC1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I holds
( {x} c= {x,y} & {y} c= {x,y} )
proof end;

theorem :: PZFMISC1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st ( {x} \/ {y} = {x} or {x} \/ {y} = {y} ) holds
x = y
proof end;

theorem :: PZFMISC1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I holds {x} \/ {x,y} = {x,y}
proof end;

theorem :: PZFMISC1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PZFMISC1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st not I is empty & {x} /\ {y} = [0] I holds
x <> y
proof end;

theorem :: PZFMISC1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) holds
x = y
proof end;

theorem :: PZFMISC1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I holds
( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} )
proof end;

theorem :: PZFMISC1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st not I is empty & {x} \ {y} = {x} holds
x <> y
proof end;

theorem :: PZFMISC1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st {x} \ {y} = [0] I holds
x = y
proof end;

theorem :: PZFMISC1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I holds
( {x} \ {x,y} = [0] I & {y} \ {x,y} = [0] I )
proof end;

theorem :: PZFMISC1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I st {x} c= {y} holds
{x} = {y}
proof end;

theorem :: PZFMISC1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y, A being ManySortedSet of I st {x,y} c= {A} holds
( x = A & y = A )
proof end;

theorem :: PZFMISC1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y, A being ManySortedSet of I st {x,y} c= {A} holds
{x,y} = {A}
proof end;

theorem :: PZFMISC1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x being ManySortedSet of I holds bool {x} = {([0] I),{x}}
proof end;

theorem :: PZFMISC1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds {A} c= bool A
proof end;

theorem :: PZFMISC1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x being ManySortedSet of I holds union {x} = x
proof end;

theorem :: PZFMISC1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y being ManySortedSet of I holds union {{x},{y}} = {x,y}
proof end;

theorem :: PZFMISC1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds union {A,B} = A \/ B
proof end;

theorem :: PZFMISC1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I holds
( {x} c= X iff x in X )
proof end;

theorem :: PZFMISC1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I st {x} \/ X = X holds
x in X
proof end;

theorem :: PZFMISC1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I st x in X holds
{x} \/ X = X
proof end;

theorem :: PZFMISC1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I st not I is empty holds
{x} \/ X <> [0] I
proof end;

theorem :: PZFMISC1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, y, X being ManySortedSet of I st not I is empty holds
{x,y} \/ X <> [0] I
proof end;

theorem :: PZFMISC1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, x being ManySortedSet of I st X /\ {x} = {x} holds
x in X
proof end;

theorem :: PZFMISC1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I st x in X holds
X /\ {x} = {x}
proof end;

theorem :: PZFMISC1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for y, X, x being ManySortedSet of I st y in X \ {x} holds
y in X
proof end;

theorem :: PZFMISC1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X being ManySortedSet of I holds
( {x} \ X = [0] I iff x in X )
proof end;

theorem :: PZFMISC1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PZFMISC1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] holds
X = Y
proof end;

theorem :: PZFMISC1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st [|X,X|] = [|Y,Y|] holds
X = Y
proof end;

theorem :: PZFMISC1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Z, X, Y being ManySortedSet of I st Z is non-empty & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) holds
X c= Y
proof end;

theorem :: PZFMISC1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x1, x2, A, B being ManySortedSet of I holds [|(x1 /\ x2),(A /\ B)|] = [|x1,A|] /\ [|x2,B|]
proof end;

theorem :: PZFMISC1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, x being ManySortedSet of I st X is non-empty holds
( [|{x},X|] is non-empty & [|X,{x}|] is non-empty )
proof end;

theorem :: PZFMISC1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x1, A, x2, B being ManySortedSet of I st x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|] holds
( x1 = x2 & A = B )
proof end;

theorem :: PZFMISC1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PZFMISC1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, y, Y being ManySortedSet of I st [|x,X|] c= [|y,Y|] & [|x,X|] is non-empty holds
( x c= y & X c= Y )
proof end;

theorem :: PZFMISC1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, X being ManySortedSet of I st A c= X holds
[|A,A|] c= [|X,X|]
proof end;

theorem :: PZFMISC1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X /\ Y = [0] I holds
[|X,Y|] /\ [|Y,X|] = [0] I
proof end;

theorem :: PZFMISC1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B, X, Y being ManySortedSet of I st A is non-empty & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds
B c= Y
proof end;

theorem :: PZFMISC1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let I be set ;
let A, B be ManySortedSet of I;
pred A 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 = {} );