Theorem ldgenpisyslem2

Description: Lemma for ldgenpisys . (Contributed by Thierry Arnoux, 18-Jul-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 )
	ldgenpisyslem1.1	|- ( ph -> A e. E )
	ldgenpisyslem2.1	|- ( ph -> T C_ { b e. ~P O | ( A i^i b ) e. E } )
Assertion	ldgenpisyslem2	|- ( ph -> E C_ { b e. ~P O | ( A i^i b ) e. E } )

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		ldgenpisyslem1.1	|- ( ph -> A e. E )
7		ldgenpisyslem2.1	|- ( ph -> T C_ { b e. ~P O | ( A i^i b ) e. E } )
8	1 2 3 4 5 6	ldgenpisyslem1	|- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )
9	8 7	jca	|- ( ph -> ( { b e. ~P O | ( A i^i b ) e. E } e. L /\ T C_ { b e. ~P O | ( A i^i b ) e. E } ) )
10		sseq2	|- ( t = { b e. ~P O | ( A i^i b ) e. E } -> ( T C_ t <-> T C_ { b e. ~P O | ( A i^i b ) e. E } ) )
11	10	elrab	|- ( { b e. ~P O | ( A i^i b ) e. E } e. { t e. L | T C_ t } <-> ( { b e. ~P O | ( A i^i b ) e. E } e. L /\ T C_ { b e. ~P O | ( A i^i b ) e. E } ) )
12	9 11	sylibr	|- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. { t e. L | T C_ t } )
13		intss1	|- ( { b e. ~P O | ( A i^i b ) e. E } e. { t e. L | T C_ t } -> |^| { t e. L | T C_ t } C_ { b e. ~P O | ( A i^i b ) e. E } )
14	12 13	syl	|- ( ph -> |^| { t e. L | T C_ t } C_ { b e. ~P O | ( A i^i b ) e. E } )
15	4 14	eqsstrid	|- ( ph -> E C_ { b e. ~P O | ( A i^i b ) e. E } )