let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st f . a [= a holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

let a be Element of L; :: thesis: ( f . a [= a implies ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f ) )

set cL = the carrier of L;

set ccL = card the carrier of L;

set nccL = nextcard (card the carrier of L);

deffunc H_{1}( Ordinal) -> Element of L = (f,$1) -. a;

consider Ls being Sequence such that

A1: ( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds

Ls . O2 = H_{1}(O2) ) )
from ORDINAL2:sch 2();

assume A2: f . a [= a ; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

A15: O in nextcard (card the carrier of L) and

A16: (f,O) -. a is_a_fixpoint_of f ;

take O ; :: thesis: ( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

card O in nextcard (card the carrier of L) by A15, CARD_1:9;

hence card O c= card the carrier of L by CARD_3:91; :: thesis: (f,O) -. a is_a_fixpoint_of f

thus (f,O) -. a is_a_fixpoint_of f by A16; :: thesis: verum

for a being Element of L st f . a [= a holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

let a be Element of L; :: thesis: ( f . a [= a implies ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f ) )

set cL = the carrier of L;

set ccL = card the carrier of L;

set nccL = nextcard (card the carrier of L);

deffunc H

consider Ls being Sequence such that

A1: ( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds

Ls . O2 = H

assume A2: f . a [= a ; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

now :: thesis: ex O being Ordinal st

( O in nextcard (card the carrier of L) & (f,O) -. a is_a_fixpoint_of f )

then consider O being Ordinal such that ( O in nextcard (card the carrier of L) & (f,O) -. a is_a_fixpoint_of f )

assume A3:
for O being Ordinal st O in nextcard (card the carrier of L) holds

not (f,O) -. a is_a_fixpoint_of f ; :: thesis: contradiction

A4: Ls is one-to-one

then A14: nextcard (card the carrier of L) c= card the carrier of L ;

card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;

hence contradiction by A14, CARD_1:4; :: thesis: verum

end;not (f,O) -. a is_a_fixpoint_of f ; :: thesis: contradiction

A4: Ls is one-to-one

proof

rng Ls c= the carrier of L
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom Ls or not x2 in dom Ls or not Ls . x1 = Ls . x2 or x1 = x2 )

assume that

A5: x1 in dom Ls and

A6: x2 in dom Ls and

A7: Ls . x1 = Ls . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;

A8: Ls . x1 = (f,x1) -. a by A1, A5;

A9: Ls . x2 = (f,x2) -. a by A1, A6;

end;assume that

A5: x1 in dom Ls and

A6: x2 in dom Ls and

A7: Ls . x1 = Ls . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;

A8: Ls . x1 = (f,x1) -. a by A1, A5;

A9: Ls . x2 = (f,x2) -. a by A1, A6;

per cases
( x1 c< x2 or x2 c< x1 or x2 = x1 )
by Lm1;

end;

suppose A10:
x1 c< x2
; :: thesis: x1 = x2

not (f,x2) -. a is_a_fixpoint_of f
by A1, A3, A6;

hence x1 = x2 by A2, A1, A6, A7, A8, A10, Th27; :: thesis: verum

end;hence x1 = x2 by A2, A1, A6, A7, A8, A10, Th27; :: thesis: verum

proof

then
card (nextcard (card the carrier of L)) c= card the carrier of L
by A1, A4, CARD_1:10;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng Ls or y in the carrier of L )

assume y in rng Ls ; :: thesis: y in the carrier of L

then consider x being object such that

A12: x in dom Ls and

A13: Ls . x = y by FUNCT_1:def 3;

reconsider x = x as Ordinal by A12;

Ls . x = (f,x) -. a by A1, A12;

hence y in the carrier of L by A13; :: thesis: verum

end;assume y in rng Ls ; :: thesis: y in the carrier of L

then consider x being object such that

A12: x in dom Ls and

A13: Ls . x = y by FUNCT_1:def 3;

reconsider x = x as Ordinal by A12;

Ls . x = (f,x) -. a by A1, A12;

hence y in the carrier of L by A13; :: thesis: verum

then A14: nextcard (card the carrier of L) c= card the carrier of L ;

card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;

hence contradiction by A14, CARD_1:4; :: thesis: verum

A15: O in nextcard (card the carrier of L) and

A16: (f,O) -. a is_a_fixpoint_of f ;

take O ; :: thesis: ( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

card O in nextcard (card the carrier of L) by A15, CARD_1:9;

hence card O c= card the carrier of L by CARD_3:91; :: thesis: (f,O) -. a is_a_fixpoint_of f

thus (f,O) -. a is_a_fixpoint_of f by A16; :: thesis: verum