let N be finite LATTICE; :: thesis: N, InclPoset (Ids N) are_isomorphic
set I = InclPoset (Ids N);
take i = IdsMap N; :: according to WAYBEL_1:def 8 :: thesis: i is V223(N, InclPoset (Ids N))
( not N is empty & not InclPoset (Ids N) is empty implies ( i is V13() & i is monotone & ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone ) ) )
proof
assume that
not N is empty and
not InclPoset (Ids N) is empty ; :: thesis: ( i is V13() & i is monotone & ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone ) )
thus ( i is V13() & i is monotone ) ; :: thesis: ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone )
take s = SupMap N; :: thesis: ( s = i " & s is monotone )
[i,s] is Galois by WAYBEL_1:57;
then i is onto by WAYBEL_1:24;
then A1: rng i = the carrier of (InclPoset (Ids N)) by FUNCT_2:def 3;
A2: for y, x being object holds
( y in rng i & x = s . y iff ( x in dom i & y = i . x ) )
proof
let y, x be object ; :: thesis: ( y in rng i & x = s . y iff ( x in dom i & y = i . x ) )
A3: dom i = the carrier of N by FUNCT_2:def 1;
hereby :: thesis: ( x in dom i & y = i . x implies ( y in rng i & x = s . y ) )
assume that
A4: y in rng i and
A5: x = s . y ; :: thesis: ( x in dom i & i . x = y )
reconsider Y = y as Element of (InclPoset (Ids N)) by A4;
x = s . Y by A5;
hence x in dom i by A3; :: thesis: i . x = y
reconsider Y1 = Y as Ideal of N by YELLOW_2:41;
thus i . x = i . (sup Y1) by A5, YELLOW_2:def 3
.= downarrow (sup Y1) by YELLOW_2:def 4
.= y by WAYBEL14:5, WAYBEL_3:16 ; :: thesis: verum
end;
assume that
A6: x in dom i and
A7: y = i . x ; :: thesis: ( y in rng i & x = s . y )
reconsider X = x as Element of N by A6;
A8: y = i . X by A7;
then reconsider Y = y as Ideal of N by YELLOW_2:41;
thus y in rng i by A1, A8; :: thesis: x = s . y
thus s . y = sup Y by YELLOW_2:def 3
.= sup (downarrow X) by A7, YELLOW_2:def 4
.= x by WAYBEL_0:34 ; :: thesis: verum
end;
dom s = the carrier of (InclPoset (Ids N)) by FUNCT_2:def 1;
hence s = i " by A1, A2, FUNCT_1:32; :: thesis: s is monotone
thus s is monotone ; :: thesis: verum
end;
hence i is V223(N, InclPoset (Ids N)) by WAYBEL_0:def 38; :: thesis: verum