:: DYNKIN semantic presentation begin theorem Th1: :: DYNKIN:1 for Omega being non empty set for f being SetSequence of Omega for x being set holds ( x in rng f iff ex n being Element of NAT st f . n = x ) proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega for x being set holds ( x in rng f iff ex n being Element of NAT st f . n = x ) let f be SetSequence of Omega; ::_thesis: for x being set holds ( x in rng f iff ex n being Element of NAT st f . n = x ) let x be set ; ::_thesis: ( x in rng f iff ex n being Element of NAT st f . n = x ) A1: now__::_thesis:_(_x_in_rng_f_implies_ex_n_being_Element_of_NAT_st_f_._n_=_x_) assume x in rng f ; ::_thesis: ex n being Element of NAT st f . n = x then consider z being set such that A2: z in dom f and A3: x = f . z by FUNCT_1:def_3; reconsider n = z as Element of NAT by A2, FUNCT_2:def_1; take n = n; ::_thesis: f . n = x thus f . n = x by A3; ::_thesis: verum end; dom f = NAT by FUNCT_2:def_1; hence ( x in rng f iff ex n being Element of NAT st f . n = x ) by A1, FUNCT_1:def_3; ::_thesis: verum end; theorem Th2: :: DYNKIN:2 for n being Element of NAT holds n is finite proof defpred S1[ Element of NAT ] means \$1 is finite ; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then succ n is finite ; hence S1[n + 1] by NAT_1:38; ::_thesis: verum end; A2: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum end; registration let n be Element of NAT ; cluster Segm n -> finite ; coherence Segm n is finite by Th2; end; Lm1: for X being non empty set for a, b, c being Element of X holds (a,b) followed_by c is Function of NAT,X ; definition let Omega be non empty set ; let a, b, c be Subset of Omega; :: original: followed_by redefine func(a,b) followed_by c -> SetSequence of Omega; coherence (a,b) followed_by c is SetSequence of Omega proof thus (a,b) followed_by c is SetSequence of Omega ; ::_thesis: verum end; end; theorem Th3: :: DYNKIN:3 for a, b being set holds Union ((a,b) followed_by {}) = a \/ b proof let a, b be set ; ::_thesis: Union ((a,b) followed_by {}) = a \/ b rng ((a,b) followed_by {}) = {a,b,{}} by FUNCT_7:127; hence Union ((a,b) followed_by {}) = union {a,b} by MEASURE1:1 .= a \/ b by ZFMISC_1:75 ; ::_thesis: verum end; definition let Omega be non empty set ; let f be SetSequence of Omega; let X be Subset of Omega; func seqIntersection (X,f) -> SetSequence of Omega means :Def1: :: DYNKIN:def 1 for n being Element of NAT holds it . n = X /\ (f . n); existence ex b1 being SetSequence of Omega st for n being Element of NAT holds b1 . n = X /\ (f . n) proof deffunc H1( Element of NAT ) -> Element of bool Omega = X /\ (f . \$1); consider g being Function of NAT,(bool Omega) such that A1: for x being Element of NAT holds g . x = H1(x) from FUNCT_2:sch_4(); take g ; ::_thesis: for n being Element of NAT holds g . n = X /\ (f . n) let n be Element of NAT ; ::_thesis: g . n = X /\ (f . n) thus g . n = X /\ (f . n) by A1; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of Omega st ( for n being Element of NAT holds b1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds b2 . n = X /\ (f . n) ) holds b1 = b2 proof let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Element of NAT holds i1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds i2 . n = X /\ (f . n) ) implies i1 = i2 ) assume A2: for n being Element of NAT holds i1 . n = X /\ (f . n) ; ::_thesis: ( ex n being Element of NAT st not i2 . n = X /\ (f . n) or i1 = i2 ) assume A3: for n being Element of NAT holds i2 . n = X /\ (f . n) ; ::_thesis: i1 = i2 now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n let n be Element of NAT ; ::_thesis: i1 . n = i2 . n i1 . n = X /\ (f . n) by A2; hence i1 . n = i2 . n by A3; ::_thesis: verum end; hence i1 = i2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines seqIntersection DYNKIN:def_1_:_ for Omega being non empty set for f being SetSequence of Omega for X being Subset of Omega for b4 being SetSequence of Omega holds ( b4 = seqIntersection (X,f) iff for n being Element of NAT holds b4 . n = X /\ (f . n) ); begin definition let Omega be non empty set ; let f be SetSequence of Omega; :: original: disjoint_valued redefine attrf is disjoint_valued means :Def2: :: DYNKIN:def 2 for n, m being Element of NAT st n < m holds f . n misses f . m; compatibility ( f is disjoint_valued iff for n, m being Element of NAT st n < m holds f . n misses f . m ) proof thus ( f is disjoint_valued implies for n, m being Element of NAT st n < m holds f . n misses f . m ) by PROB_2:def_2; ::_thesis: ( ( for n, m being Element of NAT st n < m holds f . n misses f . m ) implies f is disjoint_valued ) assume A1: for n, m being Element of NAT st n < m holds f . n misses f . m ; ::_thesis: f is disjoint_valued now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_ f_._x_misses_f_._y let x, y be set ; ::_thesis: ( x <> y implies f . b1 misses f . b2 ) assume A2: x <> y ; ::_thesis: f . b1 misses f . b2 percases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ; suppose ( x in dom f & y in dom f ) ; ::_thesis: f . b1 misses f . b2 then reconsider n = x, m = y as Element of NAT by FUNCT_2:def_1; ( n < m or n > m ) by A2, XXREAL_0:1; hence f . x misses f . y by A1; ::_thesis: verum end; suppose ( not x in dom f or not y in dom f ) ; ::_thesis: f . b1 misses f . b2 then ( f . x = {} or f . y = {} ) by FUNCT_1:def_2; hence f . x misses f . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence f is disjoint_valued by PROB_2:def_2; ::_thesis: verum end; end; :: deftheorem Def2 defines disjoint_valued DYNKIN:def_2_:_ for Omega being non empty set for f being SetSequence of Omega holds ( f is disjoint_valued iff for n, m being Element of NAT st n < m holds f . n misses f . m ); theorem Th4: :: DYNKIN:4 for Y being non empty set for x being set holds ( x c= meet Y iff for y being Element of Y holds x c= y ) proof let Y be non empty set ; ::_thesis: for x being set holds ( x c= meet Y iff for y being Element of Y holds x c= y ) let x be set ; ::_thesis: ( x c= meet Y iff for y being Element of Y holds x c= y ) hereby ::_thesis: ( ( for y being Element of Y holds x c= y ) implies x c= meet Y ) assume A1: x c= meet Y ; ::_thesis: for y being Element of Y holds x c= y let y be Element of Y; ::_thesis: x c= y for z being set st z in x holds z in y by A1, SETFAM_1:def_1; hence x c= y by TARSKI:def_3; ::_thesis: verum end; assume A2: for y being Element of Y holds x c= y ; ::_thesis: x c= meet Y for z being set st z in x holds z in meet Y proof let z be set ; ::_thesis: ( z in x implies z in meet Y ) assume A3: z in x ; ::_thesis: z in meet Y now__::_thesis:_for_u_being_set_st_u_in_Y_holds_ z_in_u let u be set ; ::_thesis: ( u in Y implies z in u ) assume u in Y ; ::_thesis: z in u then x c= u by A2; hence z in u by A3; ::_thesis: verum end; hence z in meet Y by SETFAM_1:def_1; ::_thesis: verum end; hence x c= meet Y by TARSKI:def_3; ::_thesis: verum end; notation let x be set ; synonym intersection_stable x for cap-closed ; end; definition let Omega be non empty set ; let f be SetSequence of Omega; let n be Nat; func disjointify (f,n) -> Subset of Omega equals :: DYNKIN:def 3 (f . n) \ (union (rng (f | n))); coherence (f . n) \ (union (rng (f | n))) is Subset of Omega ; end; :: deftheorem defines disjointify DYNKIN:def_3_:_ for Omega being non empty set for f being SetSequence of Omega for n being Nat holds disjointify (f,n) = (f . n) \ (union (rng (f | n))); definition let Omega be non empty set ; let g be SetSequence of Omega; func disjointify g -> SetSequence of Omega means :Def4: :: DYNKIN:def 4 for n being Nat holds it . n = disjointify (g,n); existence ex b1 being SetSequence of Omega st for n being Nat holds b1 . n = disjointify (g,n) proof deffunc H1( Nat) -> Subset of Omega = disjointify (g,\$1); consider f being Function of NAT,(bool Omega) such that A1: for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for n being Nat holds f . n = disjointify (g,n) let n be Nat; ::_thesis: f . n = disjointify (g,n) n in NAT by ORDINAL1:def_12; hence f . n = disjointify (g,n) by A1; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = disjointify (g,n) ) & ( for n being Nat holds b2 . n = disjointify (g,n) ) holds b1 = b2 proof let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Nat holds i1 . n = disjointify (g,n) ) & ( for n being Nat holds i2 . n = disjointify (g,n) ) implies i1 = i2 ) assume A2: for n being Nat holds i1 . n = disjointify (g,n) ; ::_thesis: ( ex n being Nat st not i2 . n = disjointify (g,n) or i1 = i2 ) assume A3: for n being Nat holds i2 . n = disjointify (g,n) ; ::_thesis: i1 = i2 now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n let n be Element of NAT ; ::_thesis: i1 . n = i2 . n i1 . n = disjointify (g,n) by A2; hence i1 . n = i2 . n by A3; ::_thesis: verum end; hence i1 = i2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines disjointify DYNKIN:def_4_:_ for Omega being non empty set for g, b3 being SetSequence of Omega holds ( b3 = disjointify g iff for n being Nat holds b3 . n = disjointify (g,n) ); theorem Th5: :: DYNKIN:5 for Omega being non empty set for f being SetSequence of Omega for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n))) proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n))) let f be SetSequence of Omega; ::_thesis: for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n))) let n be Nat; ::_thesis: (disjointify f) . n = (f . n) \ (union (rng (f | n))) (disjointify f) . n = disjointify (f,n) by Def4; hence (disjointify f) . n = (f . n) \ (union (rng (f | n))) ; ::_thesis: verum end; theorem Th6: :: DYNKIN:6 for Omega being non empty set for f being SetSequence of Omega holds disjointify f is V56() proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds disjointify f is V56() let f be SetSequence of Omega; ::_thesis: disjointify f is V56() now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_ (disjointify_f)_._n_misses_(disjointify_f)_._m let n, m be Element of NAT ; ::_thesis: ( n < m implies (disjointify f) . n misses (disjointify f) . m ) assume n < m ; ::_thesis: (disjointify f) . n misses (disjointify f) . m then A1: n in m by NAT_1:44; dom f = NAT by FUNCT_2:def_1; then dom (f | m) = m /\ NAT by RELAT_1:61; then n in dom (f | m) by A1, XBOOLE_0:def_4; then A2: (f | m) . n in rng (f | m) by FUNCT_1:def_3; (f | m) . n = f . n by A1, FUNCT_1:49; then f . n misses (f . m) \ (union (rng (f | m))) by A2, XBOOLE_1:85, ZFMISC_1:74; then A3: f . n misses (disjointify f) . m by Th5; (f . n) \ (union (rng (f | n))) c= f . n by XBOOLE_1:36; then (disjointify f) . n c= f . n by Th5; hence (disjointify f) . n misses (disjointify f) . m by A3, XBOOLE_1:63; ::_thesis: verum end; hence disjointify f is V56() by Def2; ::_thesis: verum end; theorem Th7: :: DYNKIN:7 for Omega being non empty set for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f) proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f) let f be SetSequence of Omega; ::_thesis: union (rng (disjointify f)) = union (rng f) A1: dom f = NAT by FUNCT_2:def_1; A2: dom (disjointify f) = NAT by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_ x_in_union_(rng_(disjointify_f)) let x be set ; ::_thesis: ( x in union (rng f) implies x in union (rng (disjointify f)) ) defpred S1[ Nat] means x in f . \$1; assume x in union (rng f) ; ::_thesis: x in union (rng (disjointify f)) then consider y being set such that A3: x in y and A4: y in rng f by TARSKI:def_4; consider z being set such that A5: z in dom f and A6: y = f . z by A4, FUNCT_1:def_3; reconsider n = z as Element of NAT by A5, FUNCT_2:def_1; A7: ex k being Nat st S1[k] proof take n ; ::_thesis: S1[n] thus S1[n] by A3, A6; ::_thesis: verum end; consider k being Nat such that A8: ( S1[k] & ( for m being Nat st S1[m] holds k <= m ) ) from NAT_1:sch_5(A7); now__::_thesis:_not_x_in_union_(rng_(f_|_k)) assume x in union (rng (f | k)) ; ::_thesis: contradiction then consider y being set such that A9: x in y and A10: y in rng (f | k) by TARSKI:def_4; consider z being set such that A11: z in dom (f | k) and A12: y = (f | k) . z by A10, FUNCT_1:def_3; dom (f | k) c= NAT by A1, RELAT_1:60; then reconsider n = z as Element of NAT by A11; dom (f | k) c= k by RELAT_1:58; then ( n < k & y = f . n ) by A11, A12, FUNCT_1:49, NAT_1:44; hence contradiction by A8, A9; ::_thesis: verum end; then x in (f . k) \ (union (rng (f | k))) by A8, XBOOLE_0:def_5; then A13: x in (disjointify f) . k by Th5; k in NAT by ORDINAL1:def_12; then (disjointify f) . k in rng (disjointify f) by A2, FUNCT_1:def_3; hence x in union (rng (disjointify f)) by A13, TARSKI:def_4; ::_thesis: verum end; then A14: union (rng f) c= union (rng (disjointify f)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_union_(rng_(disjointify_f))_holds_ x_in_union_(rng_f) let x be set ; ::_thesis: ( x in union (rng (disjointify f)) implies x in union (rng f) ) assume x in union (rng (disjointify f)) ; ::_thesis: x in union (rng f) then consider y being set such that A15: x in y and A16: y in rng (disjointify f) by TARSKI:def_4; consider z being set such that A17: z in dom (disjointify f) and A18: y = (disjointify f) . z by A16, FUNCT_1:def_3; reconsider n = z as Element of NAT by A17, FUNCT_2:def_1; A19: ( (f . n) \ (union (rng (f | n))) c= f . n & f . n in rng f ) by A1, FUNCT_1:def_3, XBOOLE_1:36; x in (f . n) \ (union (rng (f | n))) by A15, A18, Th5; hence x in union (rng f) by A19, TARSKI:def_4; ::_thesis: verum end; then union (rng (disjointify f)) c= union (rng f) by TARSKI:def_3; hence union (rng (disjointify f)) = union (rng f) by A14, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th8: :: DYNKIN:8 for Omega being non empty set for x, y being Subset of Omega st x misses y holds (x,y) followed_by ({} Omega) is V56() proof let Omega be non empty set ; ::_thesis: for x, y being Subset of Omega st x misses y holds (x,y) followed_by ({} Omega) is V56() let x, y be Subset of Omega; ::_thesis: ( x misses y implies (x,y) followed_by ({} Omega) is V56() ) assume A1: x misses y ; ::_thesis: (x,y) followed_by ({} Omega) is V56() reconsider r = (x,y) followed_by ({} Omega) as Function of NAT,(bool Omega) ; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_ r_._n_misses_r_._m let n, m be Element of NAT ; ::_thesis: ( n < m implies r . n misses r . m ) A2: ( m > 1 implies r . m = {} ) by FUNCT_7:124; assume A3: n < m ; ::_thesis: r . n misses r . m A4: now__::_thesis:_(_(_m_=_0_or_m_=_1_)_implies_(_n_=_0_&_m_=_1_)_) assume A5: ( m = 0 or m = 1 ) ; ::_thesis: ( n = 0 & m = 1 ) 0 + 1 = 1 ; then n <= 0 by A3, A5, NAT_1:13; hence ( n = 0 & m = 1 ) by A3, A5, NAT_1:3; ::_thesis: verum end; r . 0 = x by FUNCT_7:122; hence r . n misses r . m by A1, A4, A2, FUNCT_7:123, NAT_1:25, XBOOLE_1:65; ::_thesis: verum end; hence (x,y) followed_by ({} Omega) is V56() by Def2; ::_thesis: verum end; theorem Th9: :: DYNKIN:9 for Omega being non empty set for f being SetSequence of Omega st f is V56() holds for X being Subset of Omega holds seqIntersection (X,f) is V56() proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega st f is V56() holds for X being Subset of Omega holds seqIntersection (X,f) is V56() let f be SetSequence of Omega; ::_thesis: ( f is V56() implies for X being Subset of Omega holds seqIntersection (X,f) is V56() ) assume A1: f is V56() ; ::_thesis: for X being Subset of Omega holds seqIntersection (X,f) is V56() let X be Subset of Omega; ::_thesis: seqIntersection (X,f) is V56() for n, m being Element of NAT st n < m holds (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m proof let n, m be Element of NAT ; ::_thesis: ( n < m implies (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m ) assume n < m ; ::_thesis: (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m then f . n misses f . m by A1, PROB_2:def_2; then A2: X /\ (f . n) misses f . m by XBOOLE_1:74; ( (seqIntersection (X,f)) . n = X /\ (f . n) & (seqIntersection (X,f)) . m = X /\ (f . m) ) by Def1; hence (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m by A2, XBOOLE_1:74; ::_thesis: verum end; hence seqIntersection (X,f) is V56() by Def2; ::_thesis: verum end; theorem Th10: :: DYNKIN:10 for Omega being non empty set for f being SetSequence of Omega for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f)) proof let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f)) let f be SetSequence of Omega; ::_thesis: for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f)) let X be Subset of Omega; ::_thesis: X /\ (Union f) = Union (seqIntersection (X,f)) A1: dom f = NAT by FUNCT_2:def_1; now__::_thesis:_for_z_being_set_st_z_in_Union_(seqIntersection_(X,f))_holds_ z_in_X_/\_(Union_f) reconsider g = seqIntersection (X,f) as SetSequence of Omega ; let z be set ; ::_thesis: ( z in Union (seqIntersection (X,f)) implies z in X /\ (Union f) ) assume z in Union (seqIntersection (X,f)) ; ::_thesis: z in X /\ (Union f) then consider u being set such that A2: z in u and A3: u in rng g by TARSKI:def_4; consider v being set such that A4: v in dom g and A5: u = g . v by A3, FUNCT_1:def_3; reconsider n = v as Element of NAT by A4, FUNCT_2:def_1; A6: z in X /\ (f . n) by A2, A5, Def1; then A7: z in X by XBOOLE_0:def_4; A8: f . n in rng f by A1, FUNCT_1:def_3; z in f . n by A6, XBOOLE_0:def_4; then z in Union f by A8, TARSKI:def_4; hence z in X /\ (Union f) by A7, XBOOLE_0:def_4; ::_thesis: verum end; then A9: Union (seqIntersection (X,f)) c= X /\ (Union f) by TARSKI:def_3; A10: dom (seqIntersection (X,f)) = NAT by FUNCT_2:def_1; now__::_thesis:_for_z_being_set_st_z_in_X_/\_(Union_f)_holds_ z_in_Union_(seqIntersection_(X,f)) let z be set ; ::_thesis: ( z in X /\ (Union f) implies z in Union (seqIntersection (X,f)) ) assume A11: z in X /\ (Union f) ; ::_thesis: z in Union (seqIntersection (X,f)) then z in union (rng f) by XBOOLE_0:def_4; then consider u being set such that A12: z in u and A13: u in rng f by TARSKI:def_4; consider v being set such that A14: v in dom f and A15: u = f . v by A13, FUNCT_1:def_3; reconsider n = v as Element of NAT by A14, FUNCT_2:def_1; X /\ (f . n) = (seqIntersection (X,f)) . n by Def1; then A16: X /\ (f . n) in rng (seqIntersection (X,f)) by A10, FUNCT_1:def_3; z in X by A11, XBOOLE_0:def_4; then z in X /\ (f . n) by A12, A15, XBOOLE_0:def_4; hence z in Union (seqIntersection (X,f)) by A16, TARSKI:def_4; ::_thesis: verum end; then X /\ (Union f) c= Union (seqIntersection (X,f)) by TARSKI:def_3; hence X /\ (Union f) = Union (seqIntersection (X,f)) by A9, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let Omega be non empty set ; mode Dynkin_System of Omega -> Subset-Family of Omega means :Def5: :: DYNKIN:def 5 ( ( for f being SetSequence of Omega st rng f c= it & f is V56() holds Union f in it ) & ( for X being Subset of Omega st X in it holds X ` in it ) & {} in it ); existence ex b1 being Subset-Family of Omega st ( ( for f being SetSequence of Omega st rng f c= b1 & f is V56() holds Union f in b1 ) & ( for X being Subset of Omega st X in b1 holds X ` in b1 ) & {} in b1 ) proof reconsider D = bool Omega as non empty Subset-Family of Omega ; take D ; ::_thesis: ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds Union f in D ) & ( for X being Subset of Omega st X in D holds X ` in D ) & {} in D ) {} c= Omega by XBOOLE_1:2; hence ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds Union f in D ) & ( for X being Subset of Omega st X in D holds X ` in D ) & {} in D ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines Dynkin_System DYNKIN:def_5_:_ for Omega being non empty set for b2 being Subset-Family of Omega holds ( b2 is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b2 & f is V56() holds Union f in b2 ) & ( for X being Subset of Omega st X in b2 holds X ` in b2 ) & {} in b2 ) ); registration let Omega be non empty set ; cluster -> non empty for Dynkin_System of Omega; coherence for b1 being Dynkin_System of Omega holds not b1 is empty by Def5; end; theorem Th11: :: DYNKIN:11 for Omega being non empty set holds bool Omega is Dynkin_System of Omega proof let Omega be non empty set ; ::_thesis: bool Omega is Dynkin_System of Omega A1: ( {} c= Omega & bool Omega c= bool Omega ) by XBOOLE_1:2; ( ( for f being SetSequence of Omega st rng f c= bool Omega & f is V56() holds Union f in bool Omega ) & ( for X being Subset of Omega st X in bool Omega holds X ` in bool Omega ) ) ; hence bool Omega is Dynkin_System of Omega by A1, Def5; ::_thesis: verum end; theorem Th12: :: DYNKIN:12 for F, Omega being non empty set st ( for Y being set st Y in F holds Y is Dynkin_System of Omega ) holds meet F is Dynkin_System of Omega proof let F, Omega be non empty set ; ::_thesis: ( ( for Y being set st Y in F holds Y is Dynkin_System of Omega ) implies meet F is Dynkin_System of Omega ) assume A1: for Y being set st Y in F holds Y is Dynkin_System of Omega ; ::_thesis: meet F is Dynkin_System of Omega now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_ {}_in_Y let Y be set ; ::_thesis: ( Y in F implies {} in Y ) assume Y in F ; ::_thesis: {} in Y then Y is Dynkin_System of Omega by A1; hence {} in Y by Def5; ::_thesis: verum end; then A2: {} in meet F by SETFAM_1:def_1; A3: now__::_thesis:_for_f_being_SetSequence_of_Omega_st_rng_f_c=_meet_F_&_f_is_V56()_holds_ Union_f_in_meet_F let f be SetSequence of Omega; ::_thesis: ( rng f c= meet F & f is V56() implies Union f in meet F ) assume that A4: rng f c= meet F and A5: f is V56() ; ::_thesis: Union f in meet F now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_ Union_f_in_Y let Y be set ; ::_thesis: ( Y in F implies Union f in Y ) assume A6: Y in F ; ::_thesis: Union f in Y meet F c= Y by A6, SETFAM_1:3; then A7: rng f c= Y by A4, XBOOLE_1:1; Y is Dynkin_System of Omega by A1, A6; hence Union f in Y by A5, A7, Def5; ::_thesis: verum end; hence Union f in meet F by SETFAM_1:def_1; ::_thesis: verum end; A8: now__::_thesis:_for_X_being_Subset_of_Omega_st_X_in_meet_F_holds_ X_`_in_meet_F let X be Subset of Omega; ::_thesis: ( X in meet F implies X ` in meet F ) assume A9: X in meet F ; ::_thesis: X ` in meet F for Y being set st Y in F holds X ` in Y proof let Y be set ; ::_thesis: ( Y in F implies X ` in Y ) assume Y in F ; ::_thesis: X ` in Y then ( Y is Dynkin_System of Omega & meet F c= Y ) by A1, SETFAM_1:3; hence X ` in Y by A9, Def5; ::_thesis: verum end; hence X ` in meet F by SETFAM_1:def_1; ::_thesis: verum end; set Y = the Element of F; A10: meet F c= the Element of F by SETFAM_1:3; the Element of F is Dynkin_System of Omega by A1; then meet F is Subset-Family of Omega by A10, XBOOLE_1:1; hence meet F is Dynkin_System of Omega by A3, A8, A2, Def5; ::_thesis: verum end; theorem Th13: :: DYNKIN:13 for Omega being non empty set for A, B being Subset of Omega for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \ B in D proof let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \ B in D let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \ B in D let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \ B in D ) assume that A1: D is Dynkin_System of Omega and A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \ B in D ) assume that A3: A in D and A4: B in D ; ::_thesis: A \ B in D B ` in D by A1, A4, Def5; then A /\ (B `) in D by A2, A3, FINSUB_1:def_2; hence A \ B in D by SUBSET_1:13; ::_thesis: verum end; theorem Th14: :: DYNKIN:14 for Omega being non empty set for A, B being Subset of Omega for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \/ B in D proof let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \/ B in D let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds A \/ B in D let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \/ B in D ) assume that A1: D is Dynkin_System of Omega and A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \/ B in D ) assume ( A in D & B in D ) ; ::_thesis: A \/ B in D then ( A ` in D & B ` in D ) by A1, Def5; then (A `) /\ (B `) in D by A2, FINSUB_1:def_2; then (A \/ B) ` in D by XBOOLE_1:53; then ((A \/ B) `) ` in D by A1, Def5; hence A \/ B in D ; ::_thesis: verum end; theorem Th15: :: DYNKIN:15 for Omega being non empty set for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for x being finite set st x c= D holds union x in D proof let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for x being finite set st x c= D holds union x in D let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for x being finite set st x c= D holds union x in D ) assume that A1: D is Dynkin_System of Omega and A2: D is intersection_stable ; ::_thesis: for x being finite set st x c= D holds union x in D defpred S1[ set ] means union \$1 in D; let x be finite set ; ::_thesis: ( x c= D implies union x in D ) assume A3: x c= D ; ::_thesis: union x in D A4: for y, b being set st y in x & b c= x & S1[b] holds S1[b \/ {y}] proof let y, b be set ; ::_thesis: ( y in x & b c= x & S1[b] implies S1[b \/ {y}] ) assume that A5: y in x and b c= x and A6: union b in D ; ::_thesis: S1[b \/ {y}] y in D by A3, A5; then reconsider y1 = y as Subset of Omega ; reconsider unionb = union b as Subset of Omega by A6; ( union {y} = y & unionb \/ y1 in D ) by A1, A2, A3, A5, A6, Th14, ZFMISC_1:25; hence S1[b \/ {y}] by ZFMISC_1:78; ::_thesis: verum end; A7: x is finite ; A8: S1[ {} ] by A1, Def5, ZFMISC_1:2; thus S1[x] from FINSET_1:sch_2(A7, A8, A4); ::_thesis: verum end; theorem Th16: :: DYNKIN:16 for Omega being non empty set for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for f being SetSequence of Omega st rng f c= D holds rng (disjointify f) c= D proof let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for f being SetSequence of Omega st rng f c= D holds rng (disjointify f) c= D let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds rng (disjointify f) c= D ) assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds rng (disjointify f) c= D let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies rng (disjointify f) c= D ) assume A2: rng f c= D ; ::_thesis: rng (disjointify f) c= D A3: for n being Element of NAT holds (disjointify f) . n in D proof let n be Element of NAT ; ::_thesis: (disjointify f) . n in D A4: rng (f | n) c= rng f by RELAT_1:70; ( dom (f | n) c= Segm n & rng f is Subset-Family of Omega ) by RELAT_1:58, RELAT_1:def_19; then rng (f | n) is finite Subset-Family of Omega by A4, XBOOLE_1:1; then A5: union (rng (f | n)) in D by A1, A2, A4, Th15, XBOOLE_1:1; then reconsider urf = union (rng (f | n)) as Subset of Omega ; dom f = NAT by FUNCT_2:def_1; then f . n in rng f by FUNCT_1:def_3; then (f . n) \ urf in D by A1, A2, A5, Th13; hence (disjointify f) . n in D by Th5; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_(disjointify_f)_holds_ y_in_D let y be set ; ::_thesis: ( y in rng (disjointify f) implies y in D ) assume y in rng (disjointify f) ; ::_thesis: y in D then consider x being set such that A6: x in dom (disjointify f) and A7: y = (disjointify f) . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A6, FUNCT_2:def_1; y = (disjointify f) . n by A7; hence y in D by A3; ::_thesis: verum end; hence rng (disjointify f) c= D by TARSKI:def_3; ::_thesis: verum end; theorem Th17: :: DYNKIN:17 for Omega being non empty set for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for f being SetSequence of Omega st rng f c= D holds union (rng f) in D proof let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds for f being SetSequence of Omega st rng f c= D holds union (rng f) in D let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds union (rng f) in D ) assume that A1: D is Dynkin_System of Omega and A2: D is intersection_stable ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds union (rng f) in D let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies union (rng f) in D ) assume rng f c= D ; ::_thesis: union (rng f) in D then A3: rng (disjointify f) c= D by A1, A2, Th16; disjointify f is V56() by Th6; then Union (disjointify f) in D by A1, A3, Def5; hence union (rng f) in D by Th7; ::_thesis: verum end; theorem Th18: :: DYNKIN:18 for Omega being non empty set for D being Dynkin_System of Omega for x, y being Element of D st x misses y holds x \/ y in D proof let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega for x, y being Element of D st x misses y holds x \/ y in D let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x misses y holds x \/ y in D reconsider e = {} as Element of D by Def5; let x, y be Element of D; ::_thesis: ( x misses y implies x \/ y in D ) reconsider x1 = x as Subset of Omega ; reconsider y1 = y as Subset of Omega ; reconsider r = (x1,y1) followed_by ({} Omega) as SetSequence of Omega ; (x,y) followed_by e is Function of NAT,D by Lm1; then A1: rng r c= D by RELAT_1:def_19; assume x misses y ; ::_thesis: x \/ y in D then r is V56() by Th8; then Union r in D by A1, Def5; hence x \/ y in D by Th3; ::_thesis: verum end; theorem Th19: :: DYNKIN:19 for Omega being non empty set for D being Dynkin_System of Omega for x, y being Element of D st x c= y holds y \ x in D proof let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega for x, y being Element of D st x c= y holds y \ x in D let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x c= y holds y \ x in D let x, y be Element of D; ::_thesis: ( x c= y implies y \ x in D ) A1: (x \/ (y `)) ` = (x `) /\ ((y `) `) by XBOOLE_1:53 .= y \ x by SUBSET_1:13 ; assume x c= y ; ::_thesis: y \ x in D then x c= (y `) ` ; then A2: x misses y ` by SUBSET_1:23; y ` in D by Def5; then x \/ (y `) in D by A2, Th18; hence y \ x in D by A1, Def5; ::_thesis: verum end; begin theorem Th20: :: DYNKIN:20 for Omega being non empty set for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds D is SigmaField of Omega proof let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds D is SigmaField of Omega let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega ) assume that A1: D is Dynkin_System of Omega and A2: D is intersection_stable ; ::_thesis: D is SigmaField of Omega A3: for f being SetSequence of Omega st rng f c= D holds Intersection f in D proof let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies Intersection f in D ) assume A4: rng f c= D ; ::_thesis: Intersection f in D A5: for n being Element of NAT holds (f . n) ` in D proof let n be Element of NAT ; ::_thesis: (f . n) ` in D f . n in rng f by NAT_1:51; hence (f . n) ` in D by A1, A4, Def5; ::_thesis: verum end; A6: for n being Element of NAT holds (Complement f) . n in D proof let n be Element of NAT ; ::_thesis: (Complement f) . n in D (Complement f) . n = (f . n) ` by PROB_1:def_2; hence (Complement f) . n in D by A5; ::_thesis: verum end; for x being set st x in rng (Complement f) holds x in D proof let x be set ; ::_thesis: ( x in rng (Complement f) implies x in D ) assume x in rng (Complement f) ; ::_thesis: x in D then consider z being set such that A7: z in dom (Complement f) and A8: x = (Complement f) . z by FUNCT_1:def_3; reconsider n = z as Element of NAT by A7, FUNCT_2:def_1; x = (Complement f) . n by A8; hence x in D by A6; ::_thesis: verum end; then rng (Complement f) c= D by TARSKI:def_3; then Union (Complement f) in D by A1, A2, Th17; then (Union (Complement f)) ` in D by A1, Def5; hence Intersection f in D by PROB_1:def_3; ::_thesis: verum end; for X being Subset of Omega st X in D holds X ` in D by A1, Def5; hence D is SigmaField of Omega by A3, PROB_1:15; ::_thesis: verum end; definition let Omega be non empty set ; let E be Subset-Family of Omega; func generated_Dynkin_System E -> Dynkin_System of Omega means :Def6: :: DYNKIN:def 6 ( E c= it & ( for D being Dynkin_System of Omega st E c= D holds it c= D ) ); existence ex b1 being Dynkin_System of Omega st ( E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds b1 c= D ) ) proof defpred S1[ set ] means ( \$1 is Dynkin_System of Omega & E c= \$1 ); consider Y being set such that A1: for x being set holds ( x in Y iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1(); bool Omega is Dynkin_System of Omega by Th11; then reconsider Y = Y as non empty set by A1; for z being set st z in Y holds z is Dynkin_System of Omega by A1; then reconsider I = meet Y as Dynkin_System of Omega by Th12; take I ; ::_thesis: ( E c= I & ( for D being Dynkin_System of Omega st E c= D holds I c= D ) ) for y being Element of Y holds E c= y by A1; hence E c= I by Th4; ::_thesis: for D being Dynkin_System of Omega st E c= D holds I c= D let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies I c= D ) assume E c= D ; ::_thesis: I c= D then D in Y by A1; hence I c= D by SETFAM_1:3; ::_thesis: verum end; uniqueness for b1, b2 being Dynkin_System of Omega st E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds b1 c= D ) & E c= b2 & ( for D being Dynkin_System of Omega st E c= D holds b2 c= D ) holds b1 = b2 proof let I1, I2 be Dynkin_System of Omega; ::_thesis: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds I1 c= D ) & E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds I2 c= D ) implies I1 = I2 ) assume A2: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds I1 c= D ) ) ; ::_thesis: ( not E c= I2 or ex D being Dynkin_System of Omega st ( E c= D & not I2 c= D ) or I1 = I2 ) assume ( E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds I2 c= D ) ) ; ::_thesis: I1 = I2 then ( I1 c= I2 & I2 c= I1 ) by A2; hence I1 = I2 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def_6_:_ for Omega being non empty set for E being Subset-Family of Omega for b3 being Dynkin_System of Omega holds ( b3 = generated_Dynkin_System E iff ( E c= b3 & ( for D being Dynkin_System of Omega st E c= D holds b3 c= D ) ) ); definition let Omega be non empty set ; let G be set ; let X be Subset of Omega; func DynSys (X,G) -> Subset-Family of Omega means :Def7: :: DYNKIN:def 7 for A being Subset of Omega holds ( A in it iff A /\ X in G ); existence ex b1 being Subset-Family of Omega st for A being Subset of Omega holds ( A in b1 iff A /\ X in G ) proof defpred S1[ set ] means \$1 /\ X in G; consider I being set such that A1: for x being set holds ( x in I iff ( x in bool Omega & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in I holds x in bool Omega by A1; then reconsider I = I as Subset-Family of Omega by TARSKI:def_3; take I ; ::_thesis: for A being Subset of Omega holds ( A in I iff A /\ X in G ) let A be Subset of Omega; ::_thesis: ( A in I iff A /\ X in G ) thus ( A in I iff A /\ X in G ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of Omega st ( for A being Subset of Omega holds ( A in b1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds ( A in b2 iff A /\ X in G ) ) holds b1 = b2 proof let I1, I2 be Subset-Family of Omega; ::_thesis: ( ( for A being Subset of Omega holds ( A in I1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds ( A in I2 iff A /\ X in G ) ) implies I1 = I2 ) assume A2: for A being Subset of Omega holds ( A in I1 iff A /\ X in G ) ; ::_thesis: ( ex A being Subset of Omega st ( ( A in I2 implies A /\ X in G ) implies ( A /\ X in G & not A in I2 ) ) or I1 = I2 ) assume A3: for A being Subset of Omega holds ( A in I2 iff A /\ X in G ) ; ::_thesis: I1 = I2 now__::_thesis:_for_A_being_Subset_of_Omega_holds_ (_A_in_I1_iff_A_in_I2_) let A be Subset of Omega; ::_thesis: ( A in I1 iff A in I2 ) ( A in I1 iff A /\ X in G ) by A2; hence ( A in I1 iff A in I2 ) by A3; ::_thesis: verum end; hence I1 = I2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def7 defines DynSys DYNKIN:def_7_:_ for Omega being non empty set for G being set for X being Subset of Omega for b4 being Subset-Family of Omega holds ( b4 = DynSys (X,G) iff for A being Subset of Omega holds ( A in b4 iff A /\ X in G ) ); definition let Omega be non empty set ; let G be Dynkin_System of Omega; let X be Element of G; :: original: DynSys redefine func DynSys (X,G) -> Dynkin_System of Omega; coherence DynSys (X,G) is Dynkin_System of Omega proof A1: for f being SetSequence of Omega st rng f c= DynSys (X,G) & f is V56() holds Union f in DynSys (X,G) proof reconsider X1 = X as Subset of Omega ; let f be SetSequence of Omega; ::_thesis: ( rng f c= DynSys (X,G) & f is V56() implies Union f in DynSys (X,G) ) assume that A2: rng f c= DynSys (X,G) and A3: f is V56() ; ::_thesis: Union f in DynSys (X,G) now__::_thesis:_for_x_being_set_st_x_in_rng_(seqIntersection_(X1,f))_holds_ x_in_G let x be set ; ::_thesis: ( x in rng (seqIntersection (X1,f)) implies x in G ) assume x in rng (seqIntersection (X1,f)) ; ::_thesis: x in G then consider n being Element of NAT such that A4: x = (seqIntersection (X1,f)) . n by Th1; A5: f . n in rng f by Th1; x = X /\ (f . n) by A4, Def1; hence x in G by A2, A5, Def7; ::_thesis: verum end; then A6: rng (seqIntersection (X1,f)) c= G by TARSKI:def_3; seqIntersection (X,f) is V56() by A3, Th9; then Union (seqIntersection (X1,f)) in G by A6, Def5; then X /\ (Union f) in G by Th10; hence Union f in DynSys (X,G) by Def7; ::_thesis: verum end; A7: for A being Subset of Omega st A in DynSys (X,G) holds A ` in DynSys (X,G) proof let A be Subset of Omega; ::_thesis: ( A in DynSys (X,G) implies A ` in DynSys (X,G) ) X misses X ` by XBOOLE_1:79; then A8: X /\ (X `) = {} by XBOOLE_0:def_7; assume A in DynSys (X,G) ; ::_thesis: A ` in DynSys (X,G) then X /\ A in G by Def7; then A9: X \ (X /\ A) in G by Th19, XBOOLE_1:17; X \ (X /\ A) = X /\ ((X /\ A) `) by SUBSET_1:13 .= X /\ ((X `) \/ (A `)) by XBOOLE_1:54 .= (X /\ (X `)) \/ (X /\ (A `)) by XBOOLE_1:23 .= X /\ (A `) by A8 ; hence A ` in DynSys (X,G) by A9, Def7; ::_thesis: verum end; ( {} /\ X = {} & {} in G ) by Def5; then {} in DynSys (X,G) by Def7; hence DynSys (X,G) is Dynkin_System of Omega by A1, A7, Def5; ::_thesis: verum end; end; theorem Th21: :: DYNKIN:21 for Omega being non empty set for E being Subset-Family of Omega for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E proof let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E let X, Y be Subset of Omega; ::_thesis: ( X in E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E ) assume that A1: X in E and A2: Y in generated_Dynkin_System E and A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ; E c= generated_Dynkin_System E by Def6; then reconsider X = X as Element of G by A1; for x being set st x in E holds x in DynSys (X,G) proof let x be set ; ::_thesis: ( x in E implies x in DynSys (X,G) ) assume A4: x in E ; ::_thesis: x in DynSys (X,G) then reconsider x = x as Subset of Omega ; A5: E c= G by Def6; x /\ X in E by A1, A3, A4, FINSUB_1:def_2; hence x in DynSys (X,G) by A5, Def7; ::_thesis: verum end; then E c= DynSys (X,G) by TARSKI:def_3; then generated_Dynkin_System E c= DynSys (X,G) by Def6; hence X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum end; theorem Th22: :: DYNKIN:22 for Omega being non empty set for E being Subset-Family of Omega for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E proof let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds X /\ Y in generated_Dynkin_System E let X, Y be Subset of Omega; ::_thesis: ( X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E ) assume that A1: X in generated_Dynkin_System E and A2: Y in generated_Dynkin_System E and A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ; defpred S1[ set ] means ex X being Element of G st \$1 = DynSys (X,G); consider h being set such that A4: for x being set holds ( x in h iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1(); A5: for Y being set st Y in h holds Y is Dynkin_System of Omega proof let Y be set ; ::_thesis: ( Y in h implies Y is Dynkin_System of Omega ) assume Y in h ; ::_thesis: Y is Dynkin_System of Omega then ex X being Element of G st Y = DynSys (X,G) by A4; hence Y is Dynkin_System of Omega ; ::_thesis: verum end; not h is empty proof set X = the Element of G; DynSys ( the Element of G,G) in h by A4; hence not h is empty ; ::_thesis: verum end; then reconsider h = h as non empty set ; DynSys (X,G) in h by A1, A4; then A6: meet h c= DynSys (X,G) by SETFAM_1:3; for x being set st x in E holds x in meet h proof let x be set ; ::_thesis: ( x in E implies x in meet h ) assume A7: x in E ; ::_thesis: x in meet h for Y being set st Y in h holds x in Y proof let Y be set ; ::_thesis: ( Y in h implies x in Y ) assume Y in h ; ::_thesis: x in Y then consider X being Element of G such that A8: Y = DynSys (X,G) by A4; x /\ X in G by A3, A7, Th21; hence x in Y by A7, A8, Def7; ::_thesis: verum end; hence x in meet h by SETFAM_1:def_1; ::_thesis: verum end; then A9: E c= meet h by TARSKI:def_3; meet h is Dynkin_System of Omega by A5, Th12; then G c= meet h by A9, Def6; then G c= DynSys (X,G) by A6, XBOOLE_1:1; hence X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum end; theorem Th23: :: DYNKIN:23 for Omega being non empty set for E being Subset-Family of Omega st E is intersection_stable holds generated_Dynkin_System E is intersection_stable proof let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds generated_Dynkin_System E is intersection_stable let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies generated_Dynkin_System E is intersection_stable ) assume A1: E is intersection_stable ; ::_thesis: generated_Dynkin_System E is intersection_stable reconsider G = generated_Dynkin_System E as Subset-Family of Omega ; for a, b being set st a in G & b in G holds a /\ b in G by A1, Th22; hence generated_Dynkin_System E is intersection_stable by FINSUB_1:def_2; ::_thesis: verum end; theorem :: DYNKIN:24 for Omega being non empty set for E being Subset-Family of Omega st E is intersection_stable holds for D being Dynkin_System of Omega st E c= D holds sigma E c= D proof let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds for D being Dynkin_System of Omega st E c= D holds sigma E c= D let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies for D being Dynkin_System of Omega st E c= D holds sigma E c= D ) assume A1: E is intersection_stable ; ::_thesis: for D being Dynkin_System of Omega st E c= D holds sigma E c= D reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ; G is intersection_stable by A1, Th23; then A2: G is SigmaField of Omega by Th20; let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies sigma E c= D ) assume E c= D ; ::_thesis: sigma E c= D then A3: G c= D by Def6; E c= G by Def6; then sigma E c= G by A2, PROB_1:def_9; hence sigma E c= D by A3, XBOOLE_1:1; ::_thesis: verum end;