let L be complete Lattice; 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; 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; ( 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 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;
( 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]
;
S1[O4]thus
S1[
O4]
verumproof
let O1,
O2 be
Ordinal;
( O1 c= O2 & O2 c= O4 implies (f,O1) +. a [= (f,O2) +. a )
assume that A4:
O1 c= O2
and A5:
O2 c= O4
;
(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
;
(f,O1) +. a [= (f,O2) +. athus
(
f,
O1)
+. a [= (
f,
O2)
+. a
verumproof
per cases
( O1 = O2 or O1 in O2 )
by A4, A7, ORDINAL1:11;
suppose A9:
O1 in O2
;
(f,O1) +. a [= (f,O2) +. adeffunc 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;
verum end; end;
end; end; end;
end; end;
assume A12:
a [= f . a
; for O1, O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a [= (f,O2) +. a
A13:
now for O4 being Ordinal st S1[O4] holds
S1[ succ O4]let O4 be
Ordinal;
( S1[O4] implies S1[ succ O4] )assume A14:
S1[
O4]
;
S1[ succ O4]thus
S1[
succ O4]
verumproof
let O1,
O2 be
Ordinal;
( 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
;
(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 A17:
(
O1 <> O2 &
O2 = succ O4 )
;
(f,O1) +. a [= (f,O2) +. aA18:
(
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
;
(f,O4) +. a [= (f,(succ O4)) +. athus
(
f,
O4)
+. a [= (
f,
(succ O4))
+. a
verumproof
per cases
( O4 = {} or O4 <> {} )
;
suppose A20:
O4 <> {}
;
(f,O4) +. a [= (f,(succ O4)) +. adeffunc 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;
LATTICE3:def 17 ( not q in rng L1 or q [= (f,(succ O4)) +. a )
assume
q in rng L1
;
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;
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;
verum end; end;
end; end; suppose
ex
O3 being
Ordinal st
O4 = succ O3
;
(f,O4) +. a [= (f,(succ O4)) +. athen 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;
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;
verum end; end;
end; end;
let O1, O2 be Ordinal; ( O1 c= O2 implies (f,O1) +. a [= (f,O2) +. a )
assume A29:
O1 c= O2
; (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; verum