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₃( set ) -> 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 set st x in the carrier of B holds
g . x = H₃(x) ) ) from FUNCT_1:sch 3();
A2: for b being Element of B holds (b "\/" (b <=> a)) <=> b = b "\/" a

proof

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: (Bottom B) "/\" (a `) = Bottom B by LATTICES:15;
A6: b "\/" ((b "/\" a) "\/" ((b `) "/\" (a `))) = (b "\/" (b "/\" a)) "\/" ((b `) "/\" (a `)) by LATTICES:def 5;
A7: (Bottom B) "\/" ((b `) "/\" a) = (b `) "/\" a by LATTICES:14;
A8: b <=> a = (b "/\" a) "\/" ((b `) "/\" (a `)) by Th51;
A9: (b `) "/\" b = Bottom B by LATTICES:20;
A10: b "/\" b = b by LATTICES:2;
A11: (b `) "/\" ((a `) "/\" b) = ((b `) "/\" (a `)) "/\" b by LATTICES:def 7;
A12: b "\/" (Bottom B) = b by LATTICES:14;
A13: (b `) "/\" (b `) = b ` by LATTICES:2;
A14: (b `) "/\" ((b `) "/\" a) = ((b `) "/\" (b `)) "/\" a by LATTICES:def 7;
A15: (b <=> a) ` = (b "/\" (a `)) "\/" ((b `) "/\" a) by Th52;
A16: (b `) "/\" (b "/\" (a `)) = ((b `) "/\" b) "/\" (a `) by LATTICES:def 7;
A17: (b "\/" ((b `) "/\" (a `))) "/\" b = (b "/\" b) "\/" (((b `) "/\" (a `)) "/\" b) by LATTICES:def 11;
A18: (b "/\" a) "\/" b = b by LATTICES:def 8;
(b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) `) "/\" (b `)) by Th51;
hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b `) "/\" a)) by A3, A15, A4, A16, A9, A14, A13, A5, A7, A8, A6, A18, A17, A11, A10, A12, LATTICES:def 5
.= b "\/" ((b "\/" (b `)) "/\" a) by LATTICES:def 11
.= b "\/" ((Top B) "/\" a) by LATTICES:21
.= b "\/" a by LATTICES:17 ;
:: thesis: verum

end;

set S = LattRel [:(B /\/ <.a.)),(latt <.a.)):];
A19: field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] by Th33;
reconsider o1 = H₁(B), o2 = H₂(B) as BinOp of equivalence_wrt <.a.) by Th13, Th14;
A20: LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) by Def5;
set R = LattRel B;
deffunc H₄( Element of B) -> Element of the carrier of B = ($1 "\/" ($1 <=> a)) <=> $1;
consider h being UnOp of the carrier of B such that
A21: for b being Element of B holds h . b = H₄(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.)):]
A22: field (LattRel B) = the carrier of B by Th33;
A23: dom h = dom g by A1, FUNCT_2:def 1;
hence A24: dom f = field (LattRel B) by A1, A22, FUNCT_3:50; :: according to WELLORD1:def 7 :: thesis: ( proj2 f = field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) & f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )
A25: for b being Element of B holds h . b is Element of (latt <.a.))

proof

let b be Element of B; :: thesis: h . b is Element of (latt <.a.))
b "\/" (b <=> a) in Class ((equivalence_wrt <.a.)),b) by Th61;
then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:19;
then A26: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def 11;
h . b = (b "\/" (b <=> a)) <=> b by A21;
hence h . b is Element of (latt <.a.)) by A26, FILTER_0:49; :: thesis: verum

end;

thus rng f c= field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= proj2 f & f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )

proof

let x be set ; :: 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 set such that
A27: y in dom f and
A28: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of B by A1, A23, A27, FUNCT_3:50;
reconsider z2 = h . y as Element of (latt <.a.)) by A25;
g . y = EqClass ((equivalence_wrt <.a.)),y) by A1;
then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A20;
x = [z1,z2] by A27, A28, FUNCT_3:def 7;
hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A19; :: thesis: verum

end;

A29: the carrier of (latt <.a.)) = <.a.) by FILTER_0:49;
thus field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f :: thesis: ( f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )

proof

let x be set ; :: 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
A30: x = [y,z] by A19, A29, A20, DOMAIN_1:1;
consider b being Element of B such that
A31: y = Class ((equivalence_wrt <.a.)),b) by EQREL_1:36;
set ty = b "\/" (b <=> a);
(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th54;
then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;
then A32: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 11;
b "\/" (b <=> a) in y by A31, Th61;
then y = Class ((equivalence_wrt <.a.)),(b "\/" (b <=> a))) by A31, EQREL_1:23;
then A33: (b "\/" (b <=> a)) <=> z in y by A32, EQREL_1:19;
then A34: y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A31, EQREL_1:23;
then A35: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by A31, Th61;
y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A31, A33, EQREL_1:23;
then A36: g . ((b "\/" (b <=> a)) <=> z) = y by A1;
((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by A31, A34, Th61;
then A37: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by A35, LATTICES:8;
h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A21;
then h . ((b "\/" (b <=> a)) <=> z) = z by A37, Th54;
then x = f . ((b "\/" (b <=> a)) <=> z) by A22, A24, A30, A36, FUNCT_3:def 7;
hence x in rng f by A22, A24, FUNCT_1:def 3; :: thesis: verum

end;

thus f is one-to-one :: thesis: for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) )

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A38: x in dom f and
A39: y in dom f ; :: thesis: ( not f . x = f . y or x = y )
reconsider x9 = x, y9 = y as Element of B by A1, A23, A38, A39, FUNCT_3:50;
assume A40: f . x = f . y ; :: thesis: x = y
A41: g . y9 = Class ((equivalence_wrt <.a.)),y9) by A1;
A42: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
A43: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A44: g . x9 = Class ((equivalence_wrt <.a.)),x9) by A1;
A45: f . y = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def 7;
A46: f . x = [(g . x9),(h . x9)] by A22, A24, FUNCT_3:def 7;
then A47: g . x = g . y by A45, A40, ZFMISC_1:27;
then A48: y9 "\/" (y9 <=> a) [= x9 "\/" (x9 <=> a) by A44, A41, Th61;
x9 "\/" (x9 <=> a) [= y9 "\/" (y9 <=> a) by A44, A41, A47, Th61;
then A49: y9 "\/" (y9 <=> a) = x9 "\/" (x9 <=> a) by A48, LATTICES:8;
h . x = h . y by A46, A45, A40, ZFMISC_1:27;
hence x = y by A43, A42, A49, Th53; :: thesis: verum

end;

let x, y be set ; :: 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 ) )
A50: 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 A51: [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 A22, RELAT_1:15;
A52: x9 [= y9 by A51, Th32;
thus ( x in field (LattRel B) & y in field (LattRel B) ) by A51, RELAT_1:15; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]
A53: Top B in <.a.) by FILTER_0:11;
x9 "/\" (Top B) = x9 by LATTICES:17;
then Top B [= x9 => y9 by A52, FILTER_0:def 7;
then x9 => y9 in <.a.) by A53, FILTER_0:9;
then A54: x9 /\/ <.a.) [= y9 /\/ <.a.) by Th16;
A55: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A56: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th61;
A57: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A58: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A59: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th61;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A50, A55, A59, A56, Lm4;
A60: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;
x9 "\/" a [= y9 "\/" a by A52, FILTER_0:1;
then hx [= hy by A55, A59, A58, A57, FILTER_0:51;
then A61: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A54, Th37;
A62: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;
A63: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;
A64: f . y9 = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def 7;
A65: f . x9 = [(g . x9),(h . x9)] by A22, A24, 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 A60, A62, A63, A65, A64, A61; :: thesis: verum

end;

assume that
A66: x in field (LattRel B) and
A67: 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 A66, A67, Th33;
A68: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A69: f . y9 = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def 7;
A70: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;
A71: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;
A72: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A73: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A74: y9 "/\" x9 [= y9 by LATTICES:6;
A75: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th61;
A76: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th61;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A50, A68, A76, A75, Lm4;
assume A77: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; :: thesis: [x,y] in LattRel B
A78: f . x9 = [(g . x9),(h . x9)] by A22, A24, FUNCT_3:def 7;
A79: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;
x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;
then A80: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A70, A71, A79, A78, A69, A77, Th32;
then x9 /\/ <.a.) [= y9 /\/ <.a.) by Th37;
then A81: x9 => y9 in <.a.) by Th16;
x9 => y9 = (x9 `) "\/" y9 by FILTER_0:42;
then a [= (x9 `) "\/" y9 by A81, FILTER_0:15;
then A82: x9 "/\" a [= x9 "/\" ((x9 `) "\/" y9) by LATTICES:9;
A83: (Bottom B) "\/" (x9 "/\" y9) = x9 "/\" y9 by LATTICES:14;
hx [= hy by A80, Th37;
then x9 "\/" a [= y9 "\/" a by A68, A76, A73, A72, FILTER_0:51;
then A84: x9 "/\" (x9 "\/" a) [= x9 "/\" (y9 "\/" a) by LATTICES:9;
A85: x9 "/\" (x9 `) = Bottom B by LATTICES:20;
x9 "/\" ((x9 `) "\/" y9) = (x9 "/\" (x9 `)) "\/" (x9 "/\" y9) by LATTICES:def 11;
then x9 "/\" a [= y9 by A82, A85, A83, A74, LATTICES:7;
then A86: (x9 "/\" y9) "\/" (x9 "/\" a) [= y9 by A74, FILTER_0:6;
x9 [= x9 "\/" a by LATTICES:5;
then x9 "/\" (x9 "\/" a) = x9 by LATTICES:4;
then x9 [= (x9 "/\" y9) "\/" (x9 "/\" a) by A84, LATTICES:def 11;
then x9 [= y9 by A86, LATTICES:7;
hence [x,y] in LattRel B ; :: thesis: verum