Step | Hyp | Ref
| Expression |
1 | | filtop 20882 |
. . . . . . 7
    
  |
2 | 1 | 3ad2ant2 1031 |
. . . . . 6
 
        
  |
3 | | simp1 1009 |
. . . . . 6
 
        
  |
4 | | simp3 1011 |
. . . . . 6
 
               |
5 | | fmf 20972 |
. . . . . 6
 
                     |
6 | 2, 3, 4, 5 | syl3anc 1269 |
. . . . 5
 
                         |
7 | | ffn 5733 |
. . . . 5
              
        |
8 | 6, 7 | syl 17 |
. . . 4
 
                 |
9 | | fvelrnb 5917 |
. . . 4
      
                  |
10 | 8, 9 | syl 17 |
. . 3
 
          
 
              |
11 | | ffn 5733 |
. . . . . . . . . . . 12
    
  |
12 | | dffn4 5804 |
. . . . . . . . . . . 12

      |
13 | 11, 12 | sylib 200 |
. . . . . . . . . . 11
           |
14 | | foima 5803 |
. . . . . . . . . . 11
           |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
           |
16 | 15 | ad2antlr 734 |
. . . . . . . . 9
            
      |
17 | | simpll 761 |
. . . . . . . . . 10
            
  |
18 | | simpr 463 |
. . . . . . . . . 10
            
      |
19 | | simplr 763 |
. . . . . . . . . 10
            
      |
20 | | fgcl 20905 |
. . . . . . . . . . . 12
    
          |
21 | | filtop 20882 |
. . . . . . . . . . . 12
        
      |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
    
      |
23 | 22 | adantl 468 |
. . . . . . . . . 10
            
      |
24 | | eqid 2453 |
. . . . . . . . . . 11
         |
25 | 24 | imaelfm 20978 |
. . . . . . . . . 10
  
                          |
26 | 17, 18, 19, 23, 25 | syl31anc 1272 |
. . . . . . . . 9
            
            |
27 | 16, 26 | eqeltrrd 2532 |
. . . . . . . 8
            
        |
28 | | eleq2 2520 |
. . . . . . . 8
      
          |
29 | 27, 28 | syl5ibcom 224 |
. . . . . . 7
            
      
   |
30 | 29 | ex 436 |
. . . . . 6
           
      
    |
31 | 1, 30 | sylan 474 |
. . . . 5
                           |
32 | 31 | 3adant1 1027 |
. . . 4
 
                         |
33 | 32 | rexlimdv 2879 |
. . 3
 
                         |
34 | 10, 33 | sylbid 219 |
. 2
 
          

   |
35 | | simpl2 1013 |
. . . . . . . . 9
  
                |
36 | | filelss 20879 |
. . . . . . . . . 10
         |
37 | 36 | ex 436 |
. . . . . . . . 9
    

   |
38 | 35, 37 | syl 17 |
. . . . . . . 8
  
          
   |
39 | | simpr 463 |
. . . . . . . . . . . 12
       
     
   |
40 | | eqidd 2454 |
. . . . . . . . . . . 12
       
     
             |
41 | | imaeq2 5167 |
. . . . . . . . . . . . . 14
             |
42 | 41 | eqeq2d 2463 |
. . . . . . . . . . . . 13
                         |
43 | 42 | rspcev 3152 |
. . . . . . . . . . . 12
             
            |
44 | 39, 40, 43 | syl2anc 667 |
. . . . . . . . . . 11
       
     
              |
45 | | simpl1 1012 |
. . . . . . . . . . . . . 14
  
            |
46 | | cnvimass 5191 |
. . . . . . . . . . . . . . . . 17
    
 |
47 | | fdm 5738 |
. . . . . . . . . . . . . . . . 17
       |
48 | 46, 47 | syl5sseq 3482 |
. . . . . . . . . . . . . . . 16
            |
49 | 48 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . 15
 
                |
50 | 49 | adantr 467 |
. . . . . . . . . . . . . 14
  
                 |
51 | 45, 50 | ssexd 4553 |
. . . . . . . . . . . . 13
  
                 |
52 | | eqid 2453 |
. . . . . . . . . . . . . 14
               |
53 | 52 | elrnmpt 5084 |
. . . . . . . . . . . . 13
            
     

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

             |
55 | 54 | adantr 467 |
. . . . . . . . . . 11
       
     
       
     

             |
56 | 44, 55 | mpbird 236 |
. . . . . . . . . 10
       
     
      
        |
57 | | ssid 3453 |
. . . . . . . . . . 11
           |
58 | | ffun 5736 |
. . . . . . . . . . . . . 14
       |
59 | 58 | 3ad2ant3 1032 |
. . . . . . . . . . . . 13
 
           |
60 | 59 | ad2antrr 733 |
. . . . . . . . . . . 12
       
     
   |
61 | | funimass3 6003 |
. . . . . . . . . . . 12
      
                        |
62 | 60, 46, 61 | sylancl 669 |
. . . . . . . . . . 11
       
     
                        |
63 | 57, 62 | mpbiri 237 |
. . . . . . . . . 10
       
     
         
  |
64 | | imaeq2 5167 |
. . . . . . . . . . . 12
                     |
65 | 64 | sseq1d 3461 |
. . . . . . . . . . 11
          
            |
66 | 65 | rspcev 3152 |
. . . . . . . . . 10
       
              
  
             |
67 | 56, 63, 66 | syl2anc 667 |
. . . . . . . . 9
       
     
  
             |
68 | 67 | ex 436 |
. . . . . . . 8
  
           

              |
69 | 38, 68 | jcad 536 |
. . . . . . 7
  
             
               |
70 | 35 | adantr 467 |
. . . . . . . . . . . 12
       
                            |
