Metamath Proof Explorer

Theorem ldgenpisys

Description: The lambda system E generated by a pi-system T is also a pi-system. (Contributed by Thierry Arnoux, 18-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 )
ldgenpisys.e 
|- E = |^| { t e. L | T C_ t }
ldgenpisys.1 
|- ( ph -> T e. P )
Assertion ldgenpisys 
|- ( ph -> E e. P )

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 ldgenpisys.e 
 |-  E = |^| { t e. L | T C_ t }
5 ldgenpisys.1 
 |-  ( ph -> T e. P )
6 ssrab2 
 |-  { 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 ) ) } C_ ~P ~P O
7 ssrab2 
 |-  { s e. ~P ~P O | ( fi ` s ) C_ s } C_ ~P ~P O
8 5 1 eleqtrdi 
 |-  ( ph -> T e. { s e. ~P ~P O | ( fi ` s ) C_ s } )
9 7 8 sselid 
 |-  ( ph -> T e. ~P ~P O )
10 9 elpwid 
 |-  ( ph -> T C_ ~P O )
11 2 3 10 ldsysgenld 
 |-  ( ph -> |^| { t e. L | T C_ t } e. L )
12 4 11 eqeltrid 
 |-  ( ph -> E e. L )
13 12 2 eleqtrdi 
 |-  ( ph -> E e. { 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 ) ) } )
14 6 13 sselid 
 |-  ( ph -> E e. ~P ~P O )
15 simprr 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> b e. E )
16 simprl 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> a e. E )
17 3 adantr 
 |-  ( ( ph /\ a e. E ) -> O e. V )
18 5 adantr 
 |-  ( ( ph /\ a e. E ) -> T e. P )
19 simpr 
 |-  ( ( ph /\ a e. E ) -> a e. E )
20 10 adantr 
 |-  ( ( ph /\ a e. E ) -> T C_ ~P O )
21 20 sselda 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> b e. ~P O )
22 incom 
 |-  ( b i^i a ) = ( a i^i b )
23 3 ad2antrr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> O e. V )
24 5 ad2antrr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> T e. P )
25 simpr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> b e. T )
26 1 2 23 4 24 25 ldgenpisyslem3 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> E C_ { c e. ~P O | ( b i^i c ) e. E } )
27 simplr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> a e. E )
28 26 27 sseldd 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> a e. { c e. ~P O | ( b i^i c ) e. E } )
29 ineq2 
 |-  ( c = a -> ( b i^i c ) = ( b i^i a ) )
30 29 eleq1d 
 |-  ( c = a -> ( ( b i^i c ) e. E <-> ( b i^i a ) e. E ) )
31 30 elrab 
 |-  ( a e. { c e. ~P O | ( b i^i c ) e. E } <-> ( a e. ~P O /\ ( b i^i a ) e. E ) )
32 28 31 sylib 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> ( a e. ~P O /\ ( b i^i a ) e. E ) )
33 32 simprd 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> ( b i^i a ) e. E )
34 22 33 eqeltrrid 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> ( a i^i b ) e. E )
35 21 34 jca 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> ( b e. ~P O /\ ( a i^i b ) e. E ) )
36 ineq2 
 |-  ( c = b -> ( a i^i c ) = ( a i^i b ) )
37 36 eleq1d 
 |-  ( c = b -> ( ( a i^i c ) e. E <-> ( a i^i b ) e. E ) )
38 37 elrab 
 |-  ( b e. { c e. ~P O | ( a i^i c ) e. E } <-> ( b e. ~P O /\ ( a i^i b ) e. E ) )
39 35 38 sylibr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. T ) -> b e. { c e. ~P O | ( a i^i c ) e. E } )
40 39 ex 
 |-  ( ( ph /\ a e. E ) -> ( b e. T -> b e. { c e. ~P O | ( a i^i c ) e. E } ) )
41 40 ssrdv 
 |-  ( ( ph /\ a e. E ) -> T C_ { c e. ~P O | ( a i^i c ) e. E } )
42 1 2 17 4 18 19 41 ldgenpisyslem2 
 |-  ( ( ph /\ a e. E ) -> E C_ { c e. ~P O | ( a i^i c ) e. E } )
43 16 42 syldan 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> E C_ { c e. ~P O | ( a i^i c ) e. E } )
44 ssrab 
 |-  ( E C_ { c e. ~P O | ( a i^i c ) e. E } <-> ( E C_ ~P O /\ A. c e. E ( a i^i c ) e. E ) )
45 43 44 sylib 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> ( E C_ ~P O /\ A. c e. E ( a i^i c ) e. E ) )
46 45 simprd 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> A. c e. E ( a i^i c ) e. E )
47 37 rspcv 
 |-  ( b e. E -> ( A. c e. E ( a i^i c ) e. E -> ( a i^i b ) e. E ) )
48 15 46 47 sylc 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> ( a i^i b ) e. E )
49 48 ralrimivva 
 |-  ( ph -> A. a e. E A. b e. E ( a i^i b ) e. E )
50 inficl 
 |-  ( E e. L -> ( A. a e. E A. b e. E ( a i^i b ) e. E <-> ( fi ` E ) = E ) )
51 12 50 syl 
 |-  ( ph -> ( A. a e. E A. b e. E ( a i^i b ) e. E <-> ( fi ` E ) = E ) )
52 49 51 mpbid 
 |-  ( ph -> ( fi ` E ) = E )
53 eqimss 
 |-  ( ( fi ` E ) = E -> ( fi ` E ) C_ E )
54 52 53 syl 
 |-  ( ph -> ( fi ` E ) C_ E )
55 14 54 jca 
 |-  ( ph -> ( E e. ~P ~P O /\ ( fi ` E ) C_ E ) )
56 1 ispisys 
 |-  ( E e. P <-> ( E e. ~P ~P O /\ ( fi ` E ) C_ E ) )
57 55 56 sylibr 
 |-  ( ph -> E e. P )