Step | Hyp | Ref
| Expression |
1 | | xrltso 11440 |
. . . 4
 |
2 | 1 | a1i 11 |
. . 3
   |
3 | | nfv 1761 |
. . . . . . . . 9
   |
4 | | nfcv 2592 |
. . . . . . . . . 10
   |
5 | | nfmpt1 4492 |
. . . . . . . . . . 11
              ↾s     g      |
6 | 5 | nfrn 5077 |
. . . . . . . . . 10
              ↾s     g      |
7 | 4, 6 | nfel 2604 |
. . . . . . . . 9
             ↾s     g      |
8 | 3, 7 | nfan 2011 |
. . . . . . . 8
      
   
    ↾s  
  g       |
9 | | iccssxr 11717 |
. . . . . . . . . . . . . 14
    |
10 | | xrge0base 28447 |
. . . . . . . . . . . . . . 15
       
↾s       |
11 | | xrge0cmn 19010 |
. . . . . . . . . . . . . . . 16
  ↾s     CMnd |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
 
           ↾s  
 
CMnd |
13 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
                   |
14 | 13 | elin2d 3623 |
. . . . . . . . . . . . . . 15
 
           |
15 | | simpll 760 |
. . . . . . . . . . . . . . . . 17
     
   
 
   |
16 | 13 | elin1d 3622 |
. . . . . . . . . . . . . . . . . . . 20
 
                 |
17 | 16 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
     
   
 
         |
18 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . 20
 |
19 | 18 | elpw 3957 |
. . . . . . . . . . . . . . . . . . 19
  
    
      |
20 | 17, 19 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
     
   
 
        |
21 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
     
   
 
   |
22 | 20, 21 | sseldd 3433 |
. . . . . . . . . . . . . . . . 17
     
   
 
        |
23 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . 19
   |
24 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . 20
   |
25 | | nfiu1 4308 |
. . . . . . . . . . . . . . . . . . . 20
  
     |
26 | 24, 25 | nfel 2604 |
. . . . . . . . . . . . . . . . . . 19
 
     |
27 | 23, 26 | nfan 2011 |
. . . . . . . . . . . . . . . . . 18
          |
28 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . 19
     
            |
29 | | esum2d.0 |
. . . . . . . . . . . . . . . . . . . 20
   |
30 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . 20
      |
31 | 29, 30 | nfel 2604 |
. . . . . . . . . . . . . . . . . . 19
     |
32 | | esum2d.1 |
. . . . . . . . . . . . . . . . . . . . 21
      |
33 | 32 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
     
     

    

      |
34 | | simp-5l 778 |
. . . . . . . . . . . . . . . . . . . . 21
     
     

    

      |
35 | | simp-4r 777 |
. . . . . . . . . . . . . . . . . . . . 21
     
     

    

      |
36 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . 21
     
     

    

      |
37 | | esum2d.4 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
     |
38 | 34, 35, 36, 37 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . 20
     
     

    

         |
39 | 33, 38 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . 19
     
     

    

         |
40 | | elsnxp 5378 |
. . . . . . . . . . . . . . . . . . . . 21
      
      |
41 | 40 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     |
42 | 41 | adantll 720 |
. . . . . . . . . . . . . . . . . . 19
   
            
     |
43 | 28, 31, 39, 42 | r19.29af2 2928 |
. . . . . . . . . . . . . . . . . 18
   
                 |
44 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
 
      
      |
45 | | eliun 4283 |
. . . . . . . . . . . . . . . . . . 19
      
      |
46 | 44, 45 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
 
      
      |
47 | 27, 43, 46 | r19.29af 2930 |
. . . . . . . . . . . . . . . . 17
 
     
     |
48 | 15, 22, 47 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
     
   
 
      |
49 | 48 | ralrimiva 2802 |
. . . . . . . . . . . . . . 15
 
               |
50 | 10, 12, 14, 49 | gsummptcl 17599 |
. . . . . . . . . . . . . 14
 
            ↾s     g         |
51 | 9, 50 | sseldi 3430 |
. . . . . . . . . . . . 13
 
            ↾s     g      |
52 | 51 | ralrimiva 2802 |
. . . . . . . . . . . 12
              ↾s     g      |
53 | | eqid 2451 |
. . . . . . . . . . . . 13
   
        ↾s     g        
   
    ↾s  
  g      |
54 | 53 | rnmptss 6052 |
. . . . . . . . . . . 12
 
            ↾s     g   
   
   
    ↾s  
  g       |
55 | 52, 54 | syl 17 |
. . . . . . . . . . 11
    
   
    ↾s  
  g       |
56 | 55 | ad3antrrr 736 |
. . . . . . . . . 10
   
   
        ↾s     g        
   
 
   ↾s  
  g    
   
   
    ↾s  
  g       |
57 | | simpllr 769 |
. . . . . . . . . 10
   
   
        ↾s     g        
   
 
   ↾s  
  g                 ↾s     g       |
58 | 56, 57 | sseldd 3433 |
. . . . . . . . 9
   
   
        ↾s     g        
   
 
   ↾s  
  g       |
59 | | esum2d.2 |
. . . . . . . . . . . . 13
   |
60 | | snex 4641 |
. . . . . . . . . . . . . . 15
   |
61 | | esum2d.3 |
. . . . . . . . . . . . . . 15
 
   |
62 | | xpexg 6593 |
. . . . . . . . . . . . . . 15
    
      |
63 | 60, 61, 62 | sylancr 669 |
. . . . . . . . . . . . . 14
 
       |
64 | 63 | ralrimiva 2802 |
. . . . . . . . . . . . 13
        |
65 | | iunexg 6769 |
. . . . . . . . . . . . 13
               |
66 | 59, 64, 65 | syl2anc 667 |
. . . . . . . . . . . 12
        |
67 | 47 | ralrimiva 2802 |
. . . . . . . . . . . 12
 
          |
68 | | nfcv 2592 |
. . . . . . . . . . . . 13
  
     |
69 | 68 | esumcl 28851 |
. . . . . . . . . . . 12
       
        
Σ* 
          |
70 | 66, 67, 69 | syl2anc 667 |
. . . . . . . . . . 11
 Σ*            |
71 | 9, 70 | sseldi 3430 |
. . . . . . . . . 10
 Σ*         |
72 | 71 | ad3antrrr 736 |
. . . . . . . . 9
   
   
        ↾s     g        
   
 
   ↾s  
  g     Σ* 
       |
73 | | simpr 463 |
. . . . . . . . . 10
   
   
        ↾s     g        
   
 
   ↾s  
  g        ↾s     g      |
74 | | nfv 1761 |
. . . . . . . . . . . . . 14
     
   
   |
75 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
76 | 74, 75, 14, 48 | esumgsum 28866 |
. . . . . . . . . . . . 13
 
         Σ*     ↾s     g      |
77 | 66 | adantr 467 |
. . . . . . . . . . . . . 14
 
                |
78 | 47 | adantlr 721 |
. . . . . . . . . . . . . 14
     
   
 
     
     |
79 | 16, 19 | sylib 200 |
. . . . . . . . . . . . . 14
 
         
      |
80 | 74, 77, 78, 79 | esummono 28875 |
. . . . . . . . . . . . 13
 
         Σ*  Σ* 
       |
81 | 76, 80 | eqbrtrrd 4425 |
. . . . . . . . . . . 12
 
            ↾s     g    Σ*         |
82 | 81 | adantlr 721 |
. . . . . . . . . . 11
      
   
    ↾s  
  g        
   
 
  
↾s     g    Σ*         |
83 | 82 | adantr 467 |
. . . . . . . . . 10
   
   
        ↾s     g        
   
 
   ↾s  
  g        ↾s     g    Σ*         |
84 | 73, 83 | eqbrtrd 4423 |
. . . . . . . . 9
   
   
        ↾s     g        
   
 
   ↾s  
  g    
Σ* 
       |
85 | | xrlenlt 9699 |
. . . . . . . . . 10
 
Σ* 
      
Σ* 
    
Σ* 
        |
86 | 85 | biimpa 487 |
. . . . . . . . 9
   Σ*       
Σ* 
     
Σ* 
       |
87 | 58, 72, 84, 86 | syl21anc 1267 |
. . . . . . . 8
   
   
        ↾s     g        
   
 
   ↾s  
  g    
Σ* 
       |
88 | | simpr 463 |
. . . . . . . . 9
 
            ↾s     g     
            ↾s     g       |
89 | | ovex 6318 |
. . . . . . . . . 10
  
↾s     g     |
90 | 53, 89 | elrnmpti 5085 |
. . . . . . . . 9
    
        ↾s     g     
            ↾s     g      |
91 | 88, 90 | sylib 200 |
. . . . . . . 8
 
            ↾s     g     
   
   
    
↾s     g      |
92 | 8, 87, 91 | r19.29af 2930 |
. . . . . . 7
 
            ↾s     g     
Σ* 
       |
93 | 92 | ralrimiva 2802 |
. . . . . 6
              ↾s     g     Σ* 
       |
94 | | nfv 1761 |
. . . . . . . . 9
   
 Σ* 
       |
95 | | nfv 1761 |
. . . . . . . . . 10
  |
96 | 6, 95 | nfrex 2850 |
. . . . . . . . 9
               ↾s     g       |
97 | 76 | adantlr 721 |
. . . . . . . . . . . . 13
      
   
 
Σ*    
↾s     g      |
98 | 97 | adantlr 721 |
. . . . . . . . . . . 12
   
 Σ* 
     
        
Σ*    
↾s     g      |
99 | 98 | adantr 467 |
. . . . . . . . . . 11
     
Σ* 
              
Σ*  
Σ*    
↾s     g      |
100 | | simplr 762 |
. . . . . . . . . . . 12
     
Σ* 
              
Σ*     
   
   |
101 | 89 | a1i 11 |
. . . . . . . . . . . 12
     
Σ* 
              
Σ*     
↾s     g      |
102 | 53 | elrnmpt1 5083 |
. . . . . . . . . . . 12
             ↾s     g       
↾s     g       
   
    ↾s  
  g       |
103 | 100, 101,
102 | syl2anc 667 |
. . . . . . . . . . 11
     
Σ* 
              
Σ*     
↾s     g       
   
    ↾s  
  g       |
104 | 99, 103 | eqeltrd 2529 |
. . . . . . . . . 10
     
Σ* 
              
Σ*  
Σ*              ↾s     g       |
105 | | simpr 463 |
. . . . . . . . . . 11
     
 Σ*                
Σ*   Σ*
 
Σ*    |
106 | 105 | breq2d 4414 |
. . . . . . . . . 10
     
 Σ*                
Σ*   Σ*
 

Σ*     |
107 | | simpr 463 |
. . . . . . . . . 10
     
Σ* 
              
Σ*   Σ*    |
108 | 104, 106,
107 | rspcedvd 3155 |
. . . . . . . . 9
     
Σ* 
              
Σ*       
   
    ↾s  
  g        |
109 | | nfv 1761 |
. . . . . . . . . . 11
     |
110 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
111 | | nfcv 2592 |
. . . . . . . . . . . 12
  |
112 | 68 | nfesum1 28861 |
. . . . . . . . . . . 12
 Σ*        |
113 | 110, 111,
112 | nfbr 4447 |
. . . . . . . . . . 11

Σ* 
      |
114 | 109, 113 | nfan 2011 |
. . . . . . . . . 10
   
 Σ* 
       |
115 | 66 | ad2antrr 732 |
. . . . . . . . . 10
    Σ*        
      |
116 | 47 | 3ad2antr3 1175 |
. . . . . . . . . . 11
 
 Σ*      
            |
117 | 116 | 3anassrs 1232 |
. . . . . . . . . 10
   
 Σ* 
     
     
     |
118 | | simplr 762 |
. . . . . . . . . 10
    Σ*          |
119 | | simpr 463 |
. . . . . . . . . 10
    Σ*        Σ*         |
120 | 114, 115,
117, 118, 119 | esumlub 28881 |
. . . . . . . . 9
    Σ*           
   
 
Σ*    |
121 | 94, 96, 108, 120 | r19.29af2 2928 |
. . . . . . . 8
    Σ*            
   
    ↾s  
  g        |
122 | 121 | ex 436 |
. . . . . . 7
 

 Σ*      
    
   
    ↾s  
  g         |
123 | 122 | ralrimiva 2802 |
. . . . . 6
  
Σ* 
     
            ↾s     g         |
124 | 93, 123 | jca 535 |
. . . . 5
      
   
    ↾s  
  g     Σ* 
      
Σ* 
     
            ↾s     g          |
125 | | simpr 463 |
. . . . . . . . . 10
 
Σ*        Σ*         |
126 | 125 | breq1d 4412 |
. . . . . . . . 9
 
Σ*         Σ* 
        |
127 | 126 | notbid 296 |
. . . . . . . 8
 
Σ*        
Σ* 
        |
128 | 127 | ralbidv 2827 |
. . . . . . 7
 
Σ*             
   
    ↾s  
  g                  ↾s     g     Σ* 
        |
129 | 125 | breq2d 4414 |
. . . . . . . . 9
 
Σ*        
Σ* 
        |
130 | 129 | imbi1d 319 |
. . . . . . . 8
 
Σ*              
   
    ↾s  
  g       
Σ* 
     
            ↾s     g          |
131 | 130 | ralbidv 2827 |
. . . . . . 7
 
Σ*          
    
   
    ↾s  
  g       

Σ* 
     
            ↾s     g          |
132 | 128, 131 | anbi12d 717 |
. . . . . 6
 
Σ*          
   
        ↾s     g                    ↾s     g             
   
    ↾s  
  g     Σ* 
      
Σ* 
     
            ↾s     g           |
133 | 71, 132 | rspcedv 3154 |
. . . . 5
       
   
    ↾s  
  g     Σ* 
      
Σ* 
     
            ↾s     g       
      
   
    ↾s  
  g                    ↾s     g           |
134 | 124, 133 | mpd 15 |
. . . 4
                ↾s     g                    ↾s     g          |
135 | 2, 134 | supcl 7972 |
. . 3
               ↾s     g         |
136 | | nfv 1761 |
. . . . 5
   |
137 | | nfcv 2592 |
. . . . . 6
   |
138 | | nfmpt1 4492 |
. . . . . . 7
         ↾s     g  Σ*
     |
139 | 138 | nfrn 5077 |
. . . . . 6
         ↾s     g  Σ*
     |
140 | 137, 139 | nfel 2604 |
. . . . 5
        ↾s  
  g  Σ*
     |
141 | 136, 140 | nfan 2011 |
. . . 4
          ↾s     g  Σ*
      |
142 | | simpr 463 |
. . . . . . . . . . . 12
 
         |
143 | | simpll 760 |
. . . . . . . . . . . . 13
          |
144 | 142 | elin1d 3622 |
. . . . . . . . . . . . . . 15
 
       |
145 | | elpwi 3960 |
. . . . . . . . . . . . . . 15
 
  |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
 
      |
147 | 146 | sselda 3432 |
. . . . . . . . . . . . 13
          |
148 | 143, 147,
61 | syl2anc 667 |
. . . . . . . . . . . 12
          |
149 | 143 | adantrr 723 |
. . . . . . . . . . . . 13
       
 
  |
150 | 147 | adantrr 723 |
. . . . . . . . . . . . 13
       
 
  |
151 | | simprr 766 |
. . . . . . . . . . . . 13
       
 
  |
152 | 149, 150,
151, 37 | syl12anc 1266 |
. . . . . . . . . . . 12
       
 
     |
153 | 142 | elin2d 3623 |
. . . . . . . . . . . 12
 
      |
154 | 29, 32, 142, 148, 152, 153 | esum2dlem 28913 |
. . . . . . . . . . 11
 
   
Σ* Σ*  Σ*         |
155 | | nfv 1761 |
. . . . . . . . . . . 12
        |
156 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
157 | 37 | anassrs 654 |
. . . . . . . . . . . . . . 15
          |
158 | 157 | ralrimiva 2802 |
. . . . . . . . . . . . . 14
 
 
     |
159 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
160 | 159 | esumcl 28851 |
. . . . . . . . . . . . . 14
      
Σ* 
     |
161 | 61, 158, 160 | syl2anc 667 |
. . . . . . . . . . . . 13
 

Σ* 
     |
162 | 143, 147,
161 | syl2anc 667 |
. . . . . . . . . . . 12
       
Σ* 
     |
163 | 155, 156,
153, 162 | esumgsum 28866 |
. . . . . . . . . . 11
 
   
Σ* Σ*     ↾s  
  g  Σ*
     |
164 | 154, 163 | eqtr3d 2487 |
. . . . . . . . . 10
 
   
Σ* 
        ↾s  
  g  Σ*
     |
165 | | nfv 1761 |
. . . . . . . . . . 11
        |
166 | 66 | adantr 467 |
. . . . . . . . . . 11
 
    
      |
167 | 47 | adantlr 721 |
. . . . . . . . . . 11
            
     |
168 | | iunss1 4290 |
. . . . . . . . . . . 12
 
   
       |
169 | 146, 168 | syl 17 |
. . . . . . . . . . 11
 
    
   
       |
170 | 165, 166,
167, 169 | esummono 28875 |
. . . . . . . . . 10
 
   
Σ* 
     Σ*         |
171 | 164, 170 | eqbrtrrd 4425 |
. . . . . . . . 9
 
      
↾s     g  Σ*
  
Σ* 
       |
172 | 11 | a1i 11 |
. . . . . . . . . . . 12
 
     
↾s     CMnd |
173 | 162 | ralrimiva 2802 |
. . . . . . . . . . . 12
 
    
Σ* 
     |
174 | 10, 172, 153, 173 | gsummptcl 17599 |
. . . . . . . . . . 11
 
      
↾s     g  Σ*
        |
175 | 9, 174 | sseldi 3430 |
. . . . . . . . . 10
 
      
↾s     g  Σ*
     |
176 | 71 | adantr 467 |
. . . . . . . . . 10
 
   
Σ* 
       |
177 | | xrlenlt 9699 |
. . . . . . . . . 10
     ↾s  
  g  Σ*
   Σ*            ↾s     g  Σ*
  
Σ* 
    
Σ* 
        ↾s  
  g  Σ*
      |
178 | 175, 176,
177 | syl2anc 667 |
. . . . . . . . 9
 
        ↾s  
  g  Σ*
  
Σ* 
    
Σ* 
        ↾s  
  g  Σ*
      |
179 | 171, 178 | mpbid 214 |
. . . . . . . 8
 
    Σ*          ↾s  
  g  Σ*
     |
180 | | nfv 1761 |
. . . . . . . . . . 11
   |
181 | | eqidd 2452 |
. . . . . . . . . . 11
 
            ↾s     g       ↾s  
  g      |
182 | 180, 68, 66, 47, 181 | esumval 28867 |
. . . . . . . . . 10
 Σ*                     ↾s     g         |
183 | 182 | adantr 467 |
. . . . . . . . 9
 
   
Σ* 
                   ↾s     g         |
184 | 183 | breq1d 4412 |
. . . . . . . 8
 
    Σ*          ↾s  
  g  Σ*
  
              ↾s     g          ↾s  
  g  Σ*
      |
185 | 179, 184 | mtbid 302 |
. . . . . . 7
 
         
        ↾s     g          ↾s  
  g  Σ*
     |
186 | 185 | adantlr 721 |
. . . . . 6
          ↾s     g  Σ*
              
        ↾s     g          ↾s  
  g  Σ*
     |
187 | 186 | adantr 467 |
. . . . 5
   
      
↾s     g  Σ*
            ↾s     g  Σ*
                  ↾s     g          ↾s  
  g  Σ*
     |
188 | | simpr 463 |
. . . . . . 7
   
      
↾s     g  Σ*
            ↾s     g  Σ*
      
↾s     g  Σ*
     |
189 | 188 | breq2d 4414 |
. . . . . 6
   
      
↾s     g  Σ*
            ↾s     g  Σ*
                   ↾s     g                     ↾s     g          ↾s  
  g  Σ*
      |
190 | 189 | notbid 296 |
. . . . 5
   
      
↾s     g  Σ*
            ↾s     g  Σ*
                   ↾s     g      
              ↾s     g          ↾s  
  g  Σ*
      |
191 | 187, 190 | mpbird 236 |
. . . 4
   
      
↾s     g  Σ*
            ↾s     g  Σ*
                  ↾s     g         |
192 | | eqid 2451 |
. . . . . . 7
      
↾s     g  Σ*
           ↾s     g  Σ*
     |
193 | | ovex 6318 |
. . . . . . 7
  
↾s     g  Σ*
    |
194 | 192, 193 | elrnmpti 5085 |
. . . . . 6
       
↾s     g  Σ*
   
        ↾s     g  Σ*
     |
195 | 194 | biimpi 198 |
. . . . 5
       
↾s     g  Σ*
    
 
    
↾s     g  Σ*
     |
196 | 195 | adantl 468 |
. . . 4
 
       ↾s     g  Σ*
             ↾s     g  Σ*
     |
197 | 141, 191,
196 | r19.29af 2930 |
. . 3
 
       ↾s     g  Σ*
    
              ↾s     g         |
198 | 4 | nfel1 2606 |
. . . . . . . . 9
  |
199 | | nfcv 2592 |
. . . . . . . . . 10
  |
200 | | nfcv 2592 |
. . . . . . . . . . 11
   |
201 | 6, 200, 199 | nfsup 7965 |
. . . . . . . . . 10
       
        ↾s     g        |
202 | 4, 199, 201 | nfbr 4447 |
. . . . . . . . 9
               ↾s     g        |
203 | 198, 202 | nfan 2011 |
. . . . . . . 8
                 ↾s     g         |
204 | 3, 203 | nfan 2011 |
. . . . . . 7
                  ↾s     g          |
205 | | nfcv 2592 |
. . . . . . . 8
   |
206 | 205, 6 | nfel 2604 |
. . . . . . 7
             ↾s     g      |
207 | 204, 206 | nfan 2011 |
. . . . . 6
                   ↾s     g            
   
    ↾s  
  g       |
208 | | nfv 1761 |
. . . . . 6
  |
209 | 207, 208 | nfan 2011 |
. . . . 5
                    ↾s     g            
   
    ↾s  
  g        |
210 | | simp-5l 778 |
. . . . . . . 8
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g       |
211 | | simpr1l 1065 |
. . . . . . . . . 10
 
                ↾s     g       
            ↾s     g     
       
  
↾s     g         |
212 | 211 | 3anassrs 1232 |
. . . . . . . . 9
                   ↾s     g            
   
    ↾s  
  g         
   

  
↾s     g     
  |
213 | 212 | 3anassrs 1232 |
. . . . . . . 8
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g       |
214 | 210, 213 | jca 535 |
. . . . . . 7
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g     
   |
215 | | simpr1r 1066 |
. . . . . . . . 9
 
                ↾s     g       
            ↾s     g     
       
  
↾s     g                     ↾s     g         |
216 | 215 | 3anassrs 1232 |
. . . . . . . 8
                   ↾s     g            
   
    ↾s  
  g         
   

  
↾s     g     
     
        ↾s     g         |
217 | 216 | 3anassrs 1232 |
. . . . . . 7
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g          
   
    ↾s  
  g         |
218 | 214, 217 | jca 535 |
. . . . . 6
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g       
              ↾s     g          |
219 | | simpllr 769 |
. . . . . . 7
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g       |
220 | | simpr 463 |
. . . . . . 7
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g        ↾s     g      |
221 | 219, 220 | breqtrd 4427 |
. . . . . 6
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g       
↾s     g      |
222 | | simplr 762 |
. . . . . 6
     
      
        ↾s     g            
   
    ↾s  
  g         
   
 
   ↾s  
  g               |
223 | | simpr 463 |
. . . . . . . . . . . 12
   
    ↾s     g                        |
224 | 223 | elin1d 3622 |
. . . . . . . . . . 11
   
    ↾s     g                      |
225 | | elpwi 3960 |
. . . . . . . . . . 11
  
   
       |
226 | | dmss 5034 |
. . . . . . . . . . . . . 14
      
      |
227 | | dmiun 5043 |
. . . . . . . . . . . . . 14

    
     |
228 | 226, 227 | syl6sseq 3478 |
. . . . . . . . . . . . 13
             |
229 | | dmxpss 5268 |
. . . . . . . . . . . . . . . . 17
       |
230 | 229 | a1i 11 |
. . . . . . . . . . . . . . . 16
         |
231 | | snssi 4116 |
. . . . . . . . . . . . . . . 16
  
  |
232 | 230, 231 | sstrd 3442 |
. . . . . . . . . . . . . . 15
       |
233 | 232 | rgen 2747 |
. . . . . . . . . . . . . 14

   
 |
234 | | iunss 4319 |
. . . . . . . . . . . . . 14
 
           |
235 | 233, 234 | mpbir 213 |
. . . . . . . . . . . . 13

   
 |
236 | 228, 235 | syl6ss 3444 |
. . . . . . . . . . . 12
        |
237 | 18 | dmex 6726 |
. . . . . . . . . . . . 13
 |
238 | 237 | elpw 3957 |
. . . . . . . . . . . 12
 
  |
239 | 236, 238 | sylibr 216 |
. . . . . . . . . . 11
     
   |
240 | 224, 225,
239 | 3syl 18 |
. . . . . . . . . 10
   
    ↾s     g             
   |
241 | 223 | elin2d 3623 |
. . . . . . . . . . 11
   
    ↾s     g                |
242 | | dmfi 7854 |
. . . . . . . . . . 11

  |
243 | 241, 242 | syl 17 |
. . . . . . . . . 10
   
    ↾s     g             
  |
244 | 240, 243 | elind 3618 |
. . . . . . . . 9
   
    ↾s     g             
     |
245 | | ovex 6318 |
. . . . . . . . . 10
  
↾s     g  Σ*     |
246 | 245 | a1i 11 |
. . . . . . . . 9
   
    ↾s     g                 ↾s     g  Σ*      |
247 | | mpteq1 4483 |
. . . . . . . . . . 11
  Σ*
   Σ*     |
248 | 247 | oveq2d 6306 |
. . . . . . . . . 10
    ↾s  
  g  Σ*
      ↾s     g  Σ*      |
249 | 192, 248 | elrnmpt1s 5082 |
. . . . . . . . 9
        ↾s     g  Σ*        ↾s     g  Σ*           ↾s     g  Σ*
      |
250 | 244, 246,
249 | syl2anc 667 |
. . . . . . . 8
   
    ↾s     g                 ↾s     g  Σ*           ↾s     g  Σ*
      |
251 | | simpr 463 |
. . . . . . . . 9
     
  
↾s     g                 ↾s     g  Σ*       
↾s     g  Σ*      |
252 | 251 | breq2d 4414 |
. . . . . . . 8
     
  
↾s     g                 ↾s     g  Σ*         ↾s     g  Σ*       |
253 | | simpllr 769 |
. . . . . . . . 9
   
    ↾s     g                |
254 | 11 | a1i 11 |
. . . . . . . . . . 11
   
    ↾s     g                ↾s  
 
CMnd |
255 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   
↾s      |
256 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
 g |
257 | | nfmpt1 4492 |
. . . . . . . . . . . . . . . 16
     |
258 | 255, 256,
257 | nfov 6316 |
. . . . . . . . . . . . . . 15
     ↾s  
  g     |
259 | 110, 111,
258 | nfbr 4447 |
. . . . . . . . . . . . . 14
   
↾s     g     |
260 | 109, 259 | nfan 2011 |
. . . . . . . . . . . . 13
   
    ↾s     g      |
261 | | nfv 1761 |
. . . . . . . . . . . . 13
          |
262 | 260, 261 | nfan 2011 |
. . . . . . . . . . . 12
     
  
↾s     g               |
263 | | simp-4l 776 |
. . . . . . . . . . . . . 14
     
  
↾s     g              
  |
264 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . 15
   
    ↾s     g              
      |
265 | 264 | sselda 3432 |
. . . . . . . . . . . . . 14
     
  
↾s     g              
       |
266 | 263, 265,
47 | syl2anc 667 |
. . . . . . . . . . . . 13
     
  
↾s     g              
     |
267 | 266 | ex 436 |
. . . . . . . . . . . 12
   
    ↾s     g              
      |
268 | 262, 267 | ralrimi 2788 |
. . . . . . . . . . 11
   
    ↾s     g                    |
269 | 10, 254, 241, 268 | gsummptcl 17599 |
. . . . . . . . . 10
   
    ↾s     g                 ↾s     g         |
270 | 9, 269 | sseldi 3430 |
. . . . . . . . 9
   
    ↾s     g                 ↾s     g      |
271 | | nfv 1761 |
. . . . . . . . . . . . 13
   
    ↾s     g      |
272 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
273 | 25 | nfpw 3963 |
. . . . . . . . . . . . . . 15
         |
274 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
275 | 273, 274 | nfin 3639 |
. . . . . . . . . . . . . 14
    
   
  |
276 | 272, 275 | nfel 2604 |
. . . . . . . . . . . . 13
          |
277 | 271, 276 | nfan 2011 |
. . . . . . . . . . . 12
     
  
↾s     g               |
278 | | simpll 760 |
. . . . . . . . . . . . . . . 16
     
   
 
   |
279 | 79, 236 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
        
  |
280 | 279 | sselda 3432 |
. . . . . . . . . . . . . . . 16
     
   
 
   |
281 | 278, 280,
161 | syl2anc 667 |
. . . . . . . . . . . . . . 15
     
   
 

Σ* 
     |
282 | 281 | adantllr 725 |
. . . . . . . . . . . . . 14
   

          Σ*       |
283 | 282 | adantllr 725 |
. . . . . . . . . . . . 13
     
  
↾s      |