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.);
A1: ( B is 0_Lattice & B is 1_Lattice & B is I_Lattice ) by FILTER_0:40;
deffunc H₃( set ) -> Element of bool the carrier of B = Class (equivalence_wrt <.a.)),$1;
consider g being Function such that
A2: ( 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();
A3: 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
( (b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) ` ) "/\" (b ` )) & (b "\/" (b <=> a)) ` = (b ` ) "/\" ((b <=> a) ` ) & (b <=> a) ` = (b "/\" (a ` )) "\/" ((b ` ) "/\" a) & (b ` ) "/\" ((b "/\" (a ` )) "\/" ((b ` ) "/\" a)) = ((b ` ) "/\" (b "/\" (a ` ))) "\/" ((b ` ) "/\" ((b ` ) "/\" a)) & (b ` ) "/\" (b "/\" (a ` )) = ((b ` ) "/\" b) "/\" (a ` ) & (b ` ) "/\" b = Bottom B & (b ` ) "/\" ((b ` ) "/\" a) = ((b ` ) "/\" (b ` )) "/\" a & (b ` ) "/\" (b ` ) = b ` & (Bottom B) "/\" (a ` ) = Bottom B & (Bottom B) "\/" ((b ` ) "/\" a) = (b ` ) "/\" a & (b ` ) "/\" ((b ` ) "/\" a) = ((b ` ) "/\" a) "/\" (b ` ) & b <=> a = (b "/\" a) "\/" ((b ` ) "/\" (a ` )) & b "\/" ((b "/\" a) "\/" ((b ` ) "/\" (a ` ))) = (b "\/" (b "/\" a)) "\/" ((b ` ) "/\" (a ` )) & b "\/" (b "/\" a) = (b "/\" a) "\/" b & (b "/\" a) "\/" b = b & (b "\/" ((b ` ) "/\" (a ` ))) "/\" b = (b "/\" b) "\/" (((b ` ) "/\" (a ` )) "/\" b) & (b ` ) "/\" ((a ` ) "/\" b) = ((b ` ) "/\" (a ` )) "/\" b & (a ` ) "/\" b = b "/\" (a ` ) & b "/\" b = b & b "\/" (Bottom B) = b ) by Th51, Th52, LATTICES:18, LATTICES:39, LATTICES:40, LATTICES:47, LATTICES:51, LATTICES:def 5, LATTICES:def 7, LATTICES:def 8, LATTICES:def 11;
hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b ` ) "/\" a)) by LATTICES:def 5
.= b "\/" ((b "\/" (b ` )) "/\" a) by LATTICES:def 11
.= b "\/" ((Top B) "/\" a) by LATTICES:48
.= b "\/" a by LATTICES:43 ;
:: thesis: verum

end;

A4: the carrier of (latt <.a.)) = <.a.) by FILTER_0:63;
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
A5: 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.)):]
set R = LattRel B;
set S = LattRel [:(B /\/ <.a.)),(latt <.a.)):];
A6: ( field (LattRel B) = the carrier of B & field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] ) by Th33;
A7: dom h = dom g by A2, FUNCT_2:def 1;
hence A8: dom f = field (LattRel B) by A2, A6, FUNCT_3:70; :: according to WELLORD1:def 7 :: thesis: ( rng 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 ) ) ) )
reconsider o1 = H₁(B), o2 = H₂(B) as BinOp of equivalence_wrt <.a.) by A1, Th13, Th14;
A9: ( the carrier of (latt <.a.)) = <.a.) & LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) ) by A1, Def5, FILTER_0:63;
A10: 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:27;
then ( h . b = (b "\/" (b <=> a)) <=> b & (b "\/" (b <=> a)) <=> b in <.a.) ) by A5, FILTER_0:def 12;
hence h . b is Element of (latt <.a.)) by FILTER_0:63; :: 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= rng 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
A11: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
reconsider y = y as Element of B by A2, A7, A11, FUNCT_3:70;
g . y = EqClass (equivalence_wrt <.a.)),y by A2;
then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A9;
reconsider z2 = h . y as Element of (latt <.a.)) by A10;
x = [z1,z2] by A11, FUNCT_3:def 8;
hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A6; :: thesis: verum

end;

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
A12: x = [y,z] by A6, A9, DOMAIN_1:9;
consider b being Element of B such that
A13: y = Class (equivalence_wrt <.a.)),b by EQREL_1:45;
set ty = b "\/" (b <=> a);
b "\/" (b <=> a) in y by A13, Th61;
then A14: y = Class (equivalence_wrt <.a.)),(b "\/" (b <=> a)) by A13, EQREL_1:31;
(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th54;
then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;
then [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 12;
then A15: (b "\/" (b <=> a)) <=> z in y by A14, EQREL_1:27;
then y = Class (equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z) by A13, EQREL_1:31;
then ( ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) & b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) ) by A13, Th61;
then ( h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) & ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) & y = Class (equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z) ) by A5, A13, A15, EQREL_1:31, LATTICES:26;
then ( g . ((b "\/" (b <=> a)) <=> z) = y & h . ((b "\/" (b <=> a)) <=> z) = z ) by A2, Th54;
then x = f . ((b "\/" (b <=> a)) <=> z) by A6, A8, A12, FUNCT_3:def 8;
hence x in rng f by A6, A8, FUNCT_1:def 5; :: 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 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
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 ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
then reconsider x' = x, y' = y as Element of B by A2, A7, FUNCT_3:70;
A16: ( f . x = [(g . x'),(h . x')] & f . y = [(g . y'),(h . y')] & g . x' = Class (equivalence_wrt <.a.)),x' & g . y' = Class (equivalence_wrt <.a.)),y' & h . x' = (x' "\/" (x' <=> a)) <=> x' & x' "\/" (x' <=> a) in Class (equivalence_wrt <.a.)),x' & y' "\/" (y' <=> a) in Class (equivalence_wrt <.a.)),y' & h . y' = (y' "\/" (y' <=> a)) <=> y' ) by A2, A5, A6, A8, Th61, FUNCT_3:def 8;
assume f . x = f . y ; :: thesis: x = y
then A17: ( g . x = g . y & h . x = h . y ) by A16, ZFMISC_1:33;
then ( x' "\/" (x' <=> a) [= y' "\/" (y' <=> a) & y' "\/" (y' <=> a) [= x' "\/" (x' <=> a) ) by A16, Th61;
then y' "\/" (y' <=> a) = x' "\/" (x' <=> a) by LATTICES:26;
hence x = y by A16, A17, 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 ) )
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 A18: [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.)):] )
hence ( x in field (LattRel B) & y in field (LattRel B) ) by RELAT_1:30; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]
reconsider x' = x, y' = y as Element of B by A6, A18, RELAT_1:30;
A19: ( x' [= y' & x' "/\" (Top B) = x' ) by A18, Th32, LATTICES:43;
then ( Top B [= x' => y' & Top B in <.a.) ) by A1, FILTER_0:12, FILTER_0:def 8;
then x' => y' in <.a.) by FILTER_0:9;
then A20: ( x' /\/ <.a.) [= y' /\/ <.a.) & x' /\/ <.a.) = Class (equivalence_wrt <.a.)),x' & Class (equivalence_wrt <.a.)),x' = g . x' & y' /\/ <.a.) = Class (equivalence_wrt <.a.)),y' & Class (equivalence_wrt <.a.)),y' = g . y' ) by A1, A2, Def6, Th16;
A21: ( h . x' = (x' "\/" (x' <=> a)) <=> x' & h . y' = (y' "\/" (y' <=> a)) <=> y' & f . x' = [(g . x'),(h . x')] & f . y' = [(g . y'),(h . y')] & x' "\/" a [= y' "\/" a & (x' "\/" (x' <=> a)) <=> x' = x' "\/" a & (y' "\/" (y' <=> a)) <=> y' = y' "\/" a ) by A3, A5, A6, A8, A19, FILTER_0:1, FUNCT_3:def 8;
( x' "\/" (x' <=> a) in Class (equivalence_wrt <.a.)),x' & y' "\/" (y' <=> a) in Class (equivalence_wrt <.a.)),y' ) by Th61;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A1, A4, A21, Lm4;
hx [= hy by A21, FILTER_0:65;
then [(x' /\/ <.a.)),hx] [= [(y' /\/ <.a.)),hy] by A20, Th37;
hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] by A20, A21; :: thesis: verum

end;

assume ( x in field (LattRel B) & y in field (LattRel B) ) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )
then reconsider x' = x, y' = y as Element of B by Th33;
A22: ( x' /\/ <.a.) = Class (equivalence_wrt <.a.)),x' & y' /\/ <.a.) = Class (equivalence_wrt <.a.)),y' & Class (equivalence_wrt <.a.)),x' = g . x' & Class (equivalence_wrt <.a.)),y' = g . y' & h . x' = (x' "\/" (x' <=> a)) <=> x' & h . y' = (y' "\/" (y' <=> a)) <=> y' & f . x' = [(g . x'),(h . x')] & f . y' = [(g . y'),(h . y')] & (x' "\/" (x' <=> a)) <=> x' = x' "\/" a & (y' "\/" (y' <=> a)) <=> y' = y' "\/" a ) by A1, A2, A3, A5, A6, A8, Def6, FUNCT_3:def 8;
( x' "\/" (x' <=> a) in Class (equivalence_wrt <.a.)),x' & y' "\/" (y' <=> a) in Class (equivalence_wrt <.a.)),y' ) by Th61;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A1, A4, A22, Lm4;
assume [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; :: thesis: [x,y] in LattRel B
then [(x' /\/ <.a.)),hx] [= [(y' /\/ <.a.)),hy] by A22, Th32;
then ( x' /\/ <.a.) [= y' /\/ <.a.) & hx [= hy ) by Th37;
then ( x' => y' in <.a.) & x' => y' = (x' ` ) "\/" y' & x' "\/" a [= y' "\/" a & x' [= x' "\/" a ) by A1, A22, Th16, FILTER_0:55, FILTER_0:65, LATTICES:22;
then ( a [= (x' ` ) "\/" y' & x' "/\" (x' "\/" a) [= x' "/\" (y' "\/" a) & x' "/\" (x' "\/" a) = x' ) by FILTER_0:18, LATTICES:21, LATTICES:27;
then A23: ( x' "/\" a [= x' "/\" ((x' ` ) "\/" y') & x' "/\" ((x' ` ) "\/" y') = (x' "/\" (x' ` )) "\/" (x' "/\" y') & x' "/\" (x' ` ) = Bottom B & (Bottom B) "\/" (x' "/\" y') = x' "/\" y' & x' [= (x' "/\" y') "\/" (x' "/\" a) & y' "/\" x' [= y' & y' "/\" x' = x' "/\" y' ) by LATTICES:23, LATTICES:27, LATTICES:39, LATTICES:47, LATTICES:def 11;
then x' "/\" a [= y' by LATTICES:25;
then (x' "/\" y') "\/" (x' "/\" a) [= y' by A23, FILTER_0:6;
then x' [= y' by A23, LATTICES:25;
hence [x,y] in LattRel B ; :: thesis: verum