71 | | vex 3050 |
. . . . . . . . . . . . . . 15
 |
72 | 52 | elrnmpt 5084 |
. . . . . . . . . . . . . . 15
         
        |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
        
       |
74 | | ssid 3453 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
75 | 59 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
     
               |
76 | | cnvimass 5191 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 |
77 | | funimass3 6003 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                        |
78 | 75, 76, 77 | sylancl 669 |
. . . . . . . . . . . . . . . . . . . . . 22
        
     
                      
             |
79 | 74, 78 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . 21
        
     
                        |
80 | | imassrn 5182 |
. . . . . . . . . . . . . . . . . . . . 21
          |
81 | 79, 80 | jctir 541 |
. . . . . . . . . . . . . . . . . . . 20
        
     
                      
        
   |
82 | | ssin 3656 |
. . . . . . . . . . . . . . . . . . . 20
          
        
         
    |
83 | 81, 82 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19
        
     
                      
   |
84 | | elin 3619 |
. . . . . . . . . . . . . . . . . . . . 21
  

   |
85 | | fvelrnb 5917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          |
86 | 11, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
       |
87 | 86 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
          
       |
88 | 87 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
     
                      |
89 | 75 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
                    
  
    
  |
90 | 89, 76 | jctir 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                    
  
    
         |
91 | 59 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
     
   |
92 | 91 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
          
               |
93 | 47 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
           |
94 | 93 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        
     
               |
95 | 94 | eleq2d 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
     
                 |
96 | 95 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
          
               |
97 | | fvimacnv 6002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                |
98 | 92, 96, 97 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
          
                 
        |
99 | 98 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                    
  
    
       |
100 | | funfvima2 6146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                       |
101 | 90, 99, 100 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
                    
  
    
               |
102 | 101 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
          
                                  |
103 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
   |
104 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
            |
105 | 103, 104 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                       |
106 | 102, 105 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
          
                                |
107 | 106 | rexlimdva 2881 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
     
              
                  |
108 | 88, 107 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
     
                            |
109 | 108 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . 22
        
     
                            |
110 | 109 | impd 433 |
. . . . . . . . . . . . . . . . . . . . 21
        
     
              

            |
111 | 84, 110 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . 20
        
     
              
             |
112 | 111 | ssrdv 3440 |
. . . . . . . . . . . . . . . . . . 19
        
     
             
            |
113 | 83, 112 | eqssd 3451 |
. . . . . . . . . . . . . . . . . 18
        
     
                          |
114 | | filin 20881 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 
   |
115 | 114 | 3exp 1208 |
. . . . . . . . . . . . . . . . . . . . . 22
    

       |
116 | 115 | com23 81 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
117 | 116 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . 20
 
         

      |
118 | 117 | imp31 434 |
. . . . . . . . . . . . . . . . . . 19
       
     
     |
119 | 118 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
        
     
             
   |
120 | 113, 119 | eqeltrd 2531 |
. . . . . . . . . . . . . . . . 17
        
     
                        |
121 | 120 | exp32 610 |
. . . . . . . . . . . . . . . 16
       
     
                         |
122 | | imaeq2 5167 |
. . . . . . . . . . . . . . . . . 18
                     |
123 | 122 | sseq1d 3461 |
. . . . . . . . . . . . . . . . 17
          
            |
124 | 122 | eleq1d 2515 |
. . . . . . . . . . . . . . . . . 18
          
            |
125 | 124 | imbi2d 318 |
. . . . . . . . . . . . . . . . 17
                           |
126 | 123, 125 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
                                            |
127 | 121, 126 | syl5ibrcom 226 |
. . . . . . . . . . . . . . 15
       
     
                      |
128 | 127 | rexlimdva 2881 |
. . . . . . . . . . . . . 14
  
           
                    |
129 | 73, 128 | syl5bi 221 |
. . . . . . . . . . . . 13
  
                 
               |
130 | 129 | imp44 601 |
. . . . . . . . . . . 12
       
                            |
131 | | simprr 767 |
. . . . . . . . . . . 12
       
                        |
132 | | simprlr 774 |
. . . . . . . . . . . 12
       
                            |
133 | | filss 20880 |
. . . . . . . . . . . 12
                   |
134 | 70, 130, 131, 132, 133 | syl13anc 1271 |
. . . . . . . . . . 11
       
                        |
135 | 134 | exp44 618 |
. . . . . . . . . 10
  
                 
           |
136 | 135 | rexlimdv 2879 |
. . . . . . . . 9
  
           

           
    |
137 | 136 | com23 81 |
. . . . . . . 8
  
          
  
               |
138 | 137 | impd 433 |
. . . . . . 7
  
             
               |
139 | 69, 138 | impbid 194 |
. . . . . 6
  
          
                  |
140 | 2 | adantr 467 |
. . . . . . 7
  
            |
141 | | rnelfmlem 20979 |
. . . . . . 7
  
          
            |
142 | | simpl3 1014 |
. . . . . . 7
  
                |
143 | | elfm 20974 |
. . . . . . 7
            
                     
               |
144 | 140, 141,
142, 143 | syl3anc 1269 |
. . . . . 6
  
                          
               |
145 | 139, 144 | bitr4d 260 |
. . . . 5
  
          
                |
146 | 145 | eqrdv 2451 |
. . . 4
  
               
         |
147 | 8 | adantr 467 |
. . . . 5
  
                  |
148 | | fnfvelrn 6024 |
. . . . 5
       
                         
   |
149 | 147, 141,
148 | syl2anc 667 |
. . . 4
  
              

       
   |
150 | 146, 149 | eqeltrd 2531 |
. . 3
  
              |
151 | 150 | ex 436 |
. 2
 
         

    |
152 | 34, 151 | impbid 194 |
1
 
          
    |