let S1 be OrderSortedSign; :: thesis: for U1 being non-empty monotone OSAlgebra of S1
for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U1 be non-empty monotone OSAlgebra of S1; :: thesis: for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is order-sorted & F is_homomorphism U1,U2 implies ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 ) )
assume A1:
( F is order-sorted & F is_homomorphism U1,U2 )
; :: thesis: ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
reconsider O1 = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
F .:.: O1 is OrderSortedSet of
by A1, Th8;
then A2:
the Sorts of (Image F) is OrderSortedSet of
by A1, MSUALG_3:def 14;
hence
Image F is order-sorted
by OSALG_1:17; :: thesis: Image F is monotone OSAlgebra of S1
reconsider I = Image F as non-empty OSAlgebra of S1 by A2, OSALG_1:17;
consider G being ManySortedFunction of U1,I such that
A3:
( F = G & G is_epimorphism U1,I )
by A1, MSUALG_3:21;
A4:
( G is "onto" & G is order-sorted & G is_homomorphism U1,I )
by A1, A3, MSUALG_3:def 10;
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
Den o1,I c= Den o2,I
proof
let o1,
o2 be
OperSymbol of
S1;
:: thesis: ( o1 <= o2 implies Den o1,I c= Den o2,I )
assume A5:
o1 <= o2
;
:: thesis: Den o1,I c= Den o2,I
A6:
(
the_arity_of o1 <= the_arity_of o2 &
the_result_sort_of o1 <= the_result_sort_of o2 )
by A5, OSALG_1:def 22;
A7:
(
Args o1,
I c= Args o2,
I &
Result o1,
I c= Result o2,
I )
by A5, OSALG_1:26;
A8:
(
Args o1,
U1 c= Args o2,
U1 &
Result o1,
U1 c= Result o2,
U1 )
by A5, OSALG_1:26;
A9:
(
dom (Den o1,I) = Args o1,
I &
dom (Den o2,I) = Args o2,
I )
by FUNCT_2:def 1;
A10:
(Den o2,U1) | (Args o1,U1) = Den o1,
U1
by A5, OSALG_1:def 23;
for
a,
b being
set st
[a,b] in Den o1,
I holds
[a,b] in Den o2,
I
proof
set s1 =
the_result_sort_of o1;
set s2 =
the_result_sort_of o2;
let a,
b be
set ;
:: thesis: ( [a,b] in Den o1,I implies [a,b] in Den o2,I )
assume A11:
[a,b] in Den o1,
I
;
:: thesis: [a,b] in Den o2,I
A12:
(
a in Args o1,
I &
b in Result o1,
I )
by A11, ZFMISC_1:106;
then consider y being
Element of
Args o1,
U1 such that A13:
G # y = a
by A4, MSUALG_9:18;
set x =
(Den o1,U1) . y;
o1 in the
carrier' of
S1
;
then A14:
o1 in dom the
ResultSort of
S1
by FUNCT_2:def 1;
A15:
Result o1,
U1 =
(O1 * the ResultSort of S1) . o1
by MSUALG_1:def 10
.=
O1 . (the ResultSort of S1 . o1)
by A14, FUNCT_1:23
.=
O1 . (the_result_sort_of o1)
by MSUALG_1:def 7
.=
dom (G . (the_result_sort_of o1))
by FUNCT_2:def 1
;
(G . (the_result_sort_of o1)) . ((Den o1,U1) . y) = (Den o1,I) . a
by A4, A13, MSUALG_3:def 9;
then A16:
b = (G . (the_result_sort_of o1)) . ((Den o1,U1) . y)
by A11, FUNCT_1:8;
A17:
(
(Den o1,U1) . y in dom (G . (the_result_sort_of o2)) &
(G . (the_result_sort_of o1)) . ((Den o1,U1) . y) = (G . (the_result_sort_of o2)) . ((Den o1,U1) . y) )
by A1, A3, A6, A15, Def1;
reconsider y1 =
y as
Element of
Args o2,
U1 by A8, TARSKI:def 3;
A18:
G # y1 = G # y
by A1, A3, A5, Th13;
(Den o2,U1) . y = (Den o1,U1) . y
by A10, FUNCT_1:72;
then
b = (Den o2,I) . a
by A4, A13, A16, A17, A18, MSUALG_3:def 9;
hence
[a,b] in Den o2,
I
by A7, A9, A12, FUNCT_1:8;
:: thesis: verum
end;
hence
Den o1,
I c= Den o2,
I
by RELAT_1:def 3;
:: thesis: verum
end;
hence
Image F is monotone OSAlgebra of S1
by OSALG_1:27; :: thesis: verum