let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
for O1, O2 being Ordinal st O1 c= O2 holds
f,O2 -. a [= f,O1 -. a
let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds
for O1, O2 being Ordinal st O1 c= O2 holds
f,O2 -. a [= f,O1 -. a
let a be Element of L; :: thesis: ( f . a [= a implies for O1, O2 being Ordinal st O1 c= O2 holds
f,O2 -. a [= f,O1 -. a )
defpred S₁[ Ordinal] means for O1, O2 being Ordinal st O1 c= O2 & O2 c= $1 holds
f,O2 -. a [= f,O1 -. a;

A1: now

let O4 be Ordinal; :: thesis: ( O4 <> {} & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds
S₁[O3] ) implies S₁[O4] )
assume that
A2: ( O4 <> {} & O4 is limit_ordinal ) and
A3: for O3 being Ordinal st O3 in O4 holds
S₁[O3] ; :: thesis: S₁[O4]
thus S₁[O4] :: thesis: verum

proof

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 & O2 c= O4 implies f,O2 -. a [= f,O1 -. a )
assume that
A4: O1 c= O2 and
A5: O2 c= O4 ; :: thesis: f,O2 -. a [= f,O1 -. a
A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) by XBOOLE_0:def 8;
A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) by XBOOLE_0:def 8;

per cases ( O2 = O4 or O2 in O4 ) by A5, A6, ORDINAL1:21;

suppose A8: O2 = O4 ; :: thesis: f,O2 -. a [= f,O1 -. a

thus f,O2 -. a [= f,O1 -. a :: thesis: verum

proof

per cases ( O1 = O2 or O1 in O2 ) by A4, A7, ORDINAL1:21;

suppose O1 = O2 ; :: thesis: f,O2 -. a [= f,O1 -. a

hence f,O2 -. a [= f,O1 -. a ; :: thesis: verum

end;

suppose A9: O1 in O2 ; :: thesis: f,O2 -. a [= f,O1 -. a

deffunc H₁( Ordinal) -> Element of L = f,$1 -. a;
consider L1 being T-Sequence such that
A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A11: ( L1 . O1 = f,O1 -. a & L1 . O1 in rng L1 ) by A9, A10, FUNCT_1:def 5;
f,O2 -. a = "/\" (rng L1),L by A2, A8, A10, Th21;
hence f,O2 -. a [= f,O1 -. a by A11, LATTICE3:38; :: thesis: verum

end;

end;

end;

end;

suppose O2 in O4 ; :: thesis: f,O2 -. a [= f,O1 -. a

hence f,O2 -. a [= f,O1 -. a by A3, A4; :: thesis: verum

end;

end;

end;

end;

assume A12: f . a [= a ; :: thesis: for O1, O2 being Ordinal st O1 c= O2 holds
f,O2 -. a [= f,O1 -. a

A13: now

let O4 be Ordinal; :: thesis: ( S₁[O4] implies S₁[ succ O4] )
assume A14: S₁[O4] ; :: thesis: S₁[ succ O4]
thus S₁[ succ O4] :: thesis: verum

proof

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 & O2 c= succ O4 implies f,O2 -. a [= f,O1 -. a )
assume that
A15: O1 c= O2 and
A16: O2 c= succ O4 ; :: thesis: f,O2 -. a [= f,O1 -. a

per cases ( ( O1 = O2 & O2 <> succ O4 ) or ( O1 <> O2 & O2 <> succ O4 ) or ( O1 = O2 & O2 = succ O4 ) or ( O1 <> O2 & O2 = succ O4 ) ) ;

suppose ( O1 = O2 & O2 <> succ O4 ) ; :: thesis: f,O2 -. a [= f,O1 -. a

hence f,O2 -. a [= f,O1 -. a ; :: thesis: verum

end;

suppose ( O1 <> O2 & O2 <> succ O4 ) ; :: thesis: f,O2 -. a [= f,O1 -. a

then O2 c< succ O4 by A16, XBOOLE_0:def 8;
then O2 in succ O4 by ORDINAL1:21;
then O2 c= O4 by ORDINAL1:34;
hence f,O2 -. a [= f,O1 -. a by A14, A15; :: thesis: verum

end;

suppose ( O1 = O2 & O2 = succ O4 ) ; :: thesis: f,O2 -. a [= f,O1 -. a

hence f,O2 -. a [= f,O1 -. a ; :: thesis: verum

end;

suppose A17: ( O1 <> O2 & O2 = succ O4 ) ; :: thesis: f,O2 -. a [= f,O1 -. a

A18: f,(succ O4) -. a [= f,O4 -. a

proof

per cases ( O4 is limit_ordinal or ex O3 being Ordinal st O4 = succ O3 ) by ORDINAL1:42;

suppose A19: O4 is limit_ordinal ; :: thesis: f,(succ O4) -. a [= f,O4 -. a

thus f,(succ O4) -. a [= f,O4 -. a :: thesis: verum

proof

per cases ( O4 = {} or O4 <> {} ) ;

suppose O4 = {} ; :: thesis: f,(succ O4) -. a [= f,O4 -. a

then f,O4 -. a = a by Th17;
hence f,(succ O4) -. a [= f,O4 -. a by A12, Th19; :: thesis: verum

end;

suppose A20: O4 <> {} ; :: thesis: f,(succ O4) -. a [= f,O4 -. a

deffunc H₁( Ordinal) -> Element of L = f,$1 -. a;
consider L1 being T-Sequence such that
A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A22: f,(succ O4) -. a is_less_than rng L1

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or f,(succ O4) -. a [= q )
assume q in rng L1 ; :: thesis: f,(succ O4) -. a [= q
then consider O3 being set such that
A23: O3 in dom L1 and
A24: q = L1 . O3 by FUNCT_1:def 5;
reconsider O3 = O3 as Ordinal by A23;
O3 in succ O3 by ORDINAL1:10;
then A25: O3 c= succ O3 by ORDINAL1:def 2;
O3 c= O4 by A21, A23, ORDINAL1:def 2;
then f,O4 -. a [= f,O3 -. a by A14;
then f . (f,O4 -. a) [= f . (f,O3 -. a) by QUANTAL1:def 12;
then f,(succ O4) -. a [= f . (f,O3 -. a) by Th19;
then A26: f,(succ O4) -. a [= f,(succ O3) -. a by Th19;
succ O3 c= O4 by A21, A23, ORDINAL1:33;
then A27: f,(succ O3) -. a [= f,O3 -. a by A14, A25;
q = f,O3 -. a by A21, A23, A24;
hence f,(succ O4) -. a [= q by A26, A27, LATTICES:25; :: thesis: verum

end;

f,O4 -. a = "/\" (rng L1),L by A19, A20, A21, Th21;
hence f,(succ O4) -. a [= f,O4 -. a by A22, LATTICE3:34; :: thesis: verum

end;

end;

end;

end;

suppose ex O3 being Ordinal st O4 = succ O3 ; :: thesis: f,(succ O4) -. a [= f,O4 -. a

then consider O3 being Ordinal such that
A28: O4 = succ O3 ;
succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
then O3 c= O4 by A28, XBOOLE_1:7;
then f,O4 -. a [= f,O3 -. a by A14;
then f . (f,O4 -. a) [= f . (f,O3 -. a) by QUANTAL1:def 12;
then f . (f,O4 -. a) [= f,O4 -. a by A28, Th19;
hence f,(succ O4) -. a [= f,O4 -. a by Th19; :: thesis: verum

end;

end;

end;

O1 c< O2 by A15, A17, XBOOLE_0:def 8;
then O1 in O2 by ORDINAL1:21;
then O1 c= O4 by A17, ORDINAL1:34;
then f,O4 -. a [= f,O1 -. a by A14;
hence f,O2 -. a [= f,O1 -. a by A17, A18, LATTICES:25; :: thesis: verum

end;

end;

end;

end;

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies f,O2 -. a [= f,O1 -. a )
assume A29: O1 c= O2 ; :: thesis: f,O2 -. a [= f,O1 -. a
A30: S₁[ {} ] ;
for O4 being Ordinal holds S₁[O4] from ORDINAL2:sch 1(A30, A13, A1);
hence f,O2 -. a [= f,O1 -. a by A29; :: thesis: verum