let L, M be complete continuous LATTICE; for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds
L,M are_isomorphic
let Lg, Mg be set ; ( Lg is_FreeGen_set_of L & Mg is_FreeGen_set_of M & card Lg = card Mg implies L,M are_isomorphic )
assume that
A1:
Lg is_FreeGen_set_of L
and
A2:
Mg is_FreeGen_set_of M
and
A3:
card Lg = card Mg
; L,M are_isomorphic
Lg,Mg are_equipotent
by A3, CARD_1:5;
then consider f being Function such that
A4:
f is one-to-one
and
A5:
dom f = Lg
and
A6:
rng f = Mg
;
set g = f " ;
A7:
dom (f ") = Mg
by A4, A6, FUNCT_1:33;
reconsider Mg = Mg as Subset of M by A2, Th7;
A8:
rng (f ") = Lg
by A4, A5, FUNCT_1:33;
reconsider Lg = Lg as Subset of L by A1, Th7;
Mg c= the carrier of M
;
then reconsider f = f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def 1, RELSET_1:4;
consider F being CLHomomorphism of L,M such that
A9:
F | Lg = f
and
for h9 being CLHomomorphism of L,M st h9 | Lg = f holds
h9 = F
by A1;
Lg c= the carrier of L
;
then reconsider g = f " as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def 1, RELSET_1:4;
consider G being CLHomomorphism of M,L such that
A10:
G | Mg = g
and
for h9 being CLHomomorphism of M,L st h9 | Mg = g holds
h9 = G
by A2;
reconsider GF = G * F as CLHomomorphism of L,L by Th2;
GF | Lg =
G * f
by A9, RELAT_1:83
.=
g * f
by A6, A10, FUNCT_4:2
.=
id Lg
by A4, A5, FUNCT_1:39
;
then A11:
GF = id L
by A1, Th8;
then A12:
F is one-to-one
by FUNCT_2:23;
reconsider FG = F * G as CLHomomorphism of M,M by Th2;
F is directed-sups-preserving
by WAYBEL16:def 1;
then A13:
F is monotone
by WAYBEL17:3;
G is directed-sups-preserving
by WAYBEL16:def 1;
then A14:
G is monotone
by WAYBEL17:3;
FG | Mg =
F * g
by A10, RELAT_1:83
.=
f * g
by A8, A9, FUNCT_4:2
.=
id Mg
by A4, A6, FUNCT_1:39
;
then
FG = id M
by A2, Th8;
then
F is onto
by FUNCT_2:23;
then
rng F = the carrier of M
by FUNCT_2:def 3;
then
G = F "
by A11, A12, FUNCT_2:30;
then
F is isomorphic
by A12, A13, A14, WAYBEL_0:def 38;
hence
L,M are_isomorphic
by WAYBEL_1:def 8; verum