Step | Hyp | Ref
| Expression |
1 | | prdsxms.i |
. . . 4
   |
2 | | topnfn 15324 |
. . . . 5
 |
3 | | prdsxms.r |
. . . . . . 7
        |
4 | | ffn 5728 |
. . . . . . 7
     
  |
5 | 3, 4 | syl 17 |
. . . . . 6
   |
6 | | dffn2 5730 |
. . . . . 6

      |
7 | 5, 6 | sylib 200 |
. . . . 5
       |
8 | | fnfco 5748 |
. . . . 5
       
   |
9 | 2, 7, 8 | sylancr 669 |
. . . 4
 
   |
10 | | prdsxms.c |
. . . . 5
     
                          
        |
11 | 10 | ptval 20585 |
. . . 4
  
              |
12 | 1, 9, 11 | syl2anc 667 |
. . 3
             |
13 | | eldifsn 4097 |
. . . . . . . 8
        
    
   |
14 | | prdsxms.y |
. . . . . . . . . . . 12
  s  |
15 | | prdsxms.s |
. . . . . . . . . . . 12
   |
16 | | prdsxms.d |
. . . . . . . . . . . 12
     |
17 | | prdsxms.b |
. . . . . . . . . . . 12
     |
18 | 14, 15, 1, 16, 17, 3 | prdsxmslem1 21543 |
. . . . . . . . . . 11
        |
19 | | blrn 21424 |
. . . . . . . . . . 11
          

            |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
       
           |
21 | 18 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

 
       |
22 | | simprl 764 |
. . . . . . . . . . . . . . . 16
 

 
  |
23 | | simprr 766 |
. . . . . . . . . . . . . . . 16
 

    |
24 | | xbln0 21429 |
. . . . . . . . . . . . . . . 16
      
         
   |
25 | 21, 22, 23, 24 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
 

          
   |
26 | 1 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
 

    |
27 | | mptexg 6135 |
. . . . . . . . . . . . . . . . . 18
                                             |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
 

                                              |
29 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . 19
                                         |
30 | 29 | rgenw 2749 |
. . . . . . . . . . . . . . . . . 18

                                         |
31 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
                                                                                     |
32 | 31 | fnmpt 5704 |
. . . . . . . . . . . . . . . . . 18
 
                                                                                    |
33 | 30, 32 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
 

                                              |
34 | 3 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . 22
 

         |
35 | 34 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
        |
36 | | prdsxms.v |
. . . . . . . . . . . . . . . . . . . . . 22
         |
37 | | prdsxms.e |
. . . . . . . . . . . . . . . . . . . . . 22
             |
38 | 36, 37 | xmsxmet 21471 |
. . . . . . . . . . . . . . . . . . . . 21
             |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   
 
        |
40 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
  s         s        |
41 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
     s             s         |
42 | 15 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
43 | 35 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . . . . 22
 

  
       |
44 | | simp2l 1034 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

    |
45 | 34 | feqmptd 5918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

          |
46 | 45 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

    s   s         |
47 | 14, 46 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

    s         |
48 | 47 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

           s          |
49 | 17, 48 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

       s          |
50 | 44, 49 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . . . 22
 

       s          |
51 | 40, 41, 42, 26, 43, 36, 50 | prdsbascl 15381 |
. . . . . . . . . . . . . . . . . . . . 21
 

  
      |
52 | 51 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . . . 20
   
 
       |
53 | | simp2r 1035 |
. . . . . . . . . . . . . . . . . . . . 21
 

    |
54 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   
 
   |
55 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21
         |
56 | 55 | blopn 21515 |
. . . . . . . . . . . . . . . . . . . 20
          
                   |
57 | 39, 52, 54, 56 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
   
 
                   |
58 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
59 | 58 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
60 | 58 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
61 | 60, 36 | syl6eqr 2503 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
62 | 61 | sqxpeqd 4860 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       |
63 | 59, 62 | reseq12d 5106 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                           |
64 | 63, 37 | syl6eqr 2503 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               |
65 | 64 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
66 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
67 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
68 | 65, 66, 67 | oveq123d 6311 |
. . . . . . . . . . . . . . . . . . . . 21
                                                       |
69 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . 21
             |
70 | 68, 31, 69 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . . 20
                                                             |
71 | 70 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   
 
                                                             |
72 | | fvco3 5942 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
73 | | prdsxms.k |
. . . . . . . . . . . . . . . . . . . . . 22
         |
74 | 72, 73 | syl6eqr 2503 |
. . . . . . . . . . . . . . . . . . . . 21
                |
75 | 34, 74 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
   
 
         |
76 | 73, 36, 37 | xmstopn 21466 |
. . . . . . . . . . . . . . . . . . . . 21
            |
77 | 35, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   
 
       |
78 | 75, 77 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
   
 
             |
79 | 57, 71, 78 | 3eltr4d 2544 |
. . . . . . . . . . . . . . . . . 18
   
 
                                                       |
80 | 79 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . 17
 

  
                                                      |
81 | 34 | feqmptd 5918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

          |
82 | 81 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

    s   s         |
83 | 14, 82 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    s         |
84 | 83 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
 

           s          |
85 | 16, 84 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . 20
 

       s          |
86 | 85 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
 

              s           |
87 | 86 | oveqd 6307 |
. . . . . . . . . . . . . . . . . 18
 

                    s             |
88 | 58 | cbvmptv 4495 |
. . . . . . . . . . . . . . . . . . . 20
             |
89 | 88 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . 19
  s         s        |
90 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
     s             s         |
91 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
     s             s         |
92 | 83 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
 

           s          |
93 | 17, 92 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . 20
 

       s          |
94 | 44, 93 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . 19
 

       s          |
95 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . 19
 

    |
96 | 89, 90, 36, 37, 91, 42, 26, 35, 39, 94, 53, 95 | prdsbl 21506 |
. . . . . . . . . . . . . . . . . 18
 

            s           
              |
97 | 87, 96 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
 

                         |
98 | | fneq1 5664 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                         |
99 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                                               |
100 | 99 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                                                             |
101 | 100 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . 21
                                            
     
   

                                                       |
102 | 98, 101 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . 20
                                             
                                                      
                                                        |
103 | 99, 70 | sylan9eq 2505 |
. . . . . . . . . . . . . . . . . . . . . 22
                                            
                  |
104 | 103 | ixpeq2dva 7537 |
. . . . . . . . . . . . . . . . . . . . 21
                                                
              |
105 | 104 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . 20
                                                                 
               |
106 | 102, 105 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . 19
                                                                       
                                                                                                                           |
107 | 106 | spcegv 3135 |
. . . . . . . . . . . . . . . . . 18
                                                                                        
                                                                          
    
     
                      |
108 | 107 | 3impib 1206 |
. . . . . . . . . . . . . . . . 17
                                                                                       
                                                                          
    
     
                     |
109 | 28, 33, 80, 97, 108 | syl121anc 1273 |
. . . . . . . . . . . . . . . 16
 

      
     
                     |
110 | 109 | 3expia 1210 |
. . . . . . . . . . . . . . 15
 

                                    |
111 | 25, 110 | sylbid 219 |
. . . . . . . . . . . . . 14
 

               
     
                      |
112 | 111 | adantr 467 |
. . . . . . . . . . . . 13
   
                                                     |
113 | | simpr 463 |
. . . . . . . . . . . . . 14
   
                     |
114 | 113 | neeq1d 2683 |
. . . . . . . . . . . . 13
   
                       |
115 | | ral0 3874 |
. . . . . . . . . . . . . . . . . . 19
             |
116 | | difeq2 3545 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
117 | | difid 3835 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
118 | 116, 117 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
119 | 118 | raleqdv 2993 |
. . . . . . . . . . . . . . . . . . . 20
  

        
   
               |
120 | 119 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . 19
                                 |
121 | 1, 115, 120 | sylancl 668 |
. . . . . . . . . . . . . . . . . 18
                   |
122 | 121 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

  
                 |
123 | 122 | biantrud 510 |
. . . . . . . . . . . . . . . 16
 

    
     
    
              
                   |
124 | | df-3an 987 |
. . . . . . . . . . . . . . . 16
            
                   
          
                   |
125 | 123, 124 | syl6rbbr 268 |
. . . . . . . . . . . . . . 15
 

    
     
    
                 
     
        |
126 | | eqeq1 2455 |
. . . . . . . . . . . . . . 15
          
   
        
       |
127 | 125, 126 | bi2anan9 884 |
. . . . . . . . . . . . . 14
   
                        
                
        
          
        
        |
128 | 127 | exbidv 1768 |
. . . . . . . . . . . . 13
   
                
     
    
               
                                       |
129 | 112, 114,
128 | 3imtr4d 272 |
. . . . . . . . . . . 12
   
                          
                
         |
130 | 129 | ex 436 |
. . . . . . . . . . 11
 

                
     
    
               
          |
131 | 130 | rexlimdvva 2886 |
. . . . . . . . . 10
                 
     
    
               
          |
132 | 20, 131 | sylbid 219 |
. . . . . . . . 9
           
     
    
               
          |
133 | 132 | impd 433 |
. . . . . . . 8
      

    
     
    
               
         |
134 | 13, 133 | syl5bi 221 |
. . . . . . 7
      
                 
                
         |
135 | 134 | alrimiv 1773 |
. . . . . 6
                
                          
         |
136 | | ssab 3499 |
. . . . . 6
     
                  
                
      
       
                 
                
         |
137 | 135, 136 | sylibr 216 |
. . . . 5
                        
                
         |
138 | 137, 10 | syl6sseqr 3479 |
. . . 4
           |
139 | | ssv 3452 |
. . . . . . . . . 10
  |
140 | | fnssres 5689 |
. . . . . . . . . 10
          |
141 | 2, 139, 140 | mp2an 678 |
. . . . . . . . 9
     |
142 | | fvres 5879 |
. . . . . . . . . . 11
               |
143 | | xmstps 21468 |
. . . . . . . . . . . 12
    |
144 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
145 | 144 | tpstop 19954 |
. . . . . . . . . . . 12

      |
146 | 143, 145 | syl 17 |
. . . . . . . . . . 11
        |
147 | 142, 146 | eqeltrd 2529 |
. . . . . . . . . 10
           |
148 | 147 | rgen 2747 |
. . . . . . . . 9
 
        |
149 | | ffnfv 6049 |
. . . . . . . . 9
        
                 |
150 | 141, 148,
149 | mpbir2an 931 |
. . . . . . . 8
         |
151 | | fco2 5740 |
. . . . . . . 8
         
      
       |
152 | 150, 3, 151 | sylancr 669 |
. . . . . . 7
 
       |
153 | | eqid 2451 |
. . . . . . . 8

  
    
        |
154 | 10, 153 | ptbasfi 20596 |
. . . . . . 7
  
           
       
                                |
155 | 1, 152, 154 | syl2anc 667 |
. . . . . 6
      
       
                                |
156 | | eqid 2451 |
. . . . . . . . 9
         |
157 | 156 | mopntop 21455 |
. . . . . . . 8
            |
158 | 18, 157 | syl 17 |
. . . . . . 7
       |
159 | 14, 17, 15, 1, 5 | prdsbas2 15367 |
. . . . . . . . . . . 12
 
          |
160 | 3, 74 | sylan 474 |
. . . . . . . . . . . . . . . 16
 
  
      |
161 | 3 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . 18
 
        |
162 | | xmstps 21468 |
. . . . . . . . . . . . . . . . . 18
            |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
       |
164 | 36, 73 | istps 19951 |
. . . . . . . . . . . . . . . . 17
     TopOn    |
165 | 163, 164 | sylib 200 |
. . . . . . . . . . . . . . . 16
 
 TopOn    |
166 | 160, 165 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
 
  
    TopOn    |
167 | | toponuni 19942 |
. . . . . . . . . . . . . . 15
  
    TopOn           |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . . 14
 
          |
169 | 36, 168 | syl5eqr 2499 |
. . . . . . . . . . . . 13
 
                  |
170 | 169 | ixpeq2dva 7537 |
. . . . . . . . . . . 12
                    |
171 | 159, 170 | eqtrd 2485 |
. . . . . . . . . . 11
 
  
      |
172 | | fveq2 5865 |
. . . . . . . . . . . . 13
  
     
      |
173 | 172 | unieqd 4208 |
. . . . . . . . . . . 12
   
             |
174 | 173 | cbvixpv 7540 |
. . . . . . . . . . 11

  
    
        |
175 | 171, 174 | syl6eq 2501 |
. . . . . . . . . 10
 
  
      |
176 | 156 | mopntopon 21454 |
. . . . . . . . . . . 12
          TopOn    |
177 | 18, 176 | syl 17 |
. . . . . . . . . . 11
     TopOn    |
178 | | toponmax 19943 |
. . . . . . . . . . 11
     TopOn        |
179 | 177, 178 | syl 17 |
. . . . . . . . . 10
       |
180 | 175, 179 | eqeltrrd 2530 |
. . . . . . . . 9
               |
181 | 180 | snssd 4117 |
. . . . . . . 8
                 |
182 | 175 | mpteq1d 4484 |
. . . . . . . . . . . . . . . . . 18
        
  
           |
183 | 182 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
                           |
184 | 183 | cnveqd 5010 |
. . . . . . . . . . . . . . . 16
      
      

  
           |
185 | 184 | imaeq1d 5167 |
. . . . . . . . . . . . . . 15
                   
                 |
186 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . . . 20
           |
187 | 186 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . 19
     
       |
188 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20
             |
189 | 188 | mptpreima 5328 |
. . . . . . . . . . . . . . . . . . 19
           
      |
190 | 187, 189 | elrab2 3198 |
. . . . . . . . . . . . . . . . . 18
                    |
191 | 161, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
192 | 191 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
     
              |
193 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
     
         |
194 | 161, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
195 | 194 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
     
             |
196 | 193, 195 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . . 21
     
             |
197 | | simprrr 775 |
. . . . . . . . . . . . . . . . . . . . 21
     
             |
198 | 55 | mopni2 21508 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
199 | 192, 196,
197, 198 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . 20
     
                      |
200 | 18 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                        
       |
201 | | simprrl 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
202 | 201 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                        
  |
203 | | rpxr 11309 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
204 | 203 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                           |
205 | 156 | blopn 21515 |
. . . . . . . . . . . . . . . . . . . . . 22
      
               |
206 | 200, 202,
204, 205 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
   
                                       |
207 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                           |
208 | | blcntr 21428 |
. . . . . . . . . . . . . . . . . . . . . 22
      
           |
209 | 200, 202,
207, 208 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
   
                        
          |
210 | | blssm 21433 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
           |
211 | 200, 202,
204, 210 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                                   |
212 | | simplrr 771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                      
              |
213 | | simplll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
                           |
214 | | rpgt0 11313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
215 | 214 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
                        
  |
216 | 213, 202,
204, 215, 97 | syl121anc 1273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                                                |
217 | 216 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                                 
                |
218 | 217 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                      
               |
219 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
220 | 219 | elixp 7529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                   |
221 | 220 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                 |
222 | 218, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                      

                  |
223 | | simp-4r 777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                      
  |
224 | | rsp 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                
                   |
225 | 222, 223,
224 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                      
                  |
226 | 212, 225 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                      
      |
227 | 211, 226 | ssrabdv 3508 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                                         |
228 | 227, 189 | syl6sseqr 3479 |
. . . . . . . . . . . . . . . . . . . . 21
   
                                              |
229 | | eleq2 2518 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
           |
230 | | sseq1 3453 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
  
                              |
231 | 229, 230 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . 22
                      
                                |
232 | 231 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . . 21
             
                                                   |
233 | 206, 209,
228, 232 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . 20
   
                         
                    |
234 | 199, 233 | rexlimddv 2883 |
. . . . . . . . . . . . . . . . . . 19
     
                            |
235 | 234 | expr 620 |
. . . . . . . . . . . . . . . . . 18
                                  |
236 | 190, 235 | syl5bi 221 |
. . . . . . . . . . . . . . . . 17
                
                      |
237 | 236 | ralrimiv 2800 |
. . . . . . . . . . . . . . . 16
                                       |
238 | 158 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
           |
239 | | eltop2 19991 |
. . . . . . . . . . . . . . . . 17
                    
                                   |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . 16
                                                        |
241 | 237, 240 | mpbird 236 |
. . . . . . . . . . . . . . 15
                      |
242 | 185, 241 | eqeltrrd 2530 |
. . . . . . . . . . . . . 14
        
                     |
243 | 242 | ralrimiva 2802 |
. . . . . . . . . . . . 13
 
 
  

  
                  |
244 | 160 | raleqdv 2993 |
. . . . . . . . . . . . 13
 
  
 
        
                  

  

  
                   |
245 | 243, 244 | mpbird 236 |
. . . . . . . . . . . 12
 
                                  |
246 | 245 | ralrimiva 2802 |
. . . . . . . . . . 11
  
 
        
                     |
247 | | fveq2 5865 |
. . . . . . . . . . . . 13
  
     
      |
248 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
249 | 248 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . 16
  
  
          
              |
250 | 249 | cnveqd 5010 |
. . . . . . . . . . . . . . 15
  

  
                          |
251 | 250 | imaeq1d 5167 |
. . . . . . . . . . . . . 14
    
                  
                 |
252 | 251 | eleq1d 2513 |
. . . . . . . . . . . . 13
                        
  

  
                   |
253 | 247, 252 | raleqbidv 3001 |
. . . . . . . . . . . 12
  
 
        
                  
                                  |
254 | 253 | cbvralv 3019 |
. . . . . . . . . . 11
 

          
                  

                                 |
255 | 246, 254 | sylib 200 |
. . . . . . . . . 10
  
 
        
                     |
256 | | eqid 2451 |
. . . . . . . . . . 11
                                       
                 |
257 | 256 | fmpt2x 6859 |
. . . . . . . . . 10
 

          
                  
                              
                  |
258 | 255, 257 | sylib 200 |
. . . . . . . . 9
  
 
       
                  
                  |
259 | | frn 5735 |
. . . . . . . . 9
            
                  
               
                                  |
260 | 258, 259 | syl 17 |
. . . . . . . 8
                                   |
261 | 181, 260 | unssd 3610 |
. . . . . . 7
   
  
      
 
       
                       |
262 | | fiss 7938 |
. . . . . . 7
                
                                 
     
  
      
 
       
                            |
263 | 158, 261,
262 | syl2anc 667 |
. . . . . 6
              
                                        |
264 | 155, 263 | eqsstrd 3466 |
. . . . 5

          |
265 | | fitop 19930 |
. . . . . . 7
                   |
266 | 158, 265 | syl 17 |
. . . . . 6
               |
267 | 156 | mopnval 21453 |
. . . . . . . 8
                    |
268 | 18, 267 | syl 17 |
. . . . . . 7
               |
269 | | tgdif0 20008 |
. . . . . . 7
                     |
270 | 268, 269 | syl6eqr 2503 |
. . . . . 6
            
      |
271 | 266, 270 | eqtrd 2485 |
. . . . 5
                
      |
272 | 264, 271 | sseqtrd 3468 |
. . . 4

              |
273 | | 2basgen 20006 |
. . . 4
         
                    
          |
274 | 138, 272,
273 | syl2anc 667 |
. . 3
                   |
275 | 12, 274 | eqtr4d 2488 |
. 2
              
      |
276 | | prdsxms.j |
. . 3
     |
277 | 14, 15, 1, 5, 276 | prdstopn 20643 |
. 2
    
    |
278 | 275, 277,
270 | 3eqtr4d 2495 |
1
       |