A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
thus product J is directed :: thesis: product J is transitive
proof
let x, y be Element of (product J); :: according to YELLOW_6:def 3 :: thesis: ex z being Element of (product J) st
( x <= z & y <= z )
defpred S1[ Element of Y, object ] means ( [(x . T),Y] in the InternalRel of (J . T) & [(y . T),Y] in the InternalRel of (J . T) );
A2: now :: thesis: for i being Element of Y ex z being object st S1[i,z]
let i be Element of Y; :: thesis: ex z being object st S1[i,z]
consider zi being Element of (J . i) such that
A3: ( x . i <= zi & y . i <= zi ) by Def3;
reconsider z = zi as object ;
take z = z; :: thesis: S1[i,z]
thus S1[i,z] by A3, ORDERS_2:def 5; :: thesis: verum
end;
consider z being ManySortedSet of the carrier of Y such that
A4: for i being Element of Y holds S1[i,z . i] from PBOOLE:sch 6(A2);
A5: now :: thesis: for i being object st i in dom (Carrier J) holds
z . i in (Carrier J) . i
let i be object ; :: thesis: ( i in dom (Carrier J) implies z . i in (Carrier J) . i )
assume i in dom (Carrier J) ; :: thesis: z . i in (Carrier J) . i
then reconsider j = i as Element of Y ;
[(x . j),(z . j)] in the InternalRel of (J . j) by A4;
then z . j in the carrier of (J . j) by ZFMISC_1:87;
hence z . i in (Carrier J) . i by Th2; :: thesis: verum
end;
dom z = the carrier of Y by PARTFUN1:def 2
.= dom (Carrier J) by PARTFUN1:def 2 ;
then reconsider z = z as Element of (product J) by A1, A5, CARD_3:9;
take z ; :: thesis: ( x <= z & y <= z )
for i being object st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
proof
let i be object ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume i in the carrier of Y ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
reconsider xi = x . j, zi = z . j as Element of (J . j) ;
take J . j ; :: thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take zi ; :: thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus ( J . j = J . i & xi = x . i & zi = z . i ) ; :: thesis: xi <= zi
[xi,zi] in the InternalRel of (J . j) by A4;
hence xi <= zi by ORDERS_2:def 5; :: thesis: verum
end;
hence x <= z by A1, YELLOW_1:def 4; :: thesis: y <= z
for i being object st i in the carrier of Y holds
ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )
proof
let i be object ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi ) )
assume i in the carrier of Y ; :: thesis: ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )
then reconsider j = i as Element of Y ;
reconsider yi = y . j, zi = z . j as Element of (J . j) ;
take J . j ; :: thesis: ex yi, zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take yi ; :: thesis: ex zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take zi ; :: thesis: ( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
thus ( J . j = J . i & yi = y . i & zi = z . i ) ; :: thesis: yi <= zi
[yi,zi] in the InternalRel of (J . j) by A4;
hence yi <= zi by ORDERS_2:def 5; :: thesis: verum
end;
hence y <= z by A1, YELLOW_1:def 4; :: thesis: verum
end;
let x, y, z be Element of (product J); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A6: x <= y and
A7: y <= z ; :: thesis: x <= z
A8: ex fy, gz being Function st
( fy = y & gz = z & ( for i being object st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fy . i & yi = gz . i & xi <= yi ) ) ) by A1, A7, YELLOW_1:def 4;
A9: ex fx, gy being Function st
( fx = x & gy = y & ( for i being object st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fx . i & yi = gy . i & xi <= yi ) ) ) by A1, A6, YELLOW_1:def 4;
for i being object st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
proof
let i be object ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume A10: i in the carrier of Y ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
consider R1 being RelStr , xi, yi being Element of R1 such that
A11: R1 = J . i and
A12: xi = x . i and
A13: ( yi = y . i & xi <= yi ) by A9, A10;
consider R2 being RelStr , yi9, zi being Element of R2 such that
A14: R2 = J . i and
A15: yi9 = y . i and
A16: zi = z . i and
A17: yi9 <= zi by A8, A10;
reconsider xi = xi, zi = zi as Element of (J . j) by A11, A14;
take J . j ; :: thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take zi ; :: thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus ( J . j = J . i & xi = x . i & zi = z . i ) by A12, A16; :: thesis: xi <= zi
thus xi <= zi by A11, A13, A14, A15, A17, YELLOW_0:def 2; :: thesis: verum
end;
hence x <= z by A1, YELLOW_1:def 4; :: thesis: verum