defpred S1[ set ] means $1 is_a_fixpoint_of f;
set P = { x where x is Element of L : S1[x] } ;
A2:
{ x where x is Element of L : S1[x] } is Subset of L
from DOMAIN_1:sch 7();
consider a being Element of L such that
A3:
a is_a_fixpoint_of f
by A1, Th21;
A4:
a in { x where x is Element of L : S1[x] }
by A3;
reconsider P = { x where x is Element of L : S1[x] } as Subset of L by A2;
A5:
P is with_suprema
proof
let x,
y be
Element of
L;
KNASTER:def 6 ( x in P & y in P implies ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) )
assume that A6:
x in P
and A7:
y in P
;
ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
consider a being
Element of
L such that A8:
x = a
and A9:
a is_a_fixpoint_of f
by A6;
consider b being
Element of
L such that A10:
y = b
and A11:
b is_a_fixpoint_of f
by A7;
reconsider a =
a,
b =
b as
Element of
L ;
reconsider ab =
a "\/" b as
Element of
L ;
consider O being
Ordinal such that
card O c= card the
carrier of
L
and A12:
(
f,
O)
+. ab is_a_fixpoint_of f
and A13:
(
a [= (
f,
O)
+. ab &
b [= (
f,
O)
+. ab )
by A1, A9, A11, Th32;
set z = (
f,
O)
+. ab;
take
(
f,
O)
+. ab
;
( (f,O) +. ab in P & x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9 ) )
thus
(
f,
O)
+. ab in P
by A12;
( x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9 ) )
thus
(
x [= (
f,
O)
+. ab &
y [= (
f,
O)
+. ab )
by A8, A10, A13;
for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9
let z9 be
Element of
L;
( z9 in P & x [= z9 & y [= z9 implies (f,O) +. ab [= z9 )
assume that A14:
z9 in P
and A15:
(
x [= z9 &
y [= z9 )
;
(f,O) +. ab [= z9
A16:
ex
zz being
Element of
L st
(
zz = z9 &
zz is_a_fixpoint_of f )
by A14;
ab [= z9
by A8, A10, A15, FILTER_0:6;
hence
(
f,
O)
+. ab [= z9
by A1, A16, Th34;
verum
end;
P is with_infima
proof
let x,
y be
Element of
L;
KNASTER:def 7 ( x in P & y in P implies ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) )
assume that A17:
x in P
and A18:
y in P
;
ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
consider a being
Element of
L such that A19:
x = a
and A20:
a is_a_fixpoint_of f
by A17;
consider b being
Element of
L such that A21:
y = b
and A22:
b is_a_fixpoint_of f
by A18;
reconsider a =
a,
b =
b as
Element of
L ;
reconsider ab =
a "/\" b as
Element of
L ;
consider O being
Ordinal such that
card O c= card the
carrier of
L
and A23:
(
f,
O)
-. ab is_a_fixpoint_of f
and A24:
( (
f,
O)
-. ab [= a & (
f,
O)
-. ab [= b )
by A1, A20, A22, Th33;
set z = (
f,
O)
-. ab;
take
(
f,
O)
-. ab
;
( (f,O) -. ab in P & (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab ) )
thus
(
f,
O)
-. ab in P
by A23;
( (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab ) )
thus
( (
f,
O)
-. ab [= x & (
f,
O)
-. ab [= y )
by A19, A21, A24;
for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab
let z9 be
Element of
L;
( z9 in P & z9 [= x & z9 [= y implies z9 [= (f,O) -. ab )
assume that A25:
z9 in P
and A26:
(
z9 [= x &
z9 [= y )
;
z9 [= (f,O) -. ab
A27:
ex
zz being
Element of
L st
(
zz = z9 &
zz is_a_fixpoint_of f )
by A25;
z9 [= ab
by A19, A21, A26, FILTER_0:7;
hence
z9 [= (
f,
O)
-. ab
by A1, A27, Th35;
verum
end;
then reconsider P = P as non empty with_suprema with_infima Subset of L by A4, A5;
take
latt P
; ex P being non empty with_suprema with_infima Subset of L st
( P = { x where x is Element of L : x is_a_fixpoint_of f } & latt P = latt P )
take
P
; ( P = { x where x is Element of L : x is_a_fixpoint_of f } & latt P = latt P )
thus
P = { x where x is Element of L : x is_a_fixpoint_of f }
; latt P = latt P
thus
latt P = latt P
; verum