let L1, L2 be Lattice; :: thesis: [:L1,L2:],[:L2,L1:] are_isomorphic

set R = LattRel [:L1,L2:];

set S = LattRel [:L2,L1:];

set D1 = the carrier of L1;

set D2 = the carrier of L2;

set p2 = pr2 ( the carrier of L1, the carrier of L2);

set p1 = pr1 ( the carrier of L1, the carrier of L2);

take f = <:(pr2 ( the carrier of L1, the carrier of L2)),(pr1 ( the carrier of L1, the carrier of L2)):>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel [:L1,L2:], LattRel [:L2,L1:]

A1: dom (pr2 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 5;

A2: field (LattRel [:L1,L2:]) = the carrier of [:L1,L2:] by Th32;

A3: rng (pr2 ( the carrier of L1, the carrier of L2)) = the carrier of L2 by FUNCT_3:46;

A4: field (LattRel [:L2,L1:]) = the carrier of [:L2,L1:] by Th32;

dom (pr1 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 4;

then (dom (pr2 ( the carrier of L1, the carrier of L2))) /\ (dom (pr1 ( the carrier of L1, the carrier of L2))) = [: the carrier of L1, the carrier of L2:] by A1;

hence A5: dom f = field (LattRel [:L1,L2:]) by A2, FUNCT_3:def 7; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:L2,L1:]) & f is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel [:L1,L2:] or ( b_{1} in field (LattRel [:L1,L2:]) & b_{2} in field (LattRel [:L1,L2:]) & [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] ) ) & ( not b_{1} in field (LattRel [:L1,L2:]) or not b_{2} in field (LattRel [:L1,L2:]) or not [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] or [b_{1},b_{2}] in LattRel [:L1,L2:] ) ) ) )

rng (pr1 ( the carrier of L1, the carrier of L2)) = the carrier of L1 by FUNCT_3:44;

hence rng f c= field (LattRel [:L2,L1:]) by A4, A3, FUNCT_3:51; :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:L2,L1:]) c= rng f & f is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel [:L1,L2:] or ( b_{1} in field (LattRel [:L1,L2:]) & b_{2} in field (LattRel [:L1,L2:]) & [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] ) ) & ( not b_{1} in field (LattRel [:L1,L2:]) or not b_{2} in field (LattRel [:L1,L2:]) or not [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] or [b_{1},b_{2}] in LattRel [:L1,L2:] ) ) ) )

thus field (LattRel [:L2,L1:]) c= rng f :: thesis: ( f is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel [:L1,L2:] or ( b_{1} in field (LattRel [:L1,L2:]) & b_{2} in field (LattRel [:L1,L2:]) & [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] ) ) & ( not b_{1} in field (LattRel [:L1,L2:]) or not b_{2} in field (LattRel [:L1,L2:]) or not [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] or [b_{1},b_{2}] in LattRel [:L1,L2:] ) ) ) )_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel [:L1,L2:] or ( b_{1} in field (LattRel [:L1,L2:]) & b_{2} in field (LattRel [:L1,L2:]) & [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] ) ) & ( not b_{1} in field (LattRel [:L1,L2:]) or not b_{2} in field (LattRel [:L1,L2:]) or not [(f . b_{1}),(f . b_{2})] in LattRel [:L2,L1:] or [b_{1},b_{2}] in LattRel [:L1,L2:] ) )

thus ( [x,y] in LattRel [:L1,L2:] implies ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) :: thesis: ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )

A32: x in field (LattRel [:L1,L2:]) and

A33: y in field (LattRel [:L1,L2:]) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )

consider q1 being Element of L1, q2 being Element of L2 such that

A34: y = [q1,q2] by A2, A33, DOMAIN_1:1;

A35: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A34, FUNCT_3:def 7;

assume A36: [(f . x),(f . y)] in LattRel [:L2,L1:] ; :: thesis: [x,y] in LattRel [:L1,L2:]

A37: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

A38: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

consider r1 being Element of L1, r2 being Element of L2 such that

A39: x = [r1,r2] by A2, A32, DOMAIN_1:1;

A40: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A41: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A39, FUNCT_3:def 7;

