Step | Hyp | Ref
| Expression |
1 | | filtop 20948 |
. . . . . . 7
    
  |
2 | 1 | 3ad2ant2 1052 |
. . . . . 6
 
        
  |
3 | | simp1 1030 |
. . . . . 6
 
        
  |
4 | | simp3 1032 |
. . . . . 6
 
               |
5 | | fmf 21038 |
. . . . . 6
 
                     |
6 | 2, 3, 4, 5 | syl3anc 1292 |
. . . . 5
 
                         |
7 | | ffn 5739 |
. . . . 5
              
        |
8 | 6, 7 | syl 17 |
. . . 4
 
                 |
9 | | fvelrnb 5926 |
. . . 4
      
                  |
10 | 8, 9 | syl 17 |
. . 3
 
          
 
              |
11 | | ffn 5739 |
. . . . . . . . . . . 12
    
  |
12 | | dffn4 5812 |
. . . . . . . . . . . 12

      |
13 | 11, 12 | sylib 201 |
. . . . . . . . . . 11
           |
14 | | foima 5811 |
. . . . . . . . . . 11
           |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
           |
16 | 15 | ad2antlr 741 |
. . . . . . . . 9
            
      |
17 | | simpll 768 |
. . . . . . . . . 10
            
  |
18 | | simpr 468 |
. . . . . . . . . 10
            
      |
19 | | simplr 770 |
. . . . . . . . . 10
            
      |
20 | | fgcl 20971 |
. . . . . . . . . . . 12
    
          |
21 | | filtop 20948 |
. . . . . . . . . . . 12
        
      |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
    
      |
23 | 22 | adantl 473 |
. . . . . . . . . 10
            
      |
24 | | eqid 2471 |
. . . . . . . . . . 11
         |
25 | 24 | imaelfm 21044 |
. . . . . . . . . 10
  
                          |
26 | 17, 18, 19, 23, 25 | syl31anc 1295 |
. . . . . . . . 9
            
            |
27 | 16, 26 | eqeltrrd 2550 |
. . . . . . . 8
            
        |
28 | | eleq2 2538 |
. . . . . . . 8
      
          |
29 | 27, 28 | syl5ibcom 228 |
. . . . . . 7
            
      
   |
30 | 29 | ex 441 |
. . . . . 6
           
      
    |
31 | 1, 30 | sylan 479 |
. . . . 5
                           |
32 | 31 | 3adant1 1048 |
. . . 4
 
                         |
33 | 32 | rexlimdv 2870 |
. . 3
 
                         |
34 | 10, 33 | sylbid 223 |
. 2
 
          

   |
35 | | simpl2 1034 |
. . . . . . . . 9
  
                |
36 | | filelss 20945 |
. . . . . . . . . 10
         |
37 | 36 | ex 441 |
. . . . . . . . 9
    

   |
38 | 35, 37 | syl 17 |
. . . . . . . 8
  
          
   |
39 | | simpr 468 |
. . . . . . . . . . . 12
       
     
   |
40 | | eqidd 2472 |
. . . . . . . . . . . 12
       
     
             |
41 | | imaeq2 5170 |
. . . . . . . . . . . . . 14
             |
42 | 41 | eqeq2d 2481 |
. . . . . . . . . . . . 13
                         |
43 | 42 | rspcev 3136 |
. . . . . . . . . . . 12
             
            |
44 | 39, 40, 43 | syl2anc 673 |
. . . . . . . . . . 11
       
     
              |
45 | | simpl1 1033 |
. . . . . . . . . . . . . 14
  
            |
46 | | cnvimass 5194 |
. . . . . . . . . . . . . . . . 17
    
 |
47 | | fdm 5745 |
. . . . . . . . . . . . . . . . 17
       |
48 | 46, 47 | syl5sseq 3466 |
. . . . . . . . . . . . . . . 16
            |
49 | 48 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . 15
 
                |
50 | 49 | adantr 472 |
. . . . . . . . . . . . . 14
  
                 |
51 | 45, 50 | ssexd 4543 |
. . . . . . . . . . . . 13
  
                 |
52 | | eqid 2471 |
. . . . . . . . . . . . . 14
               |
53 | 52 | elrnmpt 5087 |
. . . . . . . . . . . . 13
            
     

             |
54 | 51, 53 | syl 17 |
. . . . . . . . . . . 12
  
                
     

             |
55 | 54 | adantr 472 |
. . . . . . . . . . 11
       
     
       
     

             |
56 | 44, 55 | mpbird 240 |
. . . . . . . . . 10
       
     
      
        |
57 | | ssid 3437 |
. . . . . . . . . . 11
           |
58 | | ffun 5742 |
. . . . . . . . . . . . . 14
       |
59 | 58 | 3ad2ant3 1053 |
. . . . . . . . . . . . 13
 
           |
60 | 59 | ad2antrr 740 |
. . . . . . . . . . . 12
       
     
   |
61 | | funimass3 6013 |
. . . . . . . . . . . 12
      
                        |
62 | 60, 46, 61 | sylancl 675 |
. . . . . . . . . . 11
       
     
                        |
63 | 57, 62 | mpbiri 241 |
. . . . . . . . . 10
       
     
         
  |
64 | | imaeq2 5170 |
. . . . . . . . . . . 12
                     |
65 | 64 | sseq1d 3445 |
. . . . . . . . . . 11
          
            |
66 | 65 | rspcev 3136 |
. . . . . . . . . 10
       
              
  
             |
67 | 56, 63, 66 | syl2anc 673 |
. . . . . . . . 9
       
     
  
             |
68 | 67 | ex 441 |
. . . . . . . 8
  
           

              |
69 | 38, 68 | jcad 542 |
. . . . . . 7
  
             
               |
70 | 35 | adantr 472 |
. . . . . . . . . . . 12
       
                            |
71 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
72 | 52 | elrnmpt 5087 |
. . . . . . . . . . . . . . 15
         
        |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
        
       |
74 | | ssid 3437 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
75 | 59 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
     
               |
76 | | cnvimass 5194 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 |
77 | | funimass3 6013 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                        |
78 | 75, 76, 77 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
        
     
                      
             |
79 | 74, 78 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . 21
        
     
                        |
80 | | imassrn 5185 |
. . . . . . . . . . . . . . . . . . . . 21
          |
81 | 79, 80 | jctir 547 |
. . . . . . . . . . . . . . . . . . . 20
        
     
                      
        
   |
82 | | ssin 3645 |
. . . . . . . . . . . . . . . . . . . 20
          
        
         
    |
83 | 81, 82 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
        
     
                      
   |
84 | | elin 3608 |
. . . . . . . . . . . . . . . . . . . . 21
  

   |
85 | | fvelrnb 5926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          |
86 | 11, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
       |
87 | 86 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
          
       |
88 | 87 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
     
                      |
89 | 75 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
                    
  
    
  |
90 | 89, 76 | jctir 547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                    
  
    
         |
91 | 59 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
     
   |
92 | 91 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
          
               |
93 | 47 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
           |
94 | 93 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        
     
               |
95 | 94 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
     
                 |
96 | 95 | biimpar 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
          
               |
97 | | fvimacnv 6012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                |
98 | 92, 96, 97 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
          
                 
        |
99 | 98 | biimpa 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                    
  
    
       |
100 | | funfvima2 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                       |
101 | 90, 99, 100 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
                    
  
    
               |
102 | 101 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
          
                                  |
103 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
   |
104 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
            |
105 | 103, 104 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                       |
106 | 102, 105 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
          
                                |
107 | 106 | rexlimdva 2871 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
     
              
                  |
108 | 88, 107 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
     
                            |
109 | 108 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . 22
        
     
                            |
110 | 109 | impd 438 |
. . . . . . . . . . . . . . . . . . . . 21
        
     
              

            |
111 | 84, 110 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . 20
        
     
              
             |
112 | 111 | ssrdv 3424 |
. . . . . . . . . . . . . . . . . . 19
        
     
             
            |
113 | 83, 112 | eqssd 3435 |
. . . . . . . . . . . . . . . . . 18
        
     
                          |
114 | | filin 20947 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 
   |
115 | 114 | 3exp 1230 |
. . . . . . . . . . . . . . . . . . . . . 22
    

       |
116 | 115 | com23 80 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
117 | 116 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . 20
 
         

      |
118 | 117 | imp31 439 |
. . . . . . . . . . . . . . . . . . 19
       
     
     |
119 | 118 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
        
     
             
   |
120 | 113, 119 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
        
     
                        |
121 | 120 | exp32 616 |
. . . . . . . . . . . . . . . 16
       
     
                         |
122 | | imaeq2 5170 |
. . . . . . . . . . . . . . . . . 18
                     |
123 | 122 | sseq1d 3445 |
. . . . . . . . . . . . . . . . 17
          
            |
124 | 122 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
          
            |
125 | 124 | imbi2d 323 |
. . . . . . . . . . . . . . . . 17
                           |
126 | 123, 125 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                                            |
127 | 121, 126 | syl5ibrcom 230 |
. . . . . . . . . . . . . . 15
       
     
                      |
128 | 127 | rexlimdva 2871 |
. . . . . . . . . . . . . 14
  
           
                    |
129 | 73, 128 | syl5bi 225 |
. . . . . . . . . . . . 13
  
                 
               |
130 | 129 | imp44 607 |
. . . . . . . . . . . 12
       
                            |
131 | | simprr 774 |
. . . . . . . . . . . 12
       
                        |
132 | | simprlr 781 |
. . . . . . . . . . . 12
       
                            |
133 | | filss 20946 |
. . . . . . . . . . . 12
                   |
134 | 70, 130, 131, 132, 133 | syl13anc 1294 |
. . . . . . . . . . 11
       
                        |
135 | 134 | exp44 624 |
. . . . . . . . . 10
  
                 
           |
136 | 135 | rexlimdv 2870 |
. . . . . . . . 9
  
           

           
    |
137 | 136 | com23 80 |
. . . . . . . 8
  
          
  
               |
138 | 137 | impd 438 |
. . . . . . 7
  
             
               |
139 | 69, 138 | impbid 195 |
. . . . . 6
  
          
                  |
140 | 2 | adantr 472 |
. . . . . . 7
  
            |
141 | | rnelfmlem 21045 |
. . . . . . 7
  
          
            |
142 | | simpl3 1035 |
. . . . . . 7
  
                |
143 | | elfm 21040 |
. . . . . . 7
            
                     
               |
144 | 140, 141,
142, 143 | syl3anc 1292 |
. . . . . 6
  
                          
               |
145 | 139, 144 | bitr4d 264 |
. . . . 5
  
          
                |
146 | 145 | eqrdv 2469 |
. . . 4
  
               
         |
147 | 8 | adantr 472 |
. . . . 5
  
                  |
148 | | fnfvelrn 6034 |
. . . . 5
       
                         
   |
149 | 147, 141,
148 | syl2anc 673 |
. . . 4
  
              

       
   |
150 | 146, 149 | eqeltrd 2549 |
. . 3
  
              |
151 | 150 | ex 441 |
. 2
 
         

    |
152 | 34, 151 | impbid 195 |
1
 
          
    |