:: MCART_2 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for X1, X2 being set st X1 <> {} & X2 <> {} holds
for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
Lm2:
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
Lm3:
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]
theorem :: MCART_2:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y holds
Y1 misses X ) )
theorem Th2: :: MCART_2:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5 be
set ;
func [x1,x2,x3,x4,x5] -> set equals :: MCART_2:def 1
[[x1,x2,x3,x4],x5];
correctness
coherence
[[x1,x2,x3,x4],x5] is set ;
;
end;
:: deftheorem defines [ MCART_2:def 1 :
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5];
theorem Th3: :: MCART_2:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5]
theorem :: MCART_2:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: MCART_2:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5]
theorem Th6: :: MCART_2:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5]
theorem Th7: :: MCART_2:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5,
y1,
y2,
y3,
y4,
y5 being
set st
[x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 )
theorem Th8: :: MCART_2:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X being
set st
X <> {} holds
ex
x being
set st
(
x in X & ( for
x1,
x2,
x3,
x4,
x5 being
set holds
( ( not
x1 in X & not
x2 in X ) or not
x = [x1,x2,x3,x4,x5] ) ) )
definition
let X1,
X2,
X3,
X4,
X5 be
set ;
func [:X1,X2,X3,X4,X5:] -> set equals :: MCART_2:def 2
[:[:X1,X2,X3,X4:],X5:];
correctness
coherence
[:[:X1,X2,X3,X4:],X5:] is set ;
;
end;
:: deftheorem defines [: MCART_2:def 2 :
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:];
theorem Th9: :: MCART_2:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:]
theorem :: MCART_2:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: MCART_2:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:]
theorem Th12: :: MCART_2:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:]
theorem Th13: :: MCART_2:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: MCART_2:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
[:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 )
theorem :: MCART_2:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
[:X1,X2,X3,X4,X5:] <> {} &
[:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 )
theorem :: MCART_2:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th17: :: MCART_2:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5]
definition
let X1,
X2,
X3,
X4,
X5 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5:];
func x `1 -> Element of
X1 means :
Def3:
:: MCART_2:def 3
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def4:
:: MCART_2:def 4
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def5:
:: MCART_2:def 5
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def6:
:: MCART_2:def 6
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def7:
:: MCART_2:def 7
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x5 ) holds
b1 = b2
end;
:: deftheorem Def3 defines `1 MCART_2:def 3 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X1 holds
(
b7 = x `1 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x1 );
:: deftheorem Def4 defines `2 MCART_2:def 4 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X2 holds
(
b7 = x `2 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x2 );
:: deftheorem Def5 defines `3 MCART_2:def 5 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X3 holds
(
b7 = x `3 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x3 );
:: deftheorem Def6 defines `4 MCART_2:def 6 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X4 holds
(
b7 = x `4 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x4 );
:: deftheorem Def7 defines `5 MCART_2:def 7 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X5 holds
(
b7 = x `5 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x5 );
theorem :: MCART_2:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 )
by Def3, Def4, Def5, Def6, Def7;
theorem Th19: :: MCART_2:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )]
theorem Th20: :: MCART_2:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: MCART_2:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set st (
X1 c= [:X1,X2,X3,X4,X5:] or
X1 c= [:X2,X3,X4,X5,X1:] or
X1 c= [:X3,X4,X5,X1,X2:] or
X1 c= [:X4,X5,X1,X2,X3:] or
X1 c= [:X5,X1,X2,X3,X4:] ) holds
X1 = {}
theorem :: MCART_2:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
[:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 )
theorem :: MCART_2:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5 being
set holds
[:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}
theorem :: MCART_2:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 )
by Def3, Def4, Def5, Def6, Def7;
theorem :: MCART_2:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
y1 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
y2 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
y3 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
y4 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
y5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y5 = xx5 ) holds
y5 = x `5
theorem :: MCART_2:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
y,
X1,
X2,
X3,
X4,
X5 being
set st
y in [:X1,X2,X3,X4,X5:] holds
ex
x1,
x2,
x3,
x4,
x5 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
y = [x1,x2,x3,x4,x5] )
theorem :: MCART_2:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
x1,
x2,
x3,
x4,
x5,
X1,
X2,
X3,
X4,
X5 being
set holds
(
[x1,x2,x3,x4,x5] in [:X1,X2,X3,X4,X5:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 ) )
theorem :: MCART_2:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
Z,
X1,
X2,
X3,
X4,
X5 being
set st ( for
y being
set holds
(
y in Z iff ex
x1,
x2,
x3,
x4,
x5 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
y = [x1,x2,x3,x4,x5] ) ) ) holds
Z = [:X1,X2,X3,X4,X5:]
theorem Th33: :: MCART_2:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 )
theorem :: MCART_2:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
X2,
X3,
X4,
X5 being
set for
A1 being
Subset of
X1 for
A2 being
Subset of
X2 for
A3 being
Subset of
X3 for
A4 being
Subset of
X4 for
A5 being
Subset of
X5 for
x being
Element of
[:X1,X2,X3,X4,X5:] st
x in [:A1,A2,A3,A4,A5:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 )
theorem Th35: :: MCART_2:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
X1,
Y1,
X2,
Y2,
X3,
Y3,
X4,
Y4,
X5,
Y5 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 holds
[:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]
definition
let X1,
X2,
X3,
X4,
X5 be
set ;
let A1 be
Subset of
X1;
let A2 be
Subset of
X2;
let A3 be
Subset of
X3;
let A4 be
Subset of
X4;
let A5 be
Subset of
X5;
:: original: [:redefine func [:A1,A2,A3,A4,A5:] -> Subset of
[:X1,X2,X3,X4,X5:];
coherence
[:A1,A2,A3,A4,A5:] is Subset of [:X1,X2,X3,X4,X5:]
by Th35;
end;
theorem :: MCART_2:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: MCART_2:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: MCART_2:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)