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 |
|
ldgenpisyslem3.1 |
|- ( ph -> A e. T ) |
7 |
|
id |
|- ( T C_ t -> T C_ t ) |
8 |
7
|
rgenw |
|- A. t e. L ( T C_ t -> T C_ t ) |
9 |
|
ssintrab |
|- ( T C_ |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> T C_ t ) ) |
10 |
8 9
|
mpbir |
|- T C_ |^| { t e. L | T C_ t } |
11 |
10 4
|
sseqtrri |
|- T C_ E |
12 |
11 6
|
sseldi |
|- ( ph -> A e. E ) |
13 |
1
|
ispisys |
|- ( T e. P <-> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) ) |
14 |
5 13
|
sylib |
|- ( ph -> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) ) |
15 |
14
|
simpld |
|- ( ph -> T e. ~P ~P O ) |
16 |
|
elpwi |
|- ( T e. ~P ~P O -> T C_ ~P O ) |
17 |
15 16
|
syl |
|- ( ph -> T C_ ~P O ) |
18 |
5
|
adantr |
|- ( ( ph /\ b e. T ) -> T e. P ) |
19 |
6
|
adantr |
|- ( ( ph /\ b e. T ) -> A e. T ) |
20 |
|
simpr |
|- ( ( ph /\ b e. T ) -> b e. T ) |
21 |
1
|
inelpisys |
|- ( ( T e. P /\ A e. T /\ b e. T ) -> ( A i^i b ) e. T ) |
22 |
18 19 20 21
|
syl3anc |
|- ( ( ph /\ b e. T ) -> ( A i^i b ) e. T ) |
23 |
11 22
|
sseldi |
|- ( ( ph /\ b e. T ) -> ( A i^i b ) e. E ) |
24 |
23
|
ralrimiva |
|- ( ph -> A. b e. T ( A i^i b ) e. E ) |
25 |
17 24
|
jca |
|- ( ph -> ( T C_ ~P O /\ A. b e. T ( A i^i b ) e. E ) ) |
26 |
|
ssrab |
|- ( T C_ { b e. ~P O | ( A i^i b ) e. E } <-> ( T C_ ~P O /\ A. b e. T ( A i^i b ) e. E ) ) |
27 |
25 26
|
sylibr |
|- ( ph -> T C_ { b e. ~P O | ( A i^i b ) e. E } ) |
28 |
1 2 3 4 5 12 27
|
ldgenpisyslem2 |
|- ( ph -> E C_ { b e. ~P O | ( A i^i b ) e. E } ) |