let Omega, I be non empty set ; for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let Sigma be SigmaField of Omega; for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let F be ManySortedSigmaField of I,Sigma; for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let J be non empty Subset of I; sigma (MeetSections (J,F)) = sigUn (F,J)
A1:
Union (F | J) c= MeetSections (J,F)
proof
let x be
object ;
TARSKI:def 3 ( not x in Union (F | J) or x in MeetSections (J,F) )
assume
x in Union (F | J)
;
x in MeetSections (J,F)
then consider y being
set such that A2:
x in y
and A3:
y in rng (F | J)
by TARSKI:def 4;
consider i being
object such that A4:
i in dom (F | J)
and A5:
y = (F | J) . i
by A3, FUNCT_1:def 3;
reconsider i =
i as
set by TARSKI:1;
y = (F | J) . i
by A5;
then reconsider x =
x as
Subset of
Omega by A2;
defpred S1[
object ,
object ]
means ( $2
= x & $2
in F . $1 );
A6:
{i} c= J
by A4, ZFMISC_1:31;
then reconsider E =
{i} as
finite Subset of
I by XBOOLE_1:1;
A7:
for
j being
object st
j in E holds
ex
y being
object st
(
y in Sigma &
S1[
j,
y] )
proof
let j be
object ;
( j in E implies ex y being object st
( y in Sigma & S1[j,y] ) )
assume A8:
j in E
;
ex y being object st
( y in Sigma & S1[j,y] )
i in I
by A4, TARSKI:def 3;
then A9:
F . i in bool Sigma
by FUNCT_2:5;
take y =
x;
( y in Sigma & S1[j,y] )
y in F . i
by A2, A4, A5, FUNCT_1:49;
hence
(
y in Sigma &
S1[
j,
y] )
by A8, A9, TARSKI:def 1;
verum
end;
consider g being
Function of
E,
Sigma such that A10:
for
j being
object st
j in E holds
S1[
j,
g . j]
from FUNCT_2:sch 1(A7);
for
i being
set st
i in E holds
g . i in F . i
by A10;
then reconsider g =
g as
SigmaSection of
E,
F by Def4;
dom g = E
by FUNCT_2:def 1;
then A11:
rng g = {(g . i)}
by FUNCT_1:4;
i in E
by TARSKI:def 1;
then x =
g . i
by A10
.=
meet (rng g)
by A11, SETFAM_1:10
;
hence
x in MeetSections (
J,
F)
by A6, Def9;
verum
end;
MeetSections (J,F) c= sigma (Union (F | J))
hence
sigma (MeetSections (J,F)) c= sigUn (F,J)
by PROB_1:def 9; XBOOLE_0:def 10 sigUn (F,J) c= sigma (MeetSections (J,F))
MeetSections (J,F) c= sigma (MeetSections (J,F))
by PROB_1:def 9;
then
Union (F | J) c= sigma (MeetSections (J,F))
by A1;
hence
sigUn (F,J) c= sigma (MeetSections (J,F))
by PROB_1:def 9; verum