let P be non empty strict chain-complete Poset; :: thesis: for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
let G be non empty Chain of (ConPoset (P,P)); :: thesis: (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
reconsider h = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm27;
h . (sup G) <= sup (h .: G)
proof
reconsider L = h .: G as non empty Chain of P by Th1;
set g0 = sup G;
set p0 = h . (sup G);
reconsider G0 = sup G as continuous Function of P,P by Lm24;
A1: h . (sup G) = least_fix_point G0 by Def12;
A2: sup G = sup_func G by Th11;
then reconsider g0 = sup G as continuous Function of P,P ;
set a = Bottom P;
reconsider I0 = iterSet (g0,(Bottom P)) as non empty Chain of P by Th3;
A3: h . (sup G) = sup (iter_min g0) by Th9, A1
.= sup I0 ;
A4: ex_sup_of I0,P by Def1;
for x being Element of P st x in I0 holds
x <= sup L
proof
let x be Element of P; :: thesis: ( x in I0 implies x <= sup L )
assume x in I0 ; :: thesis: x <= sup L
then consider y being Element of P such that
A5: ( x = y & ex n being Nat st y = (iter (g0,n)) . (Bottom P) ) ;
consider n0 being Nat such that
A6: x = (iter (g0,n0)) . (Bottom P) by A5;
set M0 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n0)) . (Bottom P) ) } ;
reconsider M0 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n0)) . (Bottom P) ) } as non empty Chain of P by Lm32;
for p being Element of P st p in M0 holds
p <= sup L
proof
let p be Element of P; :: thesis: ( p in M0 implies p <= sup L )
assume p in M0 ; :: thesis: p <= sup L
then consider p0 being Element of P, g being continuous Function of P,P such that
A7: ( p = p0 & g in G & p0 = (iter (g,n0)) . (Bottom P) ) by Lm28;
set r = h . g;
h . g in L by A7, Lm33;
then reconsider r = h . g as Element of P ;
A8: r <= sup L by Lm18, A7, Lm33;
p <= r by A7, Lm34;
hence p <= sup L by A8, ORDERS_2:3; :: thesis: verum
end;
then A9: sup M0 <= sup L by Lm19;
defpred S1[ Nat] means for z being Element of P
for M being non empty Chain of P st z = (iter (g0,$1)) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,$1)) . (Bottom P) ) } holds
z <= sup M;
A10: S1[ 0 ]
proof
let z be Element of P; :: thesis: for M being non empty Chain of P st z = (iter (g0,0)) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) ) } holds
z <= sup M
let M be non empty Chain of P; :: thesis: ( z = (iter (g0,0)) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) ) } implies z <= sup M )
assume z = (iter (g0,0)) . (Bottom P) ; :: thesis: ( not M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) ) } or z <= sup M )
then z = Bottom P by Lm1;
hence ( not M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) ) } or z <= sup M ) by YELLOW_0:44; :: thesis: verum
end;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; :: thesis: S1[k + 1]
for z1 being Element of P
for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) ) } holds
z1 <= sup M1
proof
let z1 be Element of P; :: thesis: for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) ) } holds
z1 <= sup M1
let M1 be non empty Chain of P; :: thesis: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) ) } implies z1 <= sup M1 )
assume A13: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) ) } ) ; :: thesis: z1 <= sup M1
reconsider z = (iter (g0,k)) . (Bottom P) as Element of P ;
A14: z1 = (g0 * (iter (g0,k))) . (Bottom P) by A13, FUNCT_7:71
.= g0 . z by Lm2 ;
reconsider M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,k)) . (Bottom P) ) } as non empty Chain of P by Lm32;
reconsider M0 = g0 .: M as non empty Chain of P by Th1;
A15: g0 . (sup M) = sup M0 by Th6;
A16: ex_sup_of M0,P by Def1;
for q being Element of P st q in M0 holds
q <= sup M1
proof
let q be Element of P; :: thesis: ( q in M0 implies q <= sup M1 )
assume q in M0 ; :: thesis: q <= sup M1
then consider g being continuous Function of P,P such that
A17: ( g in G & q = g0 . ((iter (g,k)) . (Bottom P)) ) by Lm35;
reconsider a1 = (iter (g,k)) . (Bottom P) as Element of P ;
reconsider W = G -image a1 as non empty Chain of P ;
A18: q = sup W by A17, Def10, A2;
A19: ex_sup_of W,P by Def1;
for q1 being Element of P st q1 in W holds
q1 <= sup M1
proof
let q1 be Element of P; :: thesis: ( q1 in W implies q1 <= sup M1 )
assume q1 in W ; :: thesis: q1 <= sup M1
then consider q2 being Element of P such that
A20: ( q1 = q2 & ex g1 being continuous Function of P,P st
( g1 in G & q2 = g1 . a1 ) ) ;
consider g1 being continuous Function of P,P such that
A21: ( g1 in G & q1 = g1 . a1 ) by A20;
per cases ( g1 <= g or g <= g1 ) by A17, A21, Lm31;
suppose g1 <= g ; :: thesis: q1 <= sup M1
then A22: q1 <= g . a1 by A21, YELLOW_2:9;
set a2 = g . a1;
reconsider g2 = g as Element of (ConPoset (P,P)) by Lm25;
reconsider gg = g2 as continuous Function of P,P ;
g . a1 = (g * (iter (g,k))) . (Bottom P) by Lm2
.= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ;
then g . a1 in M1 by A13, A17;
then g . a1 <= sup M1 by Lm18;
hence q1 <= sup M1 by A22, ORDERS_2:3; :: thesis: verum
end;
suppose A23: g <= g1 ; :: thesis: q1 <= sup M1
reconsider a2 = (iter (g1,k)) . (Bottom P) as Element of P ;
a1 <= a2 by A23, Lm7;
then A24: q1 <= g1 . a2 by A21, ORDERS_3:def 5;
set a3 = g1 . a2;
reconsider g2 = g1 as Element of (ConPoset (P,P)) by Lm25;
reconsider gg = g2 as continuous Function of P,P ;
g1 . a2 = (g1 * (iter (g1,k))) . (Bottom P) by Lm2
.= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ;
then g1 . a2 in M1 by A13, A21;
then g1 . a2 <= sup M1 by Lm18;
hence q1 <= sup M1 by A24, ORDERS_2:3; :: thesis: verum
end;
end;
end;
then W is_<=_than sup M1 ;
hence q <= sup M1 by A18, A19, YELLOW_0:def 9; :: thesis: verum
end;
then M0 is_<=_than sup M1 ;
then A25: sup M0 <= sup M1 by A16, YELLOW_0:def 9;
z <= sup M by A12;
then z1 <= sup M0 by A14, A15, ORDERS_3:def 5;
hence z1 <= sup M1 by A25, ORDERS_2:3; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A10, A11);
 then x <= sup M0 by A6;
hence x <= sup L by A9, ORDERS_2:3; :: thesis: verum
end;
then I0 is_<=_than sup L ;
hence h . (sup G) <= sup (h .: G) by A3, A4, YELLOW_0:def 9; :: thesis: verum
end;
hence (fix_func P) . (sup G) <= sup ((fix_func P) .: G) ; :: thesis: verum