then A42: [r2,r1] [= [q2,q1] by A39, A34, A36, A41, A40, A35, A38, A37, Th31;

then A43: r1 [= q1 by Th36;

r2 [= q2 by A42, Th36;

then [r1,r2] [= [q1,q2] by A43, Th36;

hence [x,y] in LattRel [:L1,L2:] by A39, A34; :: thesis: verum

set R = LattRel [:L1,L2:];

set S = LattRel [:L2,L1:];

set D1 = the carrier of L1;

set D2 = the carrier of L2;

set p2 = pr2 ( the carrier of L1, the carrier of L2);

set p1 = pr1 ( the carrier of L1, the carrier of L2);

take f = <:(pr2 ( the carrier of L1, the carrier of L2)),(pr1 ( the carrier of L1, the carrier of L2)):>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel [:L1,L2:], LattRel [:L2,L1:]

A1: dom (pr2 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 5;

A2: field (LattRel [:L1,L2:]) = the carrier of [:L1,L2:] by Th32;

A3: rng (pr2 ( the carrier of L1, the carrier of L2)) = the carrier of L2 by FUNCT_3:46;

A4: field (LattRel [:L2,L1:]) = the carrier of [:L2,L1:] by Th32;

dom (pr1 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 4;

then (dom (pr2 ( the carrier of L1, the carrier of L2))) /\ (dom (pr1 ( the carrier of L1, the carrier of L2))) = [: the carrier of L1, the carrier of L2:] by A1;

hence A5: dom f = field (LattRel [:L1,L2:]) by A2, FUNCT_3:def 7; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:L2,L1:]) & f is one-to-one & ( for b

( ( not [b

rng (pr1 ( the carrier of L1, the carrier of L2)) = the carrier of L1 by FUNCT_3:44;

hence rng f c= field (LattRel [:L2,L1:]) by A4, A3, FUNCT_3:51; :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:L2,L1:]) c= rng f & f is one-to-one & ( for b

( ( not [b

thus field (LattRel [:L2,L1:]) c= rng f :: thesis: ( f is one-to-one & ( for b

( ( not [b

proof

thus
f is one-to-one
:: thesis: for b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field (LattRel [:L2,L1:]) or x in rng f )

assume x in field (LattRel [:L2,L1:]) ; :: thesis: x in rng f

then consider r2 being Element of L2, r1 being Element of L1 such that

A6: x = [r2,r1] by A4, DOMAIN_1:1;

A7: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A8: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

f . [r1,r2] in rng f by A2, A5, FUNCT_1:def 3;

hence x in rng f by A2, A5, A6, A7, A8, FUNCT_3:def 7; :: thesis: verum

end;assume x in field (LattRel [:L2,L1:]) ; :: thesis: x in rng f

then consider r2 being Element of L2, r1 being Element of L1 such that

A6: x = [r2,r1] by A4, DOMAIN_1:1;

A7: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A8: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

f . [r1,r2] in rng f by A2, A5, FUNCT_1:def 3;

hence x in rng f by A2, A5, A6, A7, A8, FUNCT_3:def 7; :: thesis: verum

( ( not [b

proof

let x, y be object ; :: thesis: ( ( not [x,y] in LattRel [:L1,L2:] or ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) & ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] ) )
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )

assume A9: x in dom f ; :: thesis: ( not y in dom f or not f . x = f . y or x = y )

then A10: f . x = [((pr2 ( the carrier of L1, the carrier of L2)) . x),((pr1 ( the carrier of L1, the carrier of L2)) . x)] by FUNCT_3:def 7;

consider r1 being Element of L1, r2 being Element of L2 such that

A11: x = [r1,r2] by A2, A5, A9, DOMAIN_1:1;

A12: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A13: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

assume that

A14: y in dom f and

A15: f . x = f . y ; :: thesis: x = y

A16: f . y = [((pr2 ( the carrier of L1, the carrier of L2)) . y),((pr1 ( the carrier of L1, the carrier of L2)) . y)] by A14, FUNCT_3:def 7;

consider q1 being Element of L1, q2 being Element of L2 such that

A17: y = [q1,q2] by A2, A5, A14, DOMAIN_1:1;

A18: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

(pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

then r1 = q1 by A11, A15, A17, A13, A10, A16, XTUPLE_0:1;

hence x = y by A11, A15, A17, A12, A18, A10, A16, XTUPLE_0:1; :: thesis: verum

end;assume A9: x in dom f ; :: thesis: ( not y in dom f or not f . x = f . y or x = y )

then A10: f . x = [((pr2 ( the carrier of L1, the carrier of L2)) . x),((pr1 ( the carrier of L1, the carrier of L2)) . x)] by FUNCT_3:def 7;

consider r1 being Element of L1, r2 being Element of L2 such that

A11: x = [r1,r2] by A2, A5, A9, DOMAIN_1:1;

A12: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A13: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

assume that

A14: y in dom f and

A15: f . x = f . y ; :: thesis: x = y

A16: f . y = [((pr2 ( the carrier of L1, the carrier of L2)) . y),((pr1 ( the carrier of L1, the carrier of L2)) . y)] by A14, FUNCT_3:def 7;

consider q1 being Element of L1, q2 being Element of L2 such that

A17: y = [q1,q2] by A2, A5, A14, DOMAIN_1:1;

A18: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

(pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

then r1 = q1 by A11, A15, A17, A13, A10, A16, XTUPLE_0:1;

hence x = y by A11, A15, A17, A12, A18, A10, A16, XTUPLE_0:1; :: thesis: verum

thus ( [x,y] in LattRel [:L1,L2:] implies ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) :: thesis: ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )

proof

assume that
assume
[x,y] in LattRel [:L1,L2:]
; :: thesis: ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] )

then consider a, b being Element of [:L1,L2:] such that

A19: [x,y] = [a,b] and

A20: a [= b ;

consider q1 being Element of L1, q2 being Element of L2 such that

A21: b = [q1,q2] by DOMAIN_1:1;

A22: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A21, FUNCT_3:def 7;

A23: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

consider r1 being Element of L1, r2 being Element of L2 such that

A24: a = [r1,r2] by DOMAIN_1:1;

A25: r2 [= q2 by A20, A24, A21, Th36;

r1 [= q1 by A20, A24, A21, Th36;

then A26: [r2,r1] [= [q2,q1] by A25, Th36;

A27: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

A28: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A29: y = b by A19, XTUPLE_0:1;

A30: x = a by A19, XTUPLE_0:1;

hence ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) ) by A2, A29; :: thesis: [(f . x),(f . y)] in LattRel [:L2,L1:]

A31: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A24, FUNCT_3:def 7;

hence [(f . x),(f . y)] in LattRel [:L2,L1:] by A24, A21, A30, A29, A26, A27, A28, A31, A23, A22; :: thesis: verum

end;then consider a, b being Element of [:L1,L2:] such that

A19: [x,y] = [a,b] and

A20: a [= b ;

consider q1 being Element of L1, q2 being Element of L2 such that

A21: b = [q1,q2] by DOMAIN_1:1;

A22: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A21, FUNCT_3:def 7;

A23: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

consider r1 being Element of L1, r2 being Element of L2 such that

A24: a = [r1,r2] by DOMAIN_1:1;

A25: r2 [= q2 by A20, A24, A21, Th36;

r1 [= q1 by A20, A24, A21, Th36;

then A26: [r2,r1] [= [q2,q1] by A25, Th36;

A27: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

A28: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A29: y = b by A19, XTUPLE_0:1;

A30: x = a by A19, XTUPLE_0:1;

hence ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) ) by A2, A29; :: thesis: [(f . x),(f . y)] in LattRel [:L2,L1:]

A31: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A24, FUNCT_3:def 7;

hence [(f . x),(f . y)] in LattRel [:L2,L1:] by A24, A21, A30, A29, A26, A27, A28, A31, A23, A22; :: thesis: verum

A32: x in field (LattRel [:L1,L2:]) and

A33: y in field (LattRel [:L1,L2:]) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )

consider q1 being Element of L1, q2 being Element of L2 such that

A34: y = [q1,q2] by A2, A33, DOMAIN_1:1;

A35: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A34, FUNCT_3:def 7;

assume A36: [(f . x),(f . y)] in LattRel [:L2,L1:] ; :: thesis: [x,y] in LattRel [:L1,L2:]

A37: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;

A38: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;

consider r1 being Element of L1, r2 being Element of L2 such that

A39: x = [r1,r2] by A2, A32, DOMAIN_1:1;

A40: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;

A41: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;

f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A39, FUNCT_3:def 7;

then A42: [r2,r1] [= [q2,q1] by A39, A34, A36, A41, A40, A35, A38, A37, Th31;

then A43: r1 [= q1 by Th36;

r2 [= q2 by A42, Th36;

then [r1,r2] [= [q1,q2] by A43, Th36;

hence [x,y] in LattRel [:L1,L2:] by A39, A34; :: thesis: verum