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:
( field (LattRel [:L1,L2:]) = the carrier of [:L1,L2:] & field (LattRel [:L2,L1:]) = the carrier of [:L2,L1:] & [:L1,L2:] = LattStr(# [:the carrier of L1,the carrier of L2:],|:H1(L1),H1(L2):|,|:H2(L1),H2(L2):| #) & [:L2,L1:] = LattStr(# [:the carrier of L2,the carrier of L1:],|:H1(L2),H1(L1):|,|:H2(L2),H2(L1):| #) )
by Th33;
( dom (pr1 the carrier of L1,the carrier of L2) = [:the carrier of L1,the carrier of L2:] & dom (pr2 the carrier of L1,the carrier of L2) = [:the carrier of L1,the carrier of L2:] )
by FUNCT_3:def 5, FUNCT_3:def 6;
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:]
;
hence A2:
dom f = field (LattRel [:L1,L2:])
by A1, FUNCT_3:def 8; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:L2,L1:]) & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
( rng (pr1 the carrier of L1,the carrier of L2) = the carrier of L1 & rng (pr2 the carrier of L1,the carrier of L2) = the carrier of L2 )
by FUNCT_3:60, FUNCT_3:62;
hence
rng f c= field (LattRel [:L2,L1:])
by A1, FUNCT_3:71; :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:L2,L1:]) c= rng f & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
thus
field (LattRel [:L2,L1:]) c= rng f
:: thesis: ( f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )proof
let x be
set ;
:: 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 A3:
x = [r2,r1]
by A1, DOMAIN_1:9;
(
f . [r1,r2] in rng f &
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])] &
(pr2 the carrier of L1,the carrier of L2) . r1,
r2 = r2 &
(pr1 the carrier of L1,the carrier of L2) . r1,
r2 = r1 )
by A1, A2, FUNCT_1:def 5, FUNCT_3:def 5, FUNCT_3:def 6, FUNCT_3:def 8;
hence
x in rng f
by A3;
:: thesis: verum
end;
thus
f is one-to-one
:: thesis: for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) )proof
let x be
set ;
:: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )let y be
set ;
:: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A4:
x in dom f
;
:: thesis: ( not y in dom f or not f . x = f . y or x = y )
then consider r1 being
Element of
L1,
r2 being
Element of
L2 such that A5:
x = [r1,r2]
by A1, A2, DOMAIN_1:9;
assume A6:
(
y in dom f &
f . x = f . y )
;
:: thesis: x = y
then consider q1 being
Element of
L1,
q2 being
Element of
L2 such that A7:
y = [q1,q2]
by A1, A2, DOMAIN_1:9;
(
(pr1 the carrier of L1,the carrier of L2) . r1,
r2 = r1 &
(pr2 the carrier of L1,the carrier of L2) . r1,
r2 = r2 &
(pr1 the carrier of L1,the carrier of L2) . q1,
q2 = q1 &
(pr2 the carrier of L1,the carrier of L2) . q1,
q2 = q2 &
f . x = [((pr2 the carrier of L1,the carrier of L2) . x),((pr1 the carrier of L1,the carrier of L2) . x)] &
f . y = [((pr2 the carrier of L1,the carrier of L2) . y),((pr1 the carrier of L1,the carrier of L2) . y)] )
by A4, A6, FUNCT_3:def 5, FUNCT_3:def 6, FUNCT_3:def 8;
then
(
r1 = q1 &
r2 = q2 )
by A5, A6, A7, ZFMISC_1:33;
hence
x = y
by A5, A7;
:: thesis: verum
end;
let x, y be set ; :: 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:] ) )
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
[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 A8:
(
[x,y] = [a,b] &
a [= b )
;
consider r1 being
Element of
L1,
r2 being
Element of
L2 such that A9:
a = [r1,r2]
by DOMAIN_1:9;
consider q1 being
Element of
L1,
q2 being
Element of
L2 such that A10:
b = [q1,q2]
by DOMAIN_1:9;
A11:
(
r1 [= q1 &
r2 [= q2 )
by A8, A9, A10, Th37;
A12:
(
x = a &
y = b )
by A8, ZFMISC_1:33;
hence
(
x in field (LattRel [:L1,L2:]) &
y in field (LattRel [:L1,L2:]) )
by A1;
:: thesis: [(f . x),(f . y)] in LattRel [:L2,L1:]
(
[r2,r1] [= [q2,q1] &
(pr1 the carrier of L1,the carrier of L2) . r1,
r2 = r1 &
(pr2 the carrier of L1,the carrier of L2) . r1,
r2 = r2 &
(pr1 the carrier of L1,the carrier of L2) . q1,
q2 = q1 &
(pr2 the carrier of L1,the carrier of L2) . q1,
q2 = q2 &
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)] &
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 A1, A2, A9, A10, A11, Th37, FUNCT_3:def 5, FUNCT_3:def 6, FUNCT_3:def 8;
hence
[(f . x),(f . y)] in LattRel [:L2,L1:]
by A9, A10, A12;
:: thesis: verum
end;
assume A13:
( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) )
; :: thesis: ( not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )
then consider r1 being Element of L1, r2 being Element of L2 such that
A14:
x = [r1,r2]
by A1, DOMAIN_1:9;
consider q1 being Element of L1, q2 being Element of L2 such that
A15:
y = [q1,q2]
by A1, A13, DOMAIN_1:9;
assume A16:
[(f . x),(f . y)] in LattRel [:L2,L1:]
; :: thesis: [x,y] in LattRel [:L1,L2:]
( 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)] & (pr1 the carrier of L1,the carrier of L2) . r1,r2 = r1 & (pr2 the carrier of L1,the carrier of L2) . r1,r2 = r2 & 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)] & (pr1 the carrier of L1,the carrier of L2) . q1,q2 = q1 & (pr2 the carrier of L1,the carrier of L2) . q1,q2 = q2 )
by A1, A2, A14, A15, FUNCT_3:def 5, FUNCT_3:def 6, FUNCT_3:def 8;
then
[r2,r1] [= [q2,q1]
by A14, A15, A16, Th32;
then
( r2 [= q2 & r1 [= q1 )
by Th37;
then
[r1,r2] [= [q1,q2]
by Th37;
hence
[x,y] in LattRel [:L1,L2:]
by A14, A15; :: thesis: verum