let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let F be ManySortedSigmaField of I,Sigma; :: thesis: for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let J be non empty Subset of I; :: thesis: MeetSections (J,F) is non empty Subset of Sigma

A1: MeetSections (J,F) c= Sigma

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let F be ManySortedSigmaField of I,Sigma; :: thesis: for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

let J be non empty Subset of I; :: thesis: MeetSections (J,F) is non empty Subset of Sigma

A1: MeetSections (J,F) c= Sigma

proof

MeetSections (J,F) is non empty set
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in MeetSections (J,F) or X in Sigma )

assume X in MeetSections (J,F) ; :: thesis: X in Sigma

then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that

E c= J and

A2: X = meet (rng f) by Def9;

reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;

for B being Element of Fin E holds meet (rng (f | B)) in Sigma

hence X in Sigma by A2; :: thesis: verum

end;assume X in MeetSections (J,F) ; :: thesis: X in Sigma

then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that

E c= J and

A2: X = meet (rng f) by Def9;

reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;

for B being Element of Fin E holds meet (rng (f | B)) in Sigma

proof

then
meet (rng (f | Ee)) in Sigma
;
defpred S_{1}[ set ] means meet (rng (f | $1)) in Sigma;

let B be Element of Fin E; :: thesis: meet (rng (f | B)) in Sigma

A3: for B9 being Element of Fin E

for b being Element of E st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]

then A10: S_{1}[ {}. E]
by PROB_1:4;

for B1 being Element of Fin E holds S_{1}[B1]
from SETWISEO:sch 2(A10, A3);

hence meet (rng (f | B)) in Sigma ; :: thesis: verum

end;let B be Element of Fin E; :: thesis: meet (rng (f | B)) in Sigma

A3: for B9 being Element of Fin E

for b being Element of E st S

S

proof

meet (rng (f | {})) = {}
by SETFAM_1:def 1;
let B9 be Element of Fin E; :: thesis: for b being Element of E st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]

let b be Element of E; :: thesis: ( S_{1}[B9] & not b in B9 implies S_{1}[B9 \/ {b}] )

assume that

A4: meet (rng (f | B9)) in Sigma and

not b in B9 ; :: thesis: S_{1}[B9 \/ {b}]

A5: rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78

.= (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12 ;

( dom f = E & b in {b} ) by FUNCT_2:def 1, TARSKI:def 1;

then A6: f . b in rng (f | {b}) by FUNCT_1:50;

A7: b is Element of dom f by FUNCT_2:def 1;

then (dom f) /\ {b} = {b} by ZFMISC_1:46;

then dom (f | {b}) = {b} by RELAT_1:61;

then A8: rng (f | {b}) = {((f | {b}) . b)} by FUNCT_1:4;

b in {b} by TARSKI:def 1;

then b in dom (f | {b}) by A7, RELAT_1:57;

then rng (f | {b}) = {(f . b)} by A8, FUNCT_1:47;

then A9: meet (rng (f | {b})) is Event of Sigma by SETFAM_1:10;

end;S

let b be Element of E; :: thesis: ( S

assume that

A4: meet (rng (f | B9)) in Sigma and

not b in B9 ; :: thesis: S

A5: rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78

.= (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12 ;

( dom f = E & b in {b} ) by FUNCT_2:def 1, TARSKI:def 1;

then A6: f . b in rng (f | {b}) by FUNCT_1:50;

A7: b is Element of dom f by FUNCT_2:def 1;

then (dom f) /\ {b} = {b} by ZFMISC_1:46;

then dom (f | {b}) = {b} by RELAT_1:61;

then A8: rng (f | {b}) = {((f | {b}) . b)} by FUNCT_1:4;

b in {b} by TARSKI:def 1;

then b in dom (f | {b}) by A7, RELAT_1:57;

then rng (f | {b}) = {(f . b)} by A8, FUNCT_1:47;

then A9: meet (rng (f | {b})) is Event of Sigma by SETFAM_1:10;

then A10: S

for B1 being Element of Fin E holds S

hence meet (rng (f | B)) in Sigma ; :: thesis: verum

hence X in Sigma by A2; :: thesis: verum

proof

hence
MeetSections (J,F) is non empty Subset of Sigma
by A1; :: thesis: verum
set E = the non empty finite Subset of J;

consider f being Function such that

A11: dom f = the non empty finite Subset of J and

A12: rng f = {{}} by FUNCT_1:5;

reconsider E = the non empty finite Subset of J as non empty finite Subset of I by XBOOLE_1:1;

A13: meet (rng f) = {} by A12, SETFAM_1:10;

rng f c= Sigma

for i being set st i in E holds

f . i in F . i

reconsider mrf = meet (rng f) as Subset of Omega by A13, XBOOLE_1:2;

mrf in MeetSections (J,F) by Def9;

hence MeetSections (J,F) is non empty set ; :: thesis: verum

end;consider f being Function such that

A11: dom f = the non empty finite Subset of J and

A12: rng f = {{}} by FUNCT_1:5;

reconsider E = the non empty finite Subset of J as non empty finite Subset of I by XBOOLE_1:1;

A13: meet (rng f) = {} by A12, SETFAM_1:10;

rng f c= Sigma

proof

then reconsider f = f as Function of E,Sigma by A11, FUNCT_2:2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Sigma )

assume y in rng f ; :: thesis: y in Sigma

then y = {} by A12, TARSKI:def 1;

hence y in Sigma by PROB_1:4; :: thesis: verum

end;assume y in rng f ; :: thesis: y in Sigma

then y = {} by A12, TARSKI:def 1;

hence y in Sigma by PROB_1:4; :: thesis: verum

for i being set st i in E holds

f . i in F . i

proof

then reconsider f = f as SigmaSection of E,F by Def4;
let i be set ; :: thesis: ( i in E implies f . i in F . i )

assume A14: i in E ; :: thesis: f . i in F . i

then reconsider Fi = F . i as SigmaField of Omega by Def2;

f . i in rng f by A11, A14, FUNCT_1:def 3;

then f . i = {} by A12, TARSKI:def 1;

then f . i in Fi by PROB_1:4;

hence f . i in F . i ; :: thesis: verum

end;assume A14: i in E ; :: thesis: f . i in F . i

then reconsider Fi = F . i as SigmaField of Omega by Def2;

f . i in rng f by A11, A14, FUNCT_1:def 3;

then f . i = {} by A12, TARSKI:def 1;

then f . i in Fi by PROB_1:4;

hence f . i in F . i ; :: thesis: verum

reconsider mrf = meet (rng f) as Subset of Omega by A13, XBOOLE_1:2;

mrf in MeetSections (J,F) by Def9;

hence MeetSections (J,F) is non empty set ; :: thesis: verum