Theorem ldgenpisyslem3

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 )
	ldgenpisyslem3.1	|- ( ph -> A e. T )
Assertion	ldgenpisyslem3	|- ( 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		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 } )