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

A4: now

let O4 be Ordinal; :: thesis: ( S₁[O4] implies S₁[ succ O4] )
assume A5: 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,O1 +. a [= f,O2 +. a )
assume A6: ( O1 c= O2 & O2 c= succ O4 ) ; :: thesis: f,O1 +. a [= f,O2 +. 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,O1 +. a [= f,O2 +. a

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

end;

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

then O2 c< succ O4 by A6, XBOOLE_0:def 8;
then O2 in succ O4 by ORDINAL1:21;
then O2 c= O4 by ORDINAL1:34;
hence f,O1 +. a [= f,O2 +. a by A5, A6; :: thesis: verum

end;

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

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

end;

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

then O1 c< O2 by A6, XBOOLE_0:def 8;
then A8: O1 in O2 by ORDINAL1:21;
A9: f,O4 +. a [= f,(succ O4) +. a

proof

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

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

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

proof

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

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

then f,O4 +. a = a by Th16;
hence f,O4 +. a [= f,(succ O4) +. a by A1, Th18; :: thesis: verum

end;

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

deffunc H₁( Ordinal) -> Element of L = f,$1 +. a;
consider L1 being T-Sequence such that
A12: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A13: f,O4 +. a = "\/" (rng L1),L by A10, A11, A12, Th20;
rng L1 is_less_than f,(succ O4) +. a

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= f,(succ O4) +. a )
assume q in rng L1 ; :: thesis: q [= f,(succ O4) +. a
then consider O3 being set such that
A14: ( O3 in dom L1 & q = L1 . O3 ) by FUNCT_1:def 5;
reconsider O3 = O3 as Ordinal by A14;
O3 c= O4 by A12, A14, ORDINAL1:def 2;
then f,O3 +. a [= f,O4 +. a by A5;
then f . (f,O3 +. a) [= f . (f,O4 +. a) by QUANTAL1:def 12;
then f,(succ O3) +. a [= f . (f,O4 +. a) by Th18;
then A15: f,(succ O3) +. a [= f,(succ O4) +. a by Th18;
A16: succ O3 c= O4 by A12, A14, ORDINAL1:33;
O3 in succ O3 by ORDINAL1:10;
then O3 c= succ O3 by ORDINAL1:def 2;
then A17: f,O3 +. a [= f,(succ O3) +. a by A5, A16;
q = f,O3 +. a by A12, A14;
hence q [= f,(succ O4) +. a by A15, A17, LATTICES:25; :: thesis: verum

end;

hence f,O4 +. a [= f,(succ O4) +. a by A13, LATTICE3:def 21; :: thesis: verum

end;

end;

end;

end;

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

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

end;

end;

end;

O1 c= O4 by A7, A8, ORDINAL1:34;
then f,O1 +. a [= f,O4 +. a by A5;
hence f,O1 +. a [= f,O2 +. a by A7, A9, LATTICES:25; :: thesis: verum

end;

end;

end;

end;

A19: 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 A20: ( O4 <> {} & O4 is limit_ordinal & ( 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,O1 +. a [= f,O2 +. a )
assume A21: ( O1 c= O2 & O2 c= O4 ) ; :: thesis: f,O1 +. a [= f,O2 +. a
A22: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) by XBOOLE_0:def 8;
A23: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) by XBOOLE_0:def 8;

per cases ( O2 = O4 or O2 in O4 ) by A21, A22, ORDINAL1:21;

suppose A24: O2 = O4 ; :: thesis: f,O1 +. a [= f,O2 +. a

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

proof

per cases ( O1 = O2 or O1 in O2 ) by A21, A23, ORDINAL1:21;

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

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

end;

suppose A25: O1 in O2 ; :: thesis: f,O1 +. a [= f,O2 +. a

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

end;

end;

end;

end;

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

hence f,O1 +. a [= f,O2 +. a by A20, A21; :: thesis: verum

end;

end;

end;

end;

A28: for O4 being Ordinal holds S₁[O4] from ORDINAL2:sch 1(A2, A4, A19);
let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies f,O1 +. a [= f,O2 +. a )
assume O1 c= O2 ; :: thesis: f,O1 +. a [= f,O2 +. a
hence f,O1 +. a [= f,O2 +. a by A28; :: thesis: verum