let L, M be complete continuous LATTICE; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 V13() 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; :: thesis: verum