Step | Hyp | Ref
| Expression |
1 | | ssrab2 3514 |
. . . 4
       |
2 | | dynkin.o |
. . . . 5
   |
3 | | pwexg 4587 |
. . . . 5
 
  |
4 | | rabexg 4553 |
. . . . 5
      
  |
5 | | elpwg 3959 |
. . . . 5
     
  
  
   
       |
6 | 2, 3, 4, 5 | 4syl 19 |
. . . 4
        
         |
7 | 1, 6 | mpbiri 237 |
. . 3
  
  
    |
8 | | 0elpw 4572 |
. . . . . . 7
  |
9 | 8 | a1i 11 |
. . . . . 6

   |
10 | | in0 3760 |
. . . . . . . 8
   |
11 | | dynkin.l |
. . . . . . . . . . . . . . 15
  
 
     
Disj  
    |
12 | 11 | isldsys 28978 |
. . . . . . . . . . . . . 14

       
   Disj 
      |
13 | 12 | simprbi 466 |
. . . . . . . . . . . . 13
  
     
Disj  
    |
14 | 13 | simp1d 1020 |
. . . . . . . . . . . 12
   |
15 | 14 | ad2antlr 733 |
. . . . . . . . . . 11
       |
16 | 15 | ex 436 |
. . . . . . . . . 10
 
     |
17 | 16 | ralrimiva 2802 |
. . . . . . . . 9
  
   |
18 | 8 | elexi 3055 |
. . . . . . . . . 10
 |
19 | 18 | elintrab 4246 |
. . . . . . . . 9
   
 
   |
20 | 17, 19 | sylibr 216 |
. . . . . . . 8

     |
21 | 10, 20 | syl5eqel 2533 |
. . . . . . 7
    
   |
22 | | ldgenpisys.e |
. . . . . . 7
 
  |
23 | 21, 22 | syl6eleqr 2540 |
. . . . . 6
     |
24 | 9, 23 | jca 535 |
. . . . 5
 
      |
25 | | ineq2 3628 |
. . . . . . 7

      |
26 | 25 | eleq1d 2513 |
. . . . . 6

  
     |
27 | 26 | elrab 3196 |
. . . . 5
  
   
      |
28 | 24, 27 | sylibr 216 |
. . . 4

       |
29 | | ineq2 3628 |
. . . . . . . . 9
       |
30 | 29 | eleq1d 2513 |
. . . . . . . 8
   
     |
31 | 30 | elrab 3196 |
. . . . . . 7
     
       |
32 | | pwidg 3964 |
. . . . . . . . . . 11
    |
33 | 2, 32 | syl 17 |
. . . . . . . . . 10
    |
34 | 33 | adantr 467 |
. . . . . . . . 9
 
     
   |
35 | 34 | elpwdifcl 28155 |
. . . . . . . 8
 
           |
36 | 11 | pwldsys 28979 |
. . . . . . . . . . . . . . . . . . . 20
 
  |
37 | 2, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    |
38 | | ldgenpisys.1 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
39 | | dynkin.p |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      |
40 | 39 | ispisys 28974 |
. . . . . . . . . . . . . . . . . . . . . 22

          |
41 | 38, 40 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . 21
   
       |
42 | 41 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
     |
43 | | elpwi 3960 |
. . . . . . . . . . . . . . . . . . . 20
  
   |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

   |
45 | | sseq2 3454 |
. . . . . . . . . . . . . . . . . . . 20
       |
46 | 45 | intminss 4261 |
. . . . . . . . . . . . . . . . . . 19
  
 
      |
47 | 37, 44, 46 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
   
   |
48 | 22, 47 | syl5eqss 3476 |
. . . . . . . . . . . . . . . . 17

   |
49 | | ldgenpisyslem1.1 |
. . . . . . . . . . . . . . . . 17
   |
50 | 48, 49 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
    |
51 | | elpwi 3960 |
. . . . . . . . . . . . . . . 16
    |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15

  |
53 | 52 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
    
         |
54 | | difin 3680 |
. . . . . . . . . . . . . . . . . 18
       |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
         |
56 | | difin2 3705 |
. . . . . . . . . . . . . . . . 17
         |
57 | 55, 56 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
           |
58 | | incom 3625 |
. . . . . . . . . . . . . . . 16
         |
59 | 57, 58 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
           |
60 | | difuncomp 28166 |
. . . . . . . . . . . . . . 15
               |
61 | 59, 60 | eqtr3d 2487 |
. . . . . . . . . . . . . 14
               |
62 | 53, 61 | syl 17 |
. . . . . . . . . . . . 13
    
                     |
63 | | difeq2 3545 |
. . . . . . . . . . . . . . 15
                   |
64 | 63 | eleq1d 2513 |
. . . . . . . . . . . . . 14
         
           |
65 | | simplr 762 |
. . . . . . . . . . . . . . . 16
    
         |
66 | 13 | simp2d 1021 |
. . . . . . . . . . . . . . . 16
 
    |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . 15
    
       
    |
68 | | difeq2 3545 |
. . . . . . . . . . . . . . . . 17
       |
69 | 68 | eleq1d 2513 |
. . . . . . . . . . . . . . . 16
   
     |
70 | 69 | cbvralv 3019 |
. . . . . . . . . . . . . . 15
 
       |
71 | 67, 70 | sylib 200 |
. . . . . . . . . . . . . 14
    
       
    |
72 | 49, 22 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . . 20
      |
73 | | elintrabg 4247 |
. . . . . . . . . . . . . . . . . . . . 21
 
  


    |
74 | 49, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    


    |
75 | 72, 74 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
  
   |
76 | 75 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . 18
 
     |
77 | 76 | imp 431 |
. . . . . . . . . . . . . . . . 17
       |
78 | 77 | adantllr 725 |
. . . . . . . . . . . . . . . 16
    
         |
79 | | difeq2 3545 |
. . . . . . . . . . . . . . . . . 18
       |
80 | 79 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
   
     |
81 | 66 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
      |
82 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
83 | 80, 81, 82 | rspcdva 28115 |
. . . . . . . . . . . . . . . 16
 
     |
84 | 65, 78, 83 | syl2anc 667 |
. . . . . . . . . . . . . . 15
    
           |
85 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . 19
    
              |
86 | 85 | simprd 465 |
. . . . . . . . . . . . . . . . . 18
    
           |
87 | 86, 22 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
    
          
   |
88 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . 20
 |
89 | 88 | inex2 4545 |
. . . . . . . . . . . . . . . . . . 19
   |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
    
           |
91 | | elintrabg 4247 |
. . . . . . . . . . . . . . . . . 18
        


      |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
            


      |
93 | 87, 92 | mpbid 214 |
. . . . . . . . . . . . . . . 16
    
       

     |
94 | | simpr 463 |
. . . . . . . . . . . . . . . 16
    
         |
95 | | rspa 2755 |
. . . . . . . . . . . . . . . . 17
   
   

     |
96 | 95 | imp 431 |
. . . . . . . . . . . . . . . 16
              |
97 | 93, 65, 94, 96 | syl21anc 1267 |
. . . . . . . . . . . . . . 15
    
           |
98 | | incom 3625 |
. . . . . . . . . . . . . . . . 17
             |
99 | | inss1 3652 |
. . . . . . . . . . . . . . . . . 18
   |
100 | | disjdif 3839 |
. . . . . . . . . . . . . . . . . 18
     |
101 | | ssdisj 3814 |
. . . . . . . . . . . . . . . . . 18
   

      
     |
102 | 99, 100, 101 | mp2an 678 |
. . . . . . . . . . . . . . . . 17
       |
103 | 98, 102 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
       |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . 15
    
         
     |
105 | 11, 65, 84, 97, 104 | unelldsys 28980 |
. . . . . . . . . . . . . 14
    
               |
106 | 64, 71, 105 | rspcdva 28115 |
. . . . . . . . . . . . 13
    
                 |
107 | 62, 106 | eqeltrd 2529 |
. . . . . . . . . . . 12
    
             |
108 | 107 | ex 436 |
. . . . . . . . . . 11
                  |
109 | 108 | ralrimiva 2802 |
. . . . . . . . . 10
 
      

       |
110 | | inex1g 4546 |
. . . . . . . . . . . . 13
       |
111 | 49, 110 | syl 17 |
. . . . . . . . . . . 12
       |
112 | 111 | adantr 467 |
. . . . . . . . . . 11
 
            |
113 | | elintrabg 4247 |
. . . . . . . . . . 11
            
 
        |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
 
        
    


        |
115 | 109, 114 | mpbird 236 |
. . . . . . . . 9
 
               |
116 | 115, 22 | syl6eleqr 2540 |
. . . . . . . 8
 
            |
117 | 35, 116 | jca 535 |
. . . . . . 7
 
           
     |
118 | 31, 117 | sylan2b 478 |
. . . . . 6
 
                 |
119 | | ineq2 3628 |
. . . . . . . 8
           |
120 | 119 | eleq1d 2513 |
. . . . . . 7
     
       |
121 | 120 | elrab 3196 |
. . . . . 6
       
           |
122 | 118, 121 | sylibr 216 |
. . . . 5
 
         
     |
123 | 122 | ralrimiva 2802 |
. . . 4
                |
124 | 2 | ad2antrr 732 |
. . . . . . . . 9
           Disj     |
125 | | sspwb 4649 |
. . . . . . . . . . 11
      
          |
126 | 1, 125 | mpbi 212 |
. . . . . . . . . 10
         |
127 | | simplr 762 |
. . . . . . . . . 10
           Disj           |
128 | 126, 127 | sseldi 3430 |
. . . . . . . . 9
           Disj       |
129 | 124, 128 | elpwunicl 28168 |
. . . . . . . 8
           Disj       |
130 | | uniin2 28165 |
. . . . . . . . . . . . . 14

      |
131 | | vex 3048 |
. . . . . . . . . . . . . . . 16
 |
132 | 131 | inex2 4545 |
. . . . . . . . . . . . . . 15
   |
133 | 132 | dfiun3 5089 |
. . . . . . . . . . . . . 14

        |
134 | 130, 133 | eqtr3i 2475 |
. . . . . . . . . . . . 13
         |
135 | | simplr 762 |
. . . . . . . . . . . . . 14
            
Disj   

  |
136 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . 20
           |
137 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . 21
  |
138 | | nfdisj1 4386 |
. . . . . . . . . . . . . . . . . . . . 21
 Disj
 |
139 | 137, 138 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . 20
   Disj   |
140 | 136, 139 | nfan 2011 |
. . . . . . . . . . . . . . . . . . 19
   
      
 Disj
   |
141 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . 19
  |
142 | 140, 141 | nfan 2011 |
. . . . . . . . . . . . . . . . . 18
            
Disj     |
143 | | nfv 1761 |
. . . . . . . . . . . . . . . . . 18

 |
144 | 142, 143 | nfan 2011 |
. . . . . . . . . . . . . . . . 17
     
  
    
Disj   
  |
145 | | elpwi 3960 |
. . . . . . . . . . . . . . . . . . . . . 22
      
       |
146 | 145 | ad4antlr 739 |
. . . . . . . . . . . . . . . . . . . . 21
            
Disj   

       |
147 | 146 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . 20
     
  
    
Disj   

  
     |
148 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
149 | 148 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
150 | 149 | elrab 3196 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
151 | 150 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . 20
          |
152 | 147, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     
  
    
Disj   

     |
153 | 135 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
     
  
    
Disj   

   |
154 | | simplr 762 |
. . . . . . . . . . . . . . . . . . 19
     
  
    
Disj   

   |
155 | 22 | eleq2i 2521 |
. . . . . . . . . . . . . . . . . . . . . 22
  
       |
156 | 132 | elintrab 4246 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
     |
157 | 155, 156 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . 21
  


     |
158 | | rspa 2755 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

     |
159 | 157, 158 | sylanb 475 |
. . . . . . . . . . . . . . . . . . . 20
   
       |
160 | 159 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
    


    |
161 | 152, 153,
154, 160 | syl21anc 1267 |
. . . . . . . . . . . . . . . . . 18
     
  
    
Disj   

     |
162 | 161 | ex 436 |
. . . . . . . . . . . . . . . . 17
            
Disj   


     |
163 | 144, 162 | ralrimi 2788 |
. . . . . . . . . . . . . . . 16
            
Disj   


    |
164 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
         |
165 | 164 | rnmptss 6052 |
. . . . . . . . . . . . . . . 16
 
 
      |
166 | 163, 165 | syl 17 |
. . . . . . . . . . . . . . 15
            
Disj   

      |
167 | 135, 166 | sselpwd 28153 |
. . . . . . . . . . . . . 14
            
Disj   

       |
168 | | simpllr 769 |
. . . . . . . . . . . . . . . 16
            
Disj   

 Disj
   |
169 | 168 | simpld 461 |
. . . . . . . . . . . . . . 15
            
Disj   

  |
170 | | mptct 28302 |
. . . . . . . . . . . . . . . 16


     |
171 | | rnct 28300 |
. . . . . . . . . . . . . . . 16
    
      |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . 15

      |
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . 14
            
Disj   

      |
174 | 168 | simprd 465 |
. . . . . . . . . . . . . . . 16
            
Disj   

Disj   |
175 | | disjin2 28197 |
. . . . . . . . . . . . . . . 16
Disj
Disj
    |
176 | | disjrnmpt 28195 |
. . . . . . . . . . . . . . . 16
Disj
  Disj        |
177 | 174, 175,
176 | 3syl 18 |
. . . . . . . . . . . . . . 15
            
Disj   

Disj        |
178 | | nfmpt1 4492 |
. . . . . . . . . . . . . . . . 17
       |
179 | 178 | nfrn 5077 |
. . . . . . . . . . . . . . . 16
       |
180 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   |
181 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   |
182 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
183 | 179, 180,
181, 182 | cbvdisjf 28182 |
. . . . . . . . . . . . . . 15
Disj      Disj        |
184 | 177, 183 | sylibr 216 |
. . . . . . . . . . . . . 14
            
Disj   

Disj        |
185 | | breq1 4405 |
. . . . . . . . . . . . . . . . . 18
             |
186 | 181, 179 | disjeq1f 28184 |
. . . . . . . . . . . . . . . . . 18
     Disj
Disj         |
187 | 185, 186 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
      
Disj 
     Disj          |
188 | | unieq 4206 |
. . . . . . . . . . . . . . . . . 18
             |
189 | 188 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
      
        |
190 | 187, 189 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
       
Disj  
       Disj                |
191 | 13 | simp3d 1022 |
. . . . . . . . . . . . . . . . . 18
    
Disj  
   |
192 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
193 | | disjeq1 4380 |
. . . . . . . . . . . . . . . . . . . . 21
 Disj
Disj    |
194 | 192, 193 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . 20
   Disj   Disj     |
195 | | unieq 4206 |
. . . . . . . . . . . . . . . . . . . . 21
     |
196 | 195 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
197 | 194, 196 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
    Disj 
 
 
Disj  
    |
198 | 197 | cbvralv 3019 |
. . . . . . . . . . . . . . . . . 18
 
   Disj 
 
   
Disj  
   |
199 | 191, 198 | sylib 200 |
. . . . . . . . . . . . . . . . 17
    
Disj  
   |
200 | 199 | adantr 467 |
. . . . . . . . . . . . . . . 16
           
Disj  
   |
201 | | simpr 463 |
. . . . . . . . . . . . . . . 16
               |
202 | 190, 200,
201 | rspcdva 28115 |
. . . . . . . . . . . . . . 15
         

  
Disj               |
203 | 202 | imp 431 |
. . . . . . . . . . . . . 14
              Disj               |
204 | 135, 167,
173, 184, 203 | syl22anc 1269 |
. . . . . . . . . . . . 13
            
Disj   

       |
205 | 134, 204 | syl5eqel 2533 |
. . . . . . . . . . . 12
            
Disj   

     |
206 | 205 | ex 436 |
. . . . . . . . . . 11
   
      
 Disj
 
        |
207 | 206 | ralrimiva 2802 |
. . . . . . . . . 10
           Disj   

      |
208 | 88 | uniex 6587 |
. . . . . . . . . . . 12
  |
209 | 208 | inex2 4545 |
. . . . . . . . . . 11
    |
210 | 209 | elintrab 4246 |
. . . . . . . . . 10
      


      |
211 | 207, 210 | sylibr 216 |
. . . . . . . . 9
           Disj           |
212 | 211, 22 | syl6eleqr 2540 |
. . . . . . . 8
           Disj        |
213 | 129, 212 | jca 535 |
. . . . . . 7
           Disj    
       |
214 | | ineq2 3628 |
. . . . . . . . 9
         |
215 | 214 | eleq1d 2513 |
. . . . . . . 8
           |
216 | 215 | elrab 3196 |
. . . . . . 7
 
    
 
       |
217 | 213, 216 | sylibr 216 |
. . . . . 6
           Disj     
     |
218 | 217 | ex 436 |
. . . . 5
 
  
      Disj           |
219 | 218 | ralrimiva 2802 |
. . . 4
        
Disj    
      |
220 | 28, 123, 219 | 3jca 1188 |
. . 3
 
                          Disj            |
221 | 7, 220 | jca 535 |
. 2
                                   
Disj    
        |
222 | 11 | isldsys 28978 |
. 2
     
     
          
                  Disj             |
223 | 221, 222 | sylibr 216 |
1
  
  
  |