Metamath Proof Explorer

Theorem dynkin

Description: Dynkin's lambda-pi theorem: if a lambda-system contains a pi-system, it also contains the sigma-algebra generated by that pi-system. (Contributed by Thierry Arnoux, 16-Jun-2020)

Ref Expression
Hypotheses dynkin.p 
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
dynkin.l 
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
dynkin.o 
|- ( ph -> O e. V )
dynkin.1 
|- ( ph -> S e. L )
dynkin.2 
|- ( ph -> T e. P )
dynkin.3 
|- ( ph -> T C_ S )
Assertion dynkin 
|- ( ph -> |^| { u e. ( sigAlgebra ` O ) | T C_ u } C_ S )

Proof

Step Hyp Ref Expression
1 dynkin.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2 dynkin.l 
 |-  L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
3 dynkin.o 
 |-  ( ph -> O e. V )
4 dynkin.1 
 |-  ( ph -> S e. L )
5 dynkin.2 
 |-  ( ph -> T e. P )
6 dynkin.3 
 |-  ( ph -> T C_ S )
7 sseq2 
 |-  ( v = t -> ( T C_ v <-> T C_ t ) )
8 7 cbvrabv 
 |-  { v e. L | T C_ v } = { t e. L | T C_ t }
9 8 inteqi 
 |-  |^| { v e. L | T C_ v } = |^| { t e. L | T C_ t }
10 1 2 3 9 5 ldgenpisys 
 |-  ( ph -> |^| { v e. L | T C_ v } e. P )
11 1 ispisys2 
 |-  ( T e. P <-> ( T e. ~P ~P O /\ A. x e. ( ( ~P T i^i Fin ) \ { (/) } ) |^| x e. T ) )
12 11 simplbi 
 |-  ( T e. P -> T e. ~P ~P O )
13 5 12 syl 
 |-  ( ph -> T e. ~P ~P O )
14 13 elpwid 
 |-  ( ph -> T C_ ~P O )
15 2 3 14 ldsysgenld 
 |-  ( ph -> |^| { v e. L | T C_ v } e. L )
16 10 15 elind 
 |-  ( ph -> |^| { v e. L | T C_ v } e. ( P i^i L ) )
17 1 2 sigapildsys 
 |-  ( sigAlgebra ` O ) = ( P i^i L )
18 16 17 eleqtrrdi 
 |-  ( ph -> |^| { v e. L | T C_ v } e. ( sigAlgebra ` O ) )
19 ssintub 
 |-  T C_ |^| { v e. L | T C_ v }
20 19 a1i 
 |-  ( ph -> T C_ |^| { v e. L | T C_ v } )
21 sseq2 
 |-  ( u = |^| { v e. L | T C_ v } -> ( T C_ u <-> T C_ |^| { v e. L | T C_ v } ) )
22 21 intminss 
 |-  ( ( |^| { v e. L | T C_ v } e. ( sigAlgebra ` O ) /\ T C_ |^| { v e. L | T C_ v } ) -> |^| { u e. ( sigAlgebra ` O ) | T C_ u } C_ |^| { v e. L | T C_ v } )
23 18 20 22 syl2anc 
 |-  ( ph -> |^| { u e. ( sigAlgebra ` O ) | T C_ u } C_ |^| { v e. L | T C_ v } )
24 sseq2 
 |-  ( v = S -> ( T C_ v <-> T C_ S ) )
25 24 intminss 
 |-  ( ( S e. L /\ T C_ S ) -> |^| { v e. L | T C_ v } C_ S )
26 4 6 25 syl2anc 
 |-  ( ph -> |^| { v e. L | T C_ v } C_ S )
27 23 26 sstrd 
 |-  ( ph -> |^| { u e. ( sigAlgebra ` O ) | T C_ u } C_ S )