let Omega be non empty set ; :: thesis: for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega

let Z be Field_Subset of Omega; :: thesis: 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 )

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

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

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

y ` in Z1

let Z be Field_Subset of Omega; :: thesis: 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

A4:
for y being Element of Z1
let y, Y be set ; :: thesis: ( 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 ) } ; :: thesis: 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 ) :: thesis: verum

end;( 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 ) } ; :: thesis: 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 ) :: thesis: verum

proof

let z be set ; :: thesis: ( z in Y implies ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )

assume z in Y ; :: thesis: ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )

then ex z1 being Element of Z1 st

( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3;

hence ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ; :: thesis: verum

end;assume z in Y ; :: thesis: ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )

then ex z1 being Element of Z1 st

( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3;

hence ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ; :: thesis: verum

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

A16:
for y being Element of Z
let y be Element of Z1; :: thesis: 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

let Y be set ; :: thesis: ( 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 ) } ; :: thesis: 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

z in Z1 by A2, A5;

then Y c= Z1 ;

hence Y is MonotoneClass of Omega by A6, Th69, XBOOLE_1:1; :: thesis: verum

end;Y is MonotoneClass of Omega

let Y be set ; :: thesis: ( 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 ) } ; :: thesis: 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

for z being object st z in Y holds
let A1 be SetSequence of Omega; :: thesis: ( A1 is monotone & rng A1 c= Y implies lim A1 in Y )

assume that

A7: A1 is monotone and

A8: rng A1 c= Y ; :: thesis: lim A1 in Y

A9: A1 is convergent by A7, SETLIM_1:65;

for n being Nat holds A1 . n in Z1

then A10: lim A1 is Element of Z1 by A7, Th69;

for n being Nat holds (A1 (\) y) . n in Z1

for n being Nat holds (y (/\) A1) . n in Z1

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

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; :: thesis: verum

end;assume that

A7: A1 is monotone and

A8: rng A1 c= Y ; :: thesis: lim A1 in Y

A9: A1 is convergent by A7, SETLIM_1:65;

for n being Nat holds A1 . n in Z1

proof

then
rng A1 c= Z1
by NAT_1:52;
let n be Nat; :: thesis: A1 . n in Z1

A1 . n in rng A1 by NAT_1:51;

hence A1 . n in Z1 by A2, A5, A8; :: thesis: verum

end;A1 . n in rng A1 by NAT_1:51;

hence A1 . n in Z1 by A2, A5, A8; :: thesis: verum

then A10: lim A1 is Element of Z1 by A7, Th69;

for n being Nat holds (A1 (\) y) . n in Z1

proof

then A11:
rng (A1 (\) y) c= Z1
by NAT_1:52;
let n be Nat; :: thesis: (A1 (\) y) . n in Z1

A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & (A1 . n) \ y in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (A1 (\) y) . n in Z1 by SETLIM_2:def 8; :: thesis: verum

end;A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & (A1 . n) \ y in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (A1 (\) y) . n in Z1 by SETLIM_2:def 8; :: thesis: verum

for n being Nat holds (y (/\) A1) . n in Z1

proof

then A12:
rng (y (/\) A1) c= Z1
by NAT_1:52;
let n be Nat; :: thesis: (y (/\) A1) . n in Z1

A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & y /\ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (y (/\) A1) . n in Z1 by SETLIM_2:def 5; :: thesis: verum

end;A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & y /\ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (y (/\) A1) . n in Z1 by SETLIM_2:def 5; :: thesis: verum

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

proof

then A14:
rng (y (\) A1) c= Z1
by NAT_1:52;
let n be Nat; :: thesis: (y (\) A1) . n in Z1

A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & y \ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (y (\) A1) . n in Z1 by SETLIM_2:def 7; :: thesis: verum

end;A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & y \ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;

hence (y (\) A1) . n in Z1 by SETLIM_2:def 7; :: thesis: verum

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; :: thesis: verum

z in Z1 by A2, A5;

then Y c= Z1 ;

hence Y is MonotoneClass of Omega by A6, Th69, XBOOLE_1:1; :: thesis: verum

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

proof

A21:
for y being Element of Z1
let y be Element of Z; :: thesis: 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

let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )

assume A17: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y

A18: Z c= Y

then Y is MonotoneClass of Omega by A1, A4, A17;

hence Z1 c= Y by A18, Def9; :: thesis: verum

end;Z1 c= Y

let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )

assume A17: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y

A18: Z c= Y

proof

y in Z
;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )

reconsider zz = z as set by TARSKI:1;

assume A19: z in Z ; :: thesis: z in Y

then A20: zz /\ y in Z by FINSUB_1:def 2;

( zz \ y in Z & y \ zz in Z ) by A19, PROB_1:6;

hence z in Y by A1, A17, A19, A20; :: thesis: verum

end;reconsider zz = z as set by TARSKI:1;

assume A19: z in Z ; :: thesis: z in Y

then A20: zz /\ y in Z by FINSUB_1:def 2;

( zz \ y in Z & y \ zz in Z ) by A19, PROB_1:6;

hence z in Y by A1, A17, A19, A20; :: thesis: verum

then Y is MonotoneClass of Omega by A1, A4, A17;

hence Z1 c= Y by A18, Def9; :: thesis: verum

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

proof

A28:
for y being Subset of Omega st y in Z1 holds
let y be Element of Z1; :: thesis: 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

let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )

assume A22: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y

A23: Z c= Y

hence Z1 c= Y by A23, Def9; :: thesis: verum

end;Z1 c= Y

let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )

assume A22: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y

A23: Z c= Y

proof

Y is MonotoneClass of Omega
by A4, A22;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )

reconsider zz = z as set by TARSKI:1;

set Y1 = { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } ;

assume A24: z in Z ; :: thesis: z in Y

then A25: Z1 c= { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } by A16;

A26: y in Z1 ;

then A27: zz /\ y in Z1 by A2, A25;

( zz \ y in Z1 & y \ zz in Z1 ) by A2, A25, A26;

hence z in Y by A1, A22, A24, A27; :: thesis: verum

end;reconsider zz = z as set by TARSKI:1;

set Y1 = { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } ;

assume A24: z in Z ; :: thesis: z in Y

then A25: Z1 c= { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } by A16;

A26: y in Z1 ;

then A27: zz /\ y in Z1 by A2, A25;

( zz \ y in Z1 & y \ zz in Z1 ) by A2, A25, A26;

hence z in Y by A1, A22, A24, A27; :: thesis: verum

hence Z1 c= Y by A23, Def9; :: thesis: verum

y ` in Z1

proof

Omega in Z
by PROB_1:5;

then A29: Omega in Z1 by A1;

let y be Subset of Omega; :: thesis: ( y in Z1 implies y ` in Z1 )

assume A30: y in Z1 ; :: thesis: y ` in Z1

set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;

Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A30;

then Omega \ y in Z1 by A2, A29;

hence y ` in Z1 by SUBSET_1:def 4; :: thesis: verum

end;then A29: Omega in Z1 by A1;

let y be Subset of Omega; :: thesis: ( y in Z1 implies y ` in Z1 )

assume A30: y in Z1 ; :: thesis: y ` in Z1

set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;

Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A30;

then Omega \ y in Z1 by A2, A29;

hence y ` in Z1 by SUBSET_1:def 4; :: thesis: verum

now :: thesis: for y, z being set st y in Z1 & z in Z1 holds

y /\ z in Z1

hence
monotoneclass Z is Field_Subset of Omega
by A28, FINSUB_1:def 2, PROB_1:def 1; :: thesis: verumy /\ z in Z1

let y, z be set ; :: thesis: ( y in Z1 & z in Z1 implies y /\ z in Z1 )

assume that

A31: y in Z1 and

A32: z in Z1 ; :: thesis: y /\ z in Z1

set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;

Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A31;

hence y /\ z in Z1 by A2, A32; :: thesis: verum

end;assume that

A31: y in Z1 and

A32: z in Z1 ; :: thesis: y /\ z in Z1

set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;

Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A31;

hence y /\ z in Z1 by A2, A32; :: thesis: verum