set BS = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;
{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is non empty Subset-Family of I
proof
reconsider RE = REAL as Element of Borel_Sets by PROB_1:5;
d1: Borelsubsets_help (RE,I) in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;
{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } c= bool I
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } or x in bool I )
assume x in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ; :: thesis: x in bool I
then consider A being Element of Borel_Sets such that
D1: x = Borelsubsets_help (A,I) ;
reconsider x = x as set by D1;
x c= I by D1, XBOOLE_0:def 4;
hence x in bool I ; :: thesis: verum
end;
hence { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is non empty Subset-Family of I by d1; :: thesis: verum
end;
then reconsider BS = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } as non empty Subset-Family of I ;
A1: BS is compl-closed
proof
for A being Subset of I st A in BS holds
A ` in BS
proof
let A be Subset of I; :: thesis: ( A in BS implies A ` in BS )
assume A in BS ; :: thesis: A ` in BS
then consider A2 being Element of Borel_Sets such that
AF1: A = Borelsubsets_help (A2,I) ;
F2: I \ A = (A2 `) /\ I
proof
for x being object holds
( x in I \ A iff x in (A2 `) /\ I )
proof
let x be object ; :: thesis: ( x in I \ A iff x in (A2 `) /\ I )
thus ( x in I \ A implies x in (A2 `) /\ I ) :: thesis: ( x in (A2 `) /\ I implies x in I \ A )
proof
assume ASS0: x in I \ A ; :: thesis: x in (A2 `) /\ I
reconsider I = I as Subset of REAL ;
( x in I & not x in A ) by ASS0, XBOOLE_0:def 5;
then ( x in I & ( not x in A2 or not x in I ) ) by XBOOLE_0:def 4, AF1;
then ( x in I & x in REAL \ A2 ) by XBOOLE_0:def 5;
hence x in (A2 `) /\ I by XBOOLE_0:def 4; :: thesis: verum
end;
assume x in (A2 `) /\ I ; :: thesis: x in I \ A
then ( x in A2 ` & x in I ) by XBOOLE_0:def 4;
then ( x in I & x in REAL & not x in A2 ) by XBOOLE_0:def 5;
then ( x in I & not x in A2 /\ I ) by XBOOLE_0:def 4;
hence x in I \ A by XBOOLE_0:def 5, AF1; :: thesis: verum
end;
hence I \ A = (A2 `) /\ I ; :: thesis: verum
end;
reconsider CA2 = A2 ` as Element of Borel_Sets by PROB_1:20;
CA2 /\ I = Borelsubsets_help (CA2,I) ;
hence A ` in BS by F2; :: thesis: verum
end;
hence BS is compl-closed ; :: thesis: verum
end;
BS is sigma-multiplicative
proof
for A1 being SetSequence of I st rng A1 c= BS holds
Intersection A1 in BS
proof
let A1 be SetSequence of I; :: thesis: ( rng A1 c= BS implies Intersection A1 in BS )
assume G1: rng A1 c= BS ; :: thesis: Intersection A1 in BS
TT1: for n being Nat holds
( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) )
proof
let n be Nat; :: thesis: ( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) )
A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;
then A1 . n in BS by G1;
hence ( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) ) ; :: thesis: verum
end;
rng A1 c= bool REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng A1 or x in bool REAL )
assume d1: x in rng A1 ; :: thesis: x in bool REAL
bool I c= bool REAL by ZFMISC_1:67;
hence x in bool REAL by d1; :: thesis: verum
end;
then reconsider A10 = A1 as SetSequence of REAL by FUNCT_2:6;
for n being Nat holds A10 . n is Event of Borel_Sets
proof
let n be Nat; :: thesis: A10 . n is Event of Borel_Sets
ex A2 being Element of Borel_Sets st A10 . n = Borelsubsets_help (A2,I) by TT1;
hence A10 . n is Event of Borel_Sets ; :: thesis: verum
end;
then reconsider A10 = A10 as SetSequence of Borel_Sets by PROB_1:25;
set UA1 = Union (Complement A10);
for n being Nat holds (Complement A10) . n is Event of Borel_Sets
proof
let n be Nat; :: thesis: (Complement A10) . n is Event of Borel_Sets
consider A2 being Element of Borel_Sets such that
P1: A10 . n = Borelsubsets_help (A2,I) by TT1;
reconsider A1n = A10 . n as Element of Borel_Sets by P1;
A1n ` is Element of Borel_Sets by PROB_1:20;
hence (Complement A10) . n is Event of Borel_Sets by PROB_1:def 2; :: thesis: verum
end;
then Complement A10 is SetSequence of Borel_Sets by PROB_1:25;
then reconsider UA1 = Union (Complement A10) as Event of Borel_Sets by PROB_1:26;
k1: UA1 ` is Event of Borel_Sets by PROB_1:20;
reconsider IA1 = Intersection A10 as Element of Borel_Sets by k1;
s0: ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) )
proof
for x being object holds
( x in IA1 iff x in Borelsubsets_help (IA1,I) )
proof
let x be object ; :: thesis: ( x in IA1 iff x in Borelsubsets_help (IA1,I) )
thus ( x in IA1 implies x in Borelsubsets_help (IA1,I) ) :: thesis: ( x in Borelsubsets_help (IA1,I) implies x in IA1 )
proof
assume x in IA1 ; :: thesis: x in Borelsubsets_help (IA1,I)
then ( x in IA1 & x in A1 . 0 ) by PROB_1:13;
hence x in Borelsubsets_help (IA1,I) by XBOOLE_0:def 4; :: thesis: verum
end;
thus ( x in Borelsubsets_help (IA1,I) implies x in IA1 ) by XBOOLE_0:def 4; :: thesis: verum
end;
then IA1 = Borelsubsets_help (IA1,I) by TARSKI:2;
hence ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) ) ; :: thesis: verum
end;
Intersection A10 = Intersection A1
proof
for x being object holds
( x in Intersection A10 iff x in Intersection A1 )
proof
let x be object ; :: thesis: ( x in Intersection A10 iff x in Intersection A1 )
( x in Intersection A10 iff for n being Nat holds x in A10 . n ) by PROB_1:13;
then ( x in Intersection A10 iff for n being Nat holds x in A1 . n ) ;
hence ( x in Intersection A10 iff x in Intersection A1 ) by PROB_1:13; :: thesis: verum
end;
hence Intersection A10 = Intersection A1 ; :: thesis: verum
end;
hence Intersection A1 in BS by s0; :: thesis: verum
end;
hence BS is sigma-multiplicative ; :: thesis: verum
end;
hence { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is SigmaField of I by A1; :: thesis: verum