let i, I be set ; for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let M be ManySortedSet of I; for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let f be Function; for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let P be MSSetOp of M; ( P is monotonic & i in I & f = P . i implies for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y )
assume that
A1:
P is monotonic
and
A2:
i in I
and
A3:
f = P . i
; for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let x, y be Element of bool (M . i); ( x c= y implies f . x c= f . y )
assume A4:
x c= y
; f . x c= f . y
dom ((EmptyMS I) +* (i .--> y)) = I
by A2, PZFMISC1:1;
then reconsider Y = (EmptyMS I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
dom ((EmptyMS I) +* (i .--> x)) = I
by A2, PZFMISC1:1;
then reconsider X = (EmptyMS I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A5:
i in {i}
by TARSKI:def 1;
dom (i .--> y) = {i}
;
then A6: Y . i =
(i .--> y) . i
by A5, FUNCT_4:13
.=
y
by FUNCOP_1:72
;
dom (i .--> x) = {i}
;
then A8: X . i =
(i .--> x) . i
by A5, FUNCT_4:13
.=
x
by FUNCOP_1:72
;
A9:
X c= Y
A11:
i in dom P
by A2, PARTFUN1:def 2;
( X is Element of bool M & Y is Element of bool M )
by Lm2, MSSUBFAM:11;
then
P .. X c= P .. Y
by A1, A9;
then A12:
(P .. X) . i c= (P .. Y) . i
by A2;
i in dom Y
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom Y)
by A11, XBOOLE_0:def 4;
then
i in dom (P .. Y)
by PRALG_1:def 19;
then W:
(P .. Y) . i = f . (Y . i)
by PRALG_1:def 19, A3;
dom X = I
by PARTFUN1:def 2;
then
i in dom X
by A2;
then
i in (dom P) /\ (dom X)
by A11, XBOOLE_0:def 4;
then
i in dom (P .. X)
by PRALG_1:def 19;
then
f . (X . i) = (P .. X) . i
by A3, PRALG_1:def 19;
then
f . (X . i) c= (P .. Y) . i
by A12;
hence
f . x c= f . y
by A8, A6, W; verum