let B be B_Lattice; :: thesis: for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic

let a be Element of B; :: thesis: B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic

set F = <.a.);

set E = equivalence_wrt <.a.);

deffunc H_{3}( object ) -> Element of bool the carrier of B = Class ((equivalence_wrt <.a.)),$1);

consider g being Function such that

A1: ( dom g = the carrier of B & ( for x being object st x in the carrier of B holds

g . x = H_{3}(x) ) )
from FUNCT_1:sch 3();

A2: for b being Element of B holds (b "\/" (b <=> a)) <=> b = b "\/" a

A14: field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] by Th32;

reconsider o1 = H_{1}(B), o2 = H_{2}(B) as BinOp of equivalence_wrt <.a.) by Th13, Th14;

A15: LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) by Def5;

set R = LattRel B;

deffunc H_{4}( Element of B) -> Element of the carrier of B = ($1 "\/" ($1 <=> a)) <=> $1;

consider h being UnOp of the carrier of B such that

A16: for b being Element of B holds h . b = H_{4}(b)
from FUNCT_2:sch 4();

take f = <:g,h:>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel B, LattRel [:(B /\/ <.a.)),(latt <.a.)):]

A17: field (LattRel B) = the carrier of B by Th32;

A18: dom h = dom g by A1, FUNCT_2:def 1;

hence A19: dom f = field (LattRel B) by A1, A17, FUNCT_3:50; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) & f is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel B or ( b_{1} in field (LattRel B) & b_{2} in field (LattRel B) & [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b_{1} in field (LattRel B) or not b_{2} in field (LattRel B) or not [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b_{1},b_{2}] in LattRel B ) ) ) )

A20: for b being Element of B holds h . b is Element of (latt <.a.))_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel B or ( b_{1} in field (LattRel B) & b_{2} in field (LattRel B) & [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b_{1} in field (LattRel B) or not b_{2} in field (LattRel B) or not [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b_{1},b_{2}] in LattRel B ) ) ) )

thus field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f :: thesis: ( f is one-to-one & ( for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel B or ( b_{1} in field (LattRel B) & b_{2} in field (LattRel B) & [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b_{1} in field (LattRel B) or not b_{2} in field (LattRel B) or not [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b_{1},b_{2}] in LattRel B ) ) ) )_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in LattRel B or ( b_{1} in field (LattRel B) & b_{2} in field (LattRel B) & [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b_{1} in field (LattRel B) or not b_{2} in field (LattRel B) or not [(f . b_{1}),(f . b_{2})] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b_{1},b_{2}] in LattRel B ) )

A45: the carrier of (latt <.a.)) = <.a.) by FILTER_0:49;

thus ( [x,y] in LattRel B implies ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) :: thesis: ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )

A61: x in field (LattRel B) and

A62: y in field (LattRel B) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )

reconsider x9 = x, y9 = y as Element of B by A61, A62, Th32;

A63: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A64: f . y9 = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A65: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;

A66: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;

A67: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;

A68: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;

A69: y9 "/\" x9 [= y9 by LATTICES:6;

A70: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;

A71: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;

then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A45, A63, A71, A70, Lm4;

assume A72: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; :: thesis: [x,y] in LattRel B

A73: f . x9 = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

A74: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;

x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;

then A75: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A65, A66, A74, A73, A64, A72, Th31;

then x9 /\/ <.a.) [= y9 /\/ <.a.) by Th36;

then A76: x9 => y9 in <.a.) by Th16;

x9 => y9 = (x9 `) "\/" y9 by FILTER_0:42;

then a [= (x9 `) "\/" y9 by A76, FILTER_0:15;

then A77: x9 "/\" a [= x9 "/\" ((x9 `) "\/" y9) by LATTICES:9;

hx [= hy by A75, Th36;

then x9 "\/" a [= y9 "\/" a by A63, A71, A68, A67, FILTER_0:51;

then A78: x9 "/\" (x9 "\/" a) [= x9 "/\" (y9 "\/" a) by LATTICES:9;

A79: x9 "/\" (x9 `) = Bottom B by LATTICES:20;

x9 "/\" ((x9 `) "\/" y9) = (x9 "/\" (x9 `)) "\/" (x9 "/\" y9) by LATTICES:def 11;

then x9 "/\" a [= y9 by A77, A79, A69, LATTICES:7;

then A80: (x9 "/\" y9) "\/" (x9 "/\" a) [= y9 by A69, FILTER_0:6;

x9 [= x9 "\/" a by LATTICES:5;

then x9 "/\" (x9 "\/" a) = x9 by LATTICES:4;

then x9 [= (x9 "/\" y9) "\/" (x9 "/\" a) by A78, LATTICES:def 11;

then x9 [= y9 by A80, LATTICES:7;

hence [x,y] in LattRel B ; :: thesis: verum

let a be Element of B; :: thesis: B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic

set F = <.a.);

set E = equivalence_wrt <.a.);

deffunc H

consider g being Function such that

A1: ( dom g = the carrier of B & ( for x being object st x in the carrier of B holds

g . x = H

A2: for b being Element of B holds (b "\/" (b <=> a)) <=> b = b "\/" a

proof

set S = LattRel [:(B /\/ <.a.)),(latt <.a.)):];
let b be Element of B; :: thesis: (b "\/" (b <=> a)) <=> b = b "\/" a

A3: (b "\/" (b <=> a)) ` = (b `) "/\" ((b <=> a) `) by LATTICES:24;

A4: (b `) "/\" ((b "/\" (a `)) "\/" ((b `) "/\" a)) = ((b `) "/\" (b "/\" (a `))) "\/" ((b `) "/\" ((b `) "/\" a)) by LATTICES:def 11;

A5: b "\/" ((b "/\" a) "\/" ((b `) "/\" (a `))) = (b "\/" (b "/\" a)) "\/" ((b `) "/\" (a `)) by LATTICES:def 5;

A6: b <=> a = (b "/\" a) "\/" ((b `) "/\" (a `)) by Th50;

A7: (b `) "/\" b = Bottom B by LATTICES:20;

A8: (b `) "/\" ((a `) "/\" b) = ((b `) "/\" (a `)) "/\" b by LATTICES:def 7;

A9: (b `) "/\" ((b `) "/\" a) = ((b `) "/\" (b `)) "/\" a by LATTICES:def 7;

A10: (b <=> a) ` = (b "/\" (a `)) "\/" ((b `) "/\" a) by Th51;

A11: (b `) "/\" (b "/\" (a `)) = ((b `) "/\" b) "/\" (a `) by LATTICES:def 7;

A12: (b "\/" ((b `) "/\" (a `))) "/\" b = (b "/\" b) "\/" (((b `) "/\" (a `)) "/\" b) by LATTICES:def 11;

A13: (b "/\" a) "\/" b = b by LATTICES:def 8;

(b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) `) "/\" (b `)) by Th50;

hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b `) "/\" a)) by A3, A10, A4, A11, A7, A9, A6, A5, A13, A12, A8, LATTICES:def 5

.= b "\/" ((b "\/" (b `)) "/\" a) by LATTICES:def 11

.= b "\/" ((Top B) "/\" a) by LATTICES:21

.= b "\/" a ;

:: thesis: verum

end;A3: (b "\/" (b <=> a)) ` = (b `) "/\" ((b <=> a) `) by LATTICES:24;

A4: (b `) "/\" ((b "/\" (a `)) "\/" ((b `) "/\" a)) = ((b `) "/\" (b "/\" (a `))) "\/" ((b `) "/\" ((b `) "/\" a)) by LATTICES:def 11;

A5: b "\/" ((b "/\" a) "\/" ((b `) "/\" (a `))) = (b "\/" (b "/\" a)) "\/" ((b `) "/\" (a `)) by LATTICES:def 5;

A6: b <=> a = (b "/\" a) "\/" ((b `) "/\" (a `)) by Th50;

A7: (b `) "/\" b = Bottom B by LATTICES:20;

A8: (b `) "/\" ((a `) "/\" b) = ((b `) "/\" (a `)) "/\" b by LATTICES:def 7;

A9: (b `) "/\" ((b `) "/\" a) = ((b `) "/\" (b `)) "/\" a by LATTICES:def 7;

A10: (b <=> a) ` = (b "/\" (a `)) "\/" ((b `) "/\" a) by Th51;

A11: (b `) "/\" (b "/\" (a `)) = ((b `) "/\" b) "/\" (a `) by LATTICES:def 7;

A12: (b "\/" ((b `) "/\" (a `))) "/\" b = (b "/\" b) "\/" (((b `) "/\" (a `)) "/\" b) by LATTICES:def 11;

A13: (b "/\" a) "\/" b = b by LATTICES:def 8;

(b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) `) "/\" (b `)) by Th50;

hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b `) "/\" a)) by A3, A10, A4, A11, A7, A9, A6, A5, A13, A12, A8, LATTICES:def 5

.= b "\/" ((b "\/" (b `)) "/\" a) by LATTICES:def 11

.= b "\/" ((Top B) "/\" a) by LATTICES:21

.= b "\/" a ;

:: thesis: verum

A14: field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] by Th32;

reconsider o1 = H

A15: LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) by Def5;

set R = LattRel B;

deffunc H

consider h being UnOp of the carrier of B such that

A16: for b being Element of B holds h . b = H

take f = <:g,h:>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel B, LattRel [:(B /\/ <.a.)),(latt <.a.)):]

A17: field (LattRel B) = the carrier of B by Th32;

A18: dom h = dom g by A1, FUNCT_2:def 1;

hence A19: dom f = field (LattRel B) by A1, A17, FUNCT_3:50; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) & f is one-to-one & ( for b

( ( not [b

A20: for b being Element of B holds h . b is Element of (latt <.a.))

proof

thus
rng f c= field (LattRel [:(B /\/ <.a.)),(latt <.a.)):])
:: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f & f is one-to-one & ( for b
let b be Element of B; :: thesis: h . b is Element of (latt <.a.))

b "\/" (b <=> a) in Class ((equivalence_wrt <.a.)),b) by Th60;

then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:19;

then A21: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def 11;

h . b = (b "\/" (b <=> a)) <=> b by A16;

hence h . b is Element of (latt <.a.)) by A21, FILTER_0:49; :: thesis: verum

end;b "\/" (b <=> a) in Class ((equivalence_wrt <.a.)),b) by Th60;

then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:19;

then A21: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def 11;

h . b = (b "\/" (b <=> a)) <=> b by A16;

hence h . b is Element of (latt <.a.)) by A21, FILTER_0:49; :: thesis: verum

( ( not [b

proof

A24:
the carrier of (latt <.a.)) = <.a.)
by FILTER_0:49;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) )

assume x in rng f ; :: thesis: x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):])

then consider y being object such that

A22: y in dom f and

A23: x = f . y by FUNCT_1:def 3;

reconsider y = y as Element of B by A1, A18, A22, FUNCT_3:50;

reconsider z2 = h . y as Element of (latt <.a.)) by A20;

g . y = EqClass ((equivalence_wrt <.a.)),y) by A1;

then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A15;

x = [z1,z2] by A22, A23, FUNCT_3:def 7;

hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A14; :: thesis: verum

end;assume x in rng f ; :: thesis: x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):])

then consider y being object such that

A22: y in dom f and

A23: x = f . y by FUNCT_1:def 3;

reconsider y = y as Element of B by A1, A18, A22, FUNCT_3:50;

reconsider z2 = h . y as Element of (latt <.a.)) by A20;

g . y = EqClass ((equivalence_wrt <.a.)),y) by A1;

then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A15;

x = [z1,z2] by A22, A23, FUNCT_3:def 7;

hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A14; :: thesis: verum

thus field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) 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 [:(B /\/ <.a.)),(latt <.a.)):]) or x in rng f )

assume x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) ; :: thesis: x in rng f

then consider y being Element of Class (equivalence_wrt <.a.)), z being Element of <.a.) such that

A25: x = [y,z] by A14, A24, A15, DOMAIN_1:1;

consider b being Element of B such that

A26: y = Class ((equivalence_wrt <.a.)),b) by EQREL_1:36;

set ty = b "\/" (b <=> a);

(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th53;

then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;

then A27: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 11;

b "\/" (b <=> a) in y by A26, Th60;

then y = Class ((equivalence_wrt <.a.)),(b "\/" (b <=> a))) by A26, EQREL_1:23;

then A28: (b "\/" (b <=> a)) <=> z in y by A27, EQREL_1:19;

then A29: y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A26, EQREL_1:23;

then A30: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by A26, Th60;

y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A26, A28, EQREL_1:23;

then A31: g . ((b "\/" (b <=> a)) <=> z) = y by A1;

((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by A26, A29, Th60;

then A32: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by A30, LATTICES:8;

h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A16;

then h . ((b "\/" (b <=> a)) <=> z) = z by A32, Th53;

then x = f . ((b "\/" (b <=> a)) <=> z) by A17, A19, A25, A31, FUNCT_3:def 7;

hence x in rng f by A17, A19, FUNCT_1:def 3; :: thesis: verum

end;assume x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) ; :: thesis: x in rng f

then consider y being Element of Class (equivalence_wrt <.a.)), z being Element of <.a.) such that

A25: x = [y,z] by A14, A24, A15, DOMAIN_1:1;

consider b being Element of B such that

A26: y = Class ((equivalence_wrt <.a.)),b) by EQREL_1:36;

set ty = b "\/" (b <=> a);

(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th53;

then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;

then A27: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 11;

b "\/" (b <=> a) in y by A26, Th60;

then y = Class ((equivalence_wrt <.a.)),(b "\/" (b <=> a))) by A26, EQREL_1:23;

then A28: (b "\/" (b <=> a)) <=> z in y by A27, EQREL_1:19;

then A29: y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A26, EQREL_1:23;

then A30: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by A26, Th60;

y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A26, A28, EQREL_1:23;

then A31: g . ((b "\/" (b <=> a)) <=> z) = y by A1;

((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by A26, A29, Th60;

then A32: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by A30, LATTICES:8;

h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A16;

then h . ((b "\/" (b <=> a)) <=> z) = z by A32, Th53;

then x = f . ((b "\/" (b <=> a)) <=> z) by A17, A19, A25, A31, FUNCT_3:def 7;

hence x in rng f by A17, A19, FUNCT_1:def 3; :: thesis: verum

( ( not [b

proof

let x, y be object ; :: thesis: ( ( not [x,y] in LattRel B or ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B ) )
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 that

A33: x in dom f and

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

reconsider x9 = x, y9 = y as Element of B by A1, A18, A33, A34, FUNCT_3:50;

assume A35: f . x = f . y ; :: thesis: x = y

A36: g . y9 = Class ((equivalence_wrt <.a.)),y9) by A1;

A37: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

A38: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A39: g . x9 = Class ((equivalence_wrt <.a.)),x9) by A1;

A40: f . y = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A41: f . x = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

then A42: g . x = g . y by A40, A35, XTUPLE_0:1;

then A43: y9 "\/" (y9 <=> a) [= x9 "\/" (x9 <=> a) by A39, A36, Th60;

x9 "\/" (x9 <=> a) [= y9 "\/" (y9 <=> a) by A39, A36, A42, Th60;

then A44: y9 "\/" (y9 <=> a) = x9 "\/" (x9 <=> a) by A43, LATTICES:8;

h . x = h . y by A41, A40, A35, XTUPLE_0:1;

hence x = y by A38, A37, A44, Th52; :: thesis: verum

end;assume that

A33: x in dom f and

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

reconsider x9 = x, y9 = y as Element of B by A1, A18, A33, A34, FUNCT_3:50;

assume A35: f . x = f . y ; :: thesis: x = y

A36: g . y9 = Class ((equivalence_wrt <.a.)),y9) by A1;

A37: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

A38: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A39: g . x9 = Class ((equivalence_wrt <.a.)),x9) by A1;

A40: f . y = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A41: f . x = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

then A42: g . x = g . y by A40, A35, XTUPLE_0:1;

then A43: y9 "\/" (y9 <=> a) [= x9 "\/" (x9 <=> a) by A39, A36, Th60;

x9 "\/" (x9 <=> a) [= y9 "\/" (y9 <=> a) by A39, A36, A42, Th60;

then A44: y9 "\/" (y9 <=> a) = x9 "\/" (x9 <=> a) by A43, LATTICES:8;

h . x = h . y by A41, A40, A35, XTUPLE_0:1;

hence x = y by A38, A37, A44, Th52; :: thesis: verum

A45: the carrier of (latt <.a.)) = <.a.) by FILTER_0:49;

thus ( [x,y] in LattRel B implies ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) :: thesis: ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )

proof

assume that
assume A46:
[x,y] in LattRel B
; :: thesis: ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] )

then reconsider x9 = x, y9 = y as Element of B by A17, RELAT_1:15;

A47: x9 [= y9 by A46, Th31;

thus ( x in field (LattRel B) & y in field (LattRel B) ) by A46, RELAT_1:15; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]

A48: Top B in <.a.) by FILTER_0:11;

x9 "/\" (Top B) = x9 ;

then Top B [= x9 => y9 by A47, FILTER_0:def 7;

then x9 => y9 in <.a.) by A48;

then A49: x9 /\/ <.a.) [= y9 /\/ <.a.) by Th16;

A50: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A51: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;

A52: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;

A53: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;

A54: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;

then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A45, A50, A54, A51, Lm4;

A55: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;

x9 "\/" a [= y9 "\/" a by A47, FILTER_0:1;

then hx [= hy by A50, A54, A53, A52, FILTER_0:51;

then A56: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A49, Th36;

A57: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;

A58: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;

A59: f . y9 = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A60: f . x9 = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;

hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] by A55, A57, A58, A60, A59, A56; :: thesis: verum

end;then reconsider x9 = x, y9 = y as Element of B by A17, RELAT_1:15;

A47: x9 [= y9 by A46, Th31;

thus ( x in field (LattRel B) & y in field (LattRel B) ) by A46, RELAT_1:15; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]

A48: Top B in <.a.) by FILTER_0:11;

x9 "/\" (Top B) = x9 ;

then Top B [= x9 => y9 by A47, FILTER_0:def 7;

then x9 => y9 in <.a.) by A48;

then A49: x9 /\/ <.a.) [= y9 /\/ <.a.) by Th16;

A50: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A51: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;

A52: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;

A53: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;

A54: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;

then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A45, A50, A54, A51, Lm4;

A55: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;

x9 "\/" a [= y9 "\/" a by A47, FILTER_0:1;

then hx [= hy by A50, A54, A53, A52, FILTER_0:51;

then A56: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A49, Th36;

A57: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;

A58: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;

A59: f . y9 = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A60: f . x9 = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;

hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] by A55, A57, A58, A60, A59, A56; :: thesis: verum

A61: x in field (LattRel B) and

A62: y in field (LattRel B) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )

reconsider x9 = x, y9 = y as Element of B by A61, A62, Th32;

A63: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;

A64: f . y9 = [(g . y9),(h . y9)] by A17, A19, FUNCT_3:def 7;

A65: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;

A66: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;

A67: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;

A68: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;

A69: y9 "/\" x9 [= y9 by LATTICES:6;

A70: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;

A71: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;

x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;

then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A45, A63, A71, A70, Lm4;

assume A72: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; :: thesis: [x,y] in LattRel B

A73: f . x9 = [(g . x9),(h . x9)] by A17, A19, FUNCT_3:def 7;

A74: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;

x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;

then A75: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A65, A66, A74, A73, A64, A72, Th31;

then x9 /\/ <.a.) [= y9 /\/ <.a.) by Th36;

then A76: x9 => y9 in <.a.) by Th16;

x9 => y9 = (x9 `) "\/" y9 by FILTER_0:42;

then a [= (x9 `) "\/" y9 by A76, FILTER_0:15;

then A77: x9 "/\" a [= x9 "/\" ((x9 `) "\/" y9) by LATTICES:9;

hx [= hy by A75, Th36;

then x9 "\/" a [= y9 "\/" a by A63, A71, A68, A67, FILTER_0:51;

then A78: x9 "/\" (x9 "\/" a) [= x9 "/\" (y9 "\/" a) by LATTICES:9;

A79: x9 "/\" (x9 `) = Bottom B by LATTICES:20;

x9 "/\" ((x9 `) "\/" y9) = (x9 "/\" (x9 `)) "\/" (x9 "/\" y9) by LATTICES:def 11;

then x9 "/\" a [= y9 by A77, A79, A69, LATTICES:7;

then A80: (x9 "/\" y9) "\/" (x9 "/\" a) [= y9 by A69, FILTER_0:6;

x9 [= x9 "\/" a by LATTICES:5;

then x9 "/\" (x9 "\/" a) = x9 by LATTICES:4;

then x9 [= (x9 "/\" y9) "\/" (x9 "/\" a) by A78, LATTICES:def 11;

then x9 [= y9 by A80, LATTICES:7;

hence [x,y] in LattRel B ; :: thesis: verum