Metamath Proof Explorer


Theorem ldgenpisyslem1

Description: Lemma for ldgenpisys . (Contributed by Thierry Arnoux, 29-Jun-2020)

Ref Expression
Hypotheses dynkin.p P = s 𝒫 𝒫 O | fi s s
dynkin.l L = s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
dynkin.o φ O V
ldgenpisys.e E = t L | T t
ldgenpisys.1 φ T P
ldgenpisyslem1.1 φ A E
Assertion ldgenpisyslem1 φ b 𝒫 O | A b E L

Proof

Step Hyp Ref Expression
1 dynkin.p P = s 𝒫 𝒫 O | fi s s
2 dynkin.l L = s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
3 dynkin.o φ O V
4 ldgenpisys.e E = t L | T t
5 ldgenpisys.1 φ T P
6 ldgenpisyslem1.1 φ A E
7 ssrab2 b 𝒫 O | A b E 𝒫 O
8 pwexg O V 𝒫 O V
9 rabexg 𝒫 O V b 𝒫 O | A b E V
10 elpwg b 𝒫 O | A b E V b 𝒫 O | A b E 𝒫 𝒫 O b 𝒫 O | A b E 𝒫 O
11 3 8 9 10 4syl φ b 𝒫 O | A b E 𝒫 𝒫 O b 𝒫 O | A b E 𝒫 O
12 7 11 mpbiri φ b 𝒫 O | A b E 𝒫 𝒫 O
13 ineq2 b = A b = A
14 13 eleq1d b = A b E A E
15 0elpw 𝒫 O
16 15 a1i φ 𝒫 O
17 2 isldsys t L t 𝒫 𝒫 O t x t O x t x 𝒫 t x ω Disj y x y x t
18 17 simprbi t L t x t O x t x 𝒫 t x ω Disj y x y x t
19 18 simp1d t L t
20 19 ad2antlr φ t L T t t
21 20 ex φ t L T t t
22 21 ralrimiva φ t L T t t
23 0ex V
24 23 elintrab t L | T t t L T t t
25 22 24 sylibr φ t L | T t
26 in0 A =
27 25 26 4 3eltr4g φ A E
28 14 16 27 elrabd φ b 𝒫 O | A b E
29 ineq2 b = x A b = A x
30 29 eleq1d b = x A b E A x E
31 30 elrab x b 𝒫 O | A b E x 𝒫 O A x E
32 pwidg O V O 𝒫 O
33 3 32 syl φ O 𝒫 O
34 33 adantr φ x 𝒫 O A x E O 𝒫 O
35 34 elpwdifcl φ x 𝒫 O A x E O x 𝒫 O
36 2 pwldsys O V 𝒫 O L
37 3 36 syl φ 𝒫 O L
38 1 ispisys T P T 𝒫 𝒫 O fi T T
39 5 38 sylib φ T 𝒫 𝒫 O fi T T
40 39 simpld φ T 𝒫 𝒫 O
41 40 elpwid φ T 𝒫 O
42 sseq2 t = 𝒫 O T t T 𝒫 O
43 42 intminss 𝒫 O L T 𝒫 O t L | T t 𝒫 O
44 37 41 43 syl2anc φ t L | T t 𝒫 O
45 4 44 eqsstrid φ E 𝒫 O
46 45 6 sseldd φ A 𝒫 O
47 46 elpwid φ A O
48 47 ad3antrrr φ x 𝒫 O A x E t L T t A O
49 difin A A x = A x
50 difin2 A O A x = O x A
51 49 50 eqtrid A O A A x = O x A
52 incom O x A = A O x
53 51 52 eqtrdi A O A A x = A O x
54 difuncomp A O A A x = O O A A x
55 53 54 eqtr3d A O A O x = O O A A x
56 48 55 syl φ x 𝒫 O A x E t L T t A O x = O O A A x
57 difeq2 y = O A A x O y = O O A A x
58 57 eleq1d y = O A A x O y t O O A A x t
59 18 simp2d t L x t O x t
60 59 ad2antlr φ x 𝒫 O A x E t L T t x t O x t
61 difeq2 x = y O x = O y
62 61 eleq1d x = y O x t O y t
63 62 cbvralvw x t O x t y t O y t
64 60 63 sylib φ x 𝒫 O A x E t L T t y t O y t
65 simplr φ x 𝒫 O A x E t L T t t L
66 6 4 eleqtrdi φ A t L | T t
67 elintrabg A E A t L | T t t L T t A t
68 6 67 syl φ A t L | T t t L T t A t
69 66 68 mpbid φ t L T t A t
70 69 r19.21bi φ t L T t A t
71 70 imp φ t L T t A t
72 71 adantllr φ x 𝒫 O A x E t L T t A t
73 difeq2 x = A O x = O A
74 73 eleq1d x = A O x t O A t
75 59 adantr t L A t x t O x t
76 simpr t L A t A t
77 74 75 76 rspcdva t L A t O A t
78 65 72 77 syl2anc φ x 𝒫 O A x E t L T t O A t
79 simpllr φ x 𝒫 O A x E t L T t x 𝒫 O A x E
80 79 simprd φ x 𝒫 O A x E t L T t A x E
81 80 4 eleqtrdi φ x 𝒫 O A x E t L T t A x t L | T t
82 vex x V
83 82 inex2 A x V
84 elintrabg A x V A x t L | T t t L T t A x t
85 83 84 mp1i φ x 𝒫 O A x E t L T t A x t L | T t t L T t A x t
86 81 85 mpbid φ x 𝒫 O A x E t L T t t L T t A x t
87 simpr φ x 𝒫 O A x E t L T t T t
88 rspa t L T t A x t t L T t A x t
89 88 imp t L T t A x t t L T t A x t
90 86 65 87 89 syl21anc φ x 𝒫 O A x E t L T t A x t
91 incom O A A x = A x O A
92 inss1 A x A
93 disjdif A O A =
94 ssdisj A x A A O A = A x O A =
95 92 93 94 mp2an A x O A =
96 91 95 eqtri O A A x =
97 96 a1i φ x 𝒫 O A x E t L T t O A A x =
98 2 65 78 90 97 unelldsys φ x 𝒫 O A x E t L T t O A A x t
99 58 64 98 rspcdva φ x 𝒫 O A x E t L T t O O A A x t
100 56 99 eqeltrd φ x 𝒫 O A x E t L T t A O x t
101 100 ex φ x 𝒫 O A x E t L T t A O x t
102 101 ralrimiva φ x 𝒫 O A x E t L T t A O x t
103 inex1g A E A O x V
104 6 103 syl φ A O x V
105 104 adantr φ x 𝒫 O A x E A O x V
106 elintrabg A O x V A O x t L | T t t L T t A O x t
107 105 106 syl φ x 𝒫 O A x E A O x t L | T t t L T t A O x t
108 102 107 mpbird φ x 𝒫 O A x E A O x t L | T t
109 108 4 eleqtrrdi φ x 𝒫 O A x E A O x E
110 35 109 jca φ x 𝒫 O A x E O x 𝒫 O A O x E
111 31 110 sylan2b φ x b 𝒫 O | A b E O x 𝒫 O A O x E
112 ineq2 b = O x A b = A O x
113 112 eleq1d b = O x A b E A O x E
114 113 elrab O x b 𝒫 O | A b E O x 𝒫 O A O x E
115 111 114 sylibr φ x b 𝒫 O | A b E O x b 𝒫 O | A b E
116 115 ralrimiva φ x b 𝒫 O | A b E O x b 𝒫 O | A b E
117 ineq2 b = x A b = A x
118 117 eleq1d b = x A b E A x E
119 7 sspwi 𝒫 b 𝒫 O | A b E 𝒫 𝒫 O
120 simplr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x 𝒫 b 𝒫 O | A b E
121 119 120 sselid φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x 𝒫 𝒫 O
122 121 elpwunicl φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x 𝒫 O
123 uniin2 y x A y = A x
124 vex y V
125 124 inex2 A y V
126 125 dfiun3 y x A y = ran y x A y
127 123 126 eqtr3i A x = ran y x A y
128 simplr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t t L
129 nfv y φ x 𝒫 b 𝒫 O | A b E
130 nfv y x ω
131 nfdisj1 y Disj y x y
132 130 131 nfan y x ω Disj y x y
133 129 132 nfan y φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y
134 nfv y t L
135 133 134 nfan y φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L
136 nfv y T t
137 135 136 nfan y φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t
138 elpwi x 𝒫 b 𝒫 O | A b E x b 𝒫 O | A b E
139 138 ad4antlr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t x b 𝒫 O | A b E
140 139 sselda φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x y b 𝒫 O | A b E
141 ineq2 b = y A b = A y
142 141 eleq1d b = y A b E A y E
143 142 elrab y b 𝒫 O | A b E y 𝒫 O A y E
144 143 simprbi y b 𝒫 O | A b E A y E
145 140 144 syl φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x A y E
146 simpllr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x t L
147 simplr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x T t
148 4 eleq2i A y E A y t L | T t
149 125 elintrab A y t L | T t t L T t A y t
150 148 149 bitri A y E t L T t A y t
151 rspa t L T t A y t t L T t A y t
152 150 151 sylanb A y E t L T t A y t
153 152 imp A y E t L T t A y t
154 145 146 147 153 syl21anc φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x A y t
155 154 ex φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x A y t
156 137 155 ralrimi φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t y x A y t
157 eqid y x A y = y x A y
158 157 rnmptss y x A y t ran y x A y t
159 156 158 syl φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t ran y x A y t
160 128 159 sselpwd φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t ran y x A y 𝒫 t
161 simpllr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t x ω Disj y x y
162 161 simpld φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t x ω
163 1stcrestlem x ω ran y x A y ω
164 162 163 syl φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t ran y x A y ω
165 161 simprd φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t Disj y x y
166 disjin2 Disj y x y Disj y x A y
167 disjrnmpt Disj y x A y Disj z ran y x A y z
168 165 166 167 3syl φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t Disj z ran y x A y z
169 nfmpt1 _ y y x A y
170 169 nfrn _ y ran y x A y
171 nfcv _ z y
172 nfcv _ y z
173 id y = z y = z
174 170 171 172 173 cbvdisjf Disj y ran y x A y y Disj z ran y x A y z
175 168 174 sylibr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t Disj y ran y x A y y
176 breq1 z = ran y x A y z ω ran y x A y ω
177 172 170 disjeq1f z = ran y x A y Disj y z y Disj y ran y x A y y
178 176 177 anbi12d z = ran y x A y z ω Disj y z y ran y x A y ω Disj y ran y x A y y
179 unieq z = ran y x A y z = ran y x A y
180 179 eleq1d z = ran y x A y z t ran y x A y t
181 178 180 imbi12d z = ran y x A y z ω Disj y z y z t ran y x A y ω Disj y ran y x A y y ran y x A y t
182 18 simp3d t L x 𝒫 t x ω Disj y x y x t
183 breq1 x = z x ω z ω
184 disjeq1 x = z Disj y x y Disj y z y
185 183 184 anbi12d x = z x ω Disj y x y z ω Disj y z y
186 unieq x = z x = z
187 186 eleq1d x = z x t z t
188 185 187 imbi12d x = z x ω Disj y x y x t z ω Disj y z y z t
189 188 cbvralvw x 𝒫 t x ω Disj y x y x t z 𝒫 t z ω Disj y z y z t
190 182 189 sylib t L z 𝒫 t z ω Disj y z y z t
191 190 adantr t L ran y x A y 𝒫 t z 𝒫 t z ω Disj y z y z t
192 simpr t L ran y x A y 𝒫 t ran y x A y 𝒫 t
193 181 191 192 rspcdva t L ran y x A y 𝒫 t ran y x A y ω Disj y ran y x A y y ran y x A y t
194 193 imp t L ran y x A y 𝒫 t ran y x A y ω Disj y ran y x A y y ran y x A y t
195 128 160 164 175 194 syl22anc φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t ran y x A y t
196 127 195 eqeltrid φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t A x t
197 196 ex φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t A x t
198 197 ralrimiva φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y t L T t A x t
199 vuniex x V
200 199 inex2 A x V
201 200 elintrab A x t L | T t t L T t A x t
202 198 201 sylibr φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y A x t L | T t
203 202 4 eleqtrrdi φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y A x E
204 118 122 203 elrabd φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x b 𝒫 O | A b E
205 204 ex φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x b 𝒫 O | A b E
206 205 ralrimiva φ x 𝒫 b 𝒫 O | A b E x ω Disj y x y x b 𝒫 O | A b E
207 28 116 206 3jca φ b 𝒫 O | A b E x b 𝒫 O | A b E O x b 𝒫 O | A b E x 𝒫 b 𝒫 O | A b E x ω Disj y x y x b 𝒫 O | A b E
208 2 isldsys b 𝒫 O | A b E L b 𝒫 O | A b E 𝒫 𝒫 O b 𝒫 O | A b E x b 𝒫 O | A b E O x b 𝒫 O | A b E x 𝒫 b 𝒫 O | A b E x ω Disj y x y x b 𝒫 O | A b E
209 12 207 208 sylanbrc φ b 𝒫 O | A b E L