defpred S1[ set ] means $1 is_a_fixpoint_of f;
set P = { x where x is Element of L : S1[x] } ;
A1:
{ 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
A2:
a is_a_fixpoint_of f
by B1, Th21;
A3:
a in { x where x is Element of L : S1[x] }
by A2;
reconsider P = { x where x is Element of L : S1[x] } as Subset of L by A1;
A4:
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 A5:
x in P
and A6:
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 A7:
x = a
and A8:
a is_a_fixpoint_of f
by A5;
consider b being
Element of
L such that A9:
y = b
and A10:
b is_a_fixpoint_of f
by A6;
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 A11:
(
f,
O)
+. ab is_a_fixpoint_of f
and A12:
(
a [= (
f,
O)
+. ab &
b [= (
f,
O)
+. ab )
by B1, A8, A10, 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 A11;
( 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 A7, A9, A12;
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 A13:
z9 in P
and A14:
(
x [= z9 &
y [= z9 )
;
(f,O) +. ab [= z9
A15:
ex
zz being
Element of
L st
(
zz = z9 &
zz is_a_fixpoint_of f )
by A13;
ab [= z9
by A7, A9, A14, FILTER_0:6;
hence
(
f,
O)
+. ab [= z9
by B1, A15, 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 A16:
x in P
and A17:
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 A18:
x = a
and A19:
a is_a_fixpoint_of f
by A16;
consider b being
Element of
L such that A20:
y = b
and A21:
b is_a_fixpoint_of f
by A17;
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 A22:
(
f,
O)
-. ab is_a_fixpoint_of f
and A23:
( (
f,
O)
-. ab [= a & (
f,
O)
-. ab [= b )
by B1, A19, A21, 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 A22;
( (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 A18, A20, A23;
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 A24:
z9 in P
and A25:
(
z9 [= x &
z9 [= y )
;
z9 [= (f,O) -. ab
A26:
ex
zz being
Element of
L st
(
zz = z9 &
zz is_a_fixpoint_of f )
by A24;
z9 [= ab
by A18, A20, A25, FILTER_0:7;
hence
z9 [= (
f,
O)
-. ab
by B1, A26, Th35;
verum
end;
then reconsider P = P as non empty with_suprema with_infima Subset of L by A3, A4;
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