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 )
defpred S1[ Ordinal] means for O1, O2 being Ordinal st O1 c= O2 & O2 c= $1 holds
(f,O1) +. a [= (f,O2) +. a;
A1: now :: thesis: for O4 being Ordinal st O4 <> 0 & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds
S1[O3] ) holds
S1[O4]
let O4 be Ordinal; :: thesis: ( O4 <> 0 & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds
S1[O3] ) implies S1[O4] )
assume that
A2: ( O4 <> 0 & O4 is limit_ordinal ) and
A3: for O3 being Ordinal st O3 in O4 holds
S1[O3] ; :: thesis: S1[O4]
thus S1[O4] :: thesis: verum
proof
let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 & O2 c= O4 implies (f,O1) +. a [= (f,O2) +. a )
assume that
A4: O1 c= O2 and
A5: O2 c= O4 ; :: thesis: (f,O1) +. a [= (f,O2) +. a
A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) ;
A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) ;
per cases ( O2 = O4 or O2 in O4 ) by A5, A6, ORDINAL1:11;
suppose A8: 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 A4, A7, ORDINAL1:11;
suppose O1 = O2 ; :: thesis: (f,O1) +. a [= (f,O2) +. a
hence (f,O1) +. a [= (f,O2) +. a ; :: thesis: verum
end;
suppose A9: O1 in O2 ; :: thesis: (f,O1) +. a [= (f,O2) +. a
deffunc H1( Ordinal) -> Element of L = (f,$1) +. a;
consider L1 being Sequence such that
A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch 2();
A11: ( L1 . O1 = (f,O1) +. a & L1 . O1 in rng L1 ) by A9, A10, FUNCT_1:def 3;
(f,O2) +. a = "\/" ((rng L1),L) by A2, A8, A10, Th17;
hence (f,O1) +. a [= (f,O2) +. a by A11, 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 A3, A4; :: thesis: verum
end;
end;
end;
end;
assume A12: a [= f . a ; :: thesis: for O1, O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a [= (f,O2) +. a
A13: now :: thesis: for O4 being Ordinal st S1[O4] holds
S1[ succ O4]
let O4 be Ordinal; :: thesis: ( S1[O4] implies S1[ succ O4] )
assume A14: S1[O4] ; :: thesis: S1[ succ O4]
thus S1[ 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 that
A15: O1 c= O2 and
A16: 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 A16;
then O2 in succ O4 by ORDINAL1:11;
then O2 c= O4 by ORDINAL1:22;
hence (f,O1) +. a [= (f,O2) +. a by A14, A15; :: 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 A17: ( O1 <> O2 & O2 = succ O4 ) ; :: thesis: (f,O1) +. a [= (f,O2) +. a
A18: (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:29;
suppose A19: 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 Th13;
hence (f,O4) +. a [= (f,(succ O4)) +. a by A12, Th15; :: thesis: verum
end;
suppose A20: O4 <> {} ; :: thesis: (f,O4) +. a [= (f,(succ O4)) +. a
deffunc H1( Ordinal) -> Element of L = (f,$1) +. a;
consider L1 being Sequence such that
A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch 2();
A22: 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 object such that
A23: O3 in dom L1 and
A24: q = L1 . O3 by FUNCT_1:def 3;
reconsider O3 = O3 as Ordinal by A23;
O3 in succ O3 by ORDINAL1:6;
then A25: O3 c= succ O3 by ORDINAL1:def 2;
O3 c= O4 by A21, A23, ORDINAL1:def 2;
then (f,O3) +. a [= (f,O4) +. a by A14;
then f . ((f,O3) +. a) [= f . ((f,O4) +. a) by QUANTAL1:def 12;
then (f,(succ O3)) +. a [= f . ((f,O4) +. a) by Th15;
then A26: (f,(succ O3)) +. a [= (f,(succ O4)) +. a by Th15;
succ O3 c= O4 by A21, A23, ORDINAL1:21;
then A27: (f,O3) +. a [= (f,(succ O3)) +. a by A14, A25;
q = (f,O3) +. a by A21, A23, A24;
hence q [= (f,(succ O4)) +. a by A26, A27, LATTICES:7; :: thesis: verum
end;
(f,O4) +. a = "\/" ((rng L1),L) by A19, A20, A21, Th17;
hence (f,O4) +. a [= (f,(succ O4)) +. a by A22, 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
A28: O4 = succ O3 ;
O3 c= O4 by A28, XBOOLE_1:7;
then (f,O3) +. a [= (f,O4) +. a by A14;
then f . ((f,O3) +. a) [= f . ((f,O4) +. a) by QUANTAL1:def 12;
then (f,O4) +. a [= f . ((f,O4) +. a) by A28, Th15;
hence (f,O4) +. a [= (f,(succ O4)) +. a by Th15; :: thesis: verum
end;
end;
end;
O1 c< O2 by A15, A17;
then O1 in O2 by ORDINAL1:11;
then O1 c= O4 by A17, ORDINAL1:22;
then (f,O1) +. a [= (f,O4) +. a by A14;
hence (f,O1) +. a [= (f,O2) +. a by A17, A18, LATTICES:7; :: thesis: verum
end;
end;
end;
end;
let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies (f,O1) +. a [= (f,O2) +. a )
assume A29: O1 c= O2 ; :: thesis: (f,O1) +. a [= (f,O2) +. a
A30: S1[ 0 ] ;
for O4 being Ordinal holds S1[O4] from ORDINAL2:sch 1(A30, A13, A1);
 hence (f,O1) +. a [= (f,O2) +. a by A29; :: thesis: verum