let Omega be non empty set ; for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega
let Z be Field_Subset of Omega; monotoneclass Z is Field_Subset of Omega
A1:
Z c= monotoneclass Z
by Def9;
then reconsider Z1 = monotoneclass Z as non empty Subset-Family of Omega ;
A2:
for y, Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
proof
let y,
Y be
set ;
( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )
assume A3:
Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) }
;
for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
thus
for
z being
set st
z in Y holds
(
z in Z1 &
y \ z in Z1 &
z \ y in Z1 &
z /\ y in Z1 )
verum
end;
A4:
for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omega
proof
let y be
Element of
Z1;
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omegalet Y be
set ;
( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Y is MonotoneClass of Omega )
assume A5:
Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) }
;
Y is MonotoneClass of Omega
A6:
for
A1 being
SetSequence of
Omega st
A1 is
monotone &
rng A1 c= Y holds
lim A1 in Y
proof
let A1 be
SetSequence of
Omega;
( A1 is monotone & rng A1 c= Y implies lim A1 in Y )
assume that A7:
A1 is
monotone
and A8:
rng A1 c= Y
;
lim A1 in Y
A9:
A1 is
convergent
by A7, SETLIM_1:65;
for
n being
Nat holds
A1 . n in Z1
then
rng A1 c= Z1
by NAT_1:52;
then A10:
lim A1 is
Element of
Z1
by A7, Th69;
for
n being
Nat holds
(A1 (\) y) . n in Z1
then A11:
rng (A1 (\) y) c= Z1
by NAT_1:52;
for
n being
Nat holds
(y (/\) A1) . n in Z1
then A12:
rng (y (/\) A1) c= Z1
by NAT_1:52;
y (/\) A1 is
monotone
by A7, SETLIM_2:23;
then
lim (y (/\) A1) in Z1
by A12, Th69;
then A13:
y /\ (lim A1) in Z1
by A9, SETLIM_2:92;
for
n being
Nat holds
(y (\) A1) . n in Z1
then A14:
rng (y (\) A1) c= Z1
by NAT_1:52;
y (\) A1 is
monotone
by A7, SETLIM_2:29;
then
lim (y (\) A1) in Z1
by A14, Th69;
then A15:
y \ (lim A1) in Z1
by A9, SETLIM_2:94;
A1 (\) y is
monotone
by A7, SETLIM_2:32;
then
lim (A1 (\) y) in Z1
by A11, Th69;
then
(lim A1) \ y in Z1
by A9, SETLIM_2:95;
hence
lim A1 in Y
by A5, A10, A15, A13;
verum
end;
for
z being
object st
z in Y holds
z in Z1
by A2, A5;
then
Y c= Z1
;
hence
Y is
MonotoneClass of
Omega
by A6, Th69, XBOOLE_1:1;
verum
end;
A16:
for y being Element of Z
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
A21:
for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
A28:
for y being Subset of Omega st y in Z1 holds
y ` in Z1
hence
monotoneclass Z is Field_Subset of Omega
by A28, FINSUB_1:def 2, PROB_1:def 1; verum