Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . 4
       |
2 | | filelss 20867 |
. . . . 5
         |
3 | 2 | ex 436 |
. . . 4
    

   |
4 | 1, 3 | syl 17 |
. . 3
 
   |
5 | | fmfnfm.b |
. . . . . . . . 9
       |
6 | | mptexg 6135 |
. . . . . . . . . . 11
    

        |
7 | | rnexg 6725 |
. . . . . . . . . . 11
                 |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
    
         |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
          |
10 | | unexg 6592 |
. . . . . . . . 9
      
       
          |
11 | 5, 9, 10 | syl2anc 667 |
. . . . . . . 8
  
         |
12 | | ssfii 7933 |
. . . . . . . . 9
           
          

          |
13 | 12 | unssbd 3612 |
. . . . . . . 8
                                |
14 | 11, 13 | syl 17 |
. . . . . . 7
                       |
15 | 14 | adantr 467 |
. . . . . 6
 
 
                     |
16 | | eqid 2451 |
. . . . . . . . 9
           |
17 | | imaeq2 5164 |
. . . . . . . . . . 11
             |
18 | 17 | eqeq2d 2461 |
. . . . . . . . . 10
                         |
19 | 18 | rspcev 3150 |
. . . . . . . . 9
             
            |
20 | 16, 19 | mpan2 677 |
. . . . . . . 8
 
            |
21 | 20 | adantl 468 |
. . . . . . 7
 
 
            |
22 | | elfvdm 5891 |
. . . . . . . . . . 11
    
  |
23 | 5, 22 | syl 17 |
. . . . . . . . . 10
   |
24 | | cnvimass 5188 |
. . . . . . . . . . 11
    
 |
25 | | fmfnfm.f |
. . . . . . . . . . . 12
       |
26 | | fdm 5733 |
. . . . . . . . . . . 12
       |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
   |
28 | 24, 27 | syl5sseq 3480 |
. . . . . . . . . 10
        |
29 | 23, 28 | ssexd 4550 |
. . . . . . . . 9
        |
30 | 29 | adantr 467 |
. . . . . . . 8
 
        |
31 | | eqid 2451 |
. . . . . . . . 9
               |
32 | 31 | elrnmpt 5081 |
. . . . . . . 8
            
     

             |
33 | 30, 32 | syl 17 |
. . . . . . 7
 
       
     

             |
34 | 21, 33 | mpbird 236 |
. . . . . 6
 
               |
35 | 15, 34 | sseldd 3433 |
. . . . 5
 
         

          |
36 | | ffun 5731 |
. . . . . . . 8
       |
37 | | ssid 3451 |
. . . . . . . 8
           |
38 | | funimass2 5657 |
. . . . . . . 8
                     
  |
39 | 36, 37, 38 | sylancl 668 |
. . . . . . 7
             
  |
40 | 25, 39 | syl 17 |
. . . . . 6
         
  |
41 | 40 | adantr 467 |
. . . . 5
 
            |
42 | | imaeq2 5164 |
. . . . . . 7
                     |
43 | 42 | sseq1d 3459 |
. . . . . 6
          
            |
44 | 43 | rspcev 3150 |
. . . . 5
                            
                      |
45 | 35, 41, 44 | syl2anc 667 |
. . . 4
 
     
                |
46 | 45 | ex 436 |
. . 3
                        |
47 | 4, 46 | jcad 536 |
. 2
                          |
48 | | elfiun 7944 |
. . . . . . 7
      
                             
                 
              |
49 | 5, 9, 48 | syl2anc 667 |
. . . . . 6
              
        
                 
              |
50 | | fmfnfm.fm |
. . . . . . . 8
         |
51 | 5, 1, 25, 50 | fmfnfmlem1 20969 |
. . . . . . 7
                 |
52 | 5, 1, 25, 50 | fmfnfmlem3 20971 |
. . . . . . . . 9
    
                |
53 | 52 | eleq2d 2514 |
. . . . . . . 8
            
          |
54 | | vex 3048 |
. . . . . . . . . 10
 |
55 | 31 | elrnmpt 5081 |
. . . . . . . . . 10
         
        |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . 9
        
       |
57 | 5, 1, 25, 50 | fmfnfmlem2 20970 |
. . . . . . . . 9
                   |
58 | 56, 57 | syl5bi 221 |
. . . . . . . 8
  
                 |
59 | 53, 58 | sylbid 219 |
. . . . . . 7
                 

     |
60 | 52 | eleq2d 2514 |
. . . . . . . . . . . . 13
            
          |
61 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
62 | 31 | elrnmpt 5081 |
. . . . . . . . . . . . . 14
         
        |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . 13
        
       |
64 | 60, 63 | syl6bb 265 |
. . . . . . . . . . . 12
            

        |
65 | 64 | adantr 467 |
. . . . . . . . . . 11
 
    
    
       
        |
66 | | fbssfi 20852 |
. . . . . . . . . . . . 13
           
  |
67 | 5, 66 | sylan 474 |
. . . . . . . . . . . 12
 
    

  |
68 | 1 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . 18
    
       
      
        |
69 | 1 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
      |
70 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         |
71 | | filtop 20870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
73 | 72, 5, 25 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           |
74 | 73 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
           |
75 | | ssfg 20887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
      |
76 | 5, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

      |
77 | 76 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
78 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
79 | 78 | imaelfm 20966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                          |
80 | 74, 77, 79 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
             |
81 | 70, 80 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
82 | 81 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
 

        |
83 | 69, 82 | jca 535 |
. . . . . . . . . . . . . . . . . . . 20
 

              |
84 | | filin 20869 |
. . . . . . . . . . . . . . . . . . . . 21
               
   |
85 | 84 | 3expa 1208 |
. . . . . . . . . . . . . . . . . . . 20
           
     
   |
86 | 83, 85 | sylan 474 |
. . . . . . . . . . . . . . . . . . 19
      
        |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    
       
      
          |
88 | | simprr 766 |
. . . . . . . . . . . . . . . . . 18
    
       
      
    |
89 | | elin 3617 |
. . . . . . . . . . . . . . . . . . . . . 22
      
    
   |
90 | 25, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
91 | | fvelima 5917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
      |
92 | 91 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

    

       |
93 | 90, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
94 | 93 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
         
       |
95 | 90 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
   
          |
96 | | simplrr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
  |
97 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
         |
98 | | ssel2 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   |
99 | 96, 97, 98 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
   
          |
100 | 90 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
  |
101 | | fbelss 20848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         |
102 | 5, 101 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
103 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
104 | 102, 103 | sseqtr4d 3469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   |
105 | 104 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

 
  |
106 | 105 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
  |
107 | | fvimacnv 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                |
108 | 100, 106,
107 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
    
        |
109 | 108 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
    
        |
110 | 109 | impr 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    |
111 | 110 | ad2ant2rl 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
   
               |
112 | 99, 111 | elind 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
   
                 |
113 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
114 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 |
115 | 113, 114 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        |
116 | | funfvima2 6141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
     
        
                  |
117 | 115, 116 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

       
                  |
118 | 95, 112, 117 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
   
                         |
119 | 118 | anassrs 654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                            |
120 | 119 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                            |
121 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
   |
122 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                   |
123 | 121, 122 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                           
               |
124 | 120, 123 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                          |
125 | 124 | rexlimdva 2879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
     
                    |
126 | 94, 125 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                         |
127 | 126 | impd 433 |
. . . . . . . . . . . . . . . . . . . . . 22
    
          
              |
128 | 89, 127 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . 21
    
          
              |
129 | 128 | adantrl 722 |
. . . . . . . . . . . . . . . . . . . 20
    
       
      
        
              |
130 | 129 | ssrdv 3438 |
. . . . . . . . . . . . . . . . . . 19
    
       
      
                     |
131 | | simprl 764 |
. . . . . . . . . . . . . . . . . . 19
    
       
      
               |
132 | 130, 131 | sstrd 3442 |
. . . . . . . . . . . . . . . . . 18
    
       
      
          |
133 | | filss 20868 |
. . . . . . . . . . . . . . . . . 18
                 
     |
134 | 68, 87, 88, 132, 133 | syl13anc 1270 |
. . . . . . . . . . . . . . . . 17
    
       
      
    |
135 | 134 | exp32 610 |
. . . . . . . . . . . . . . . 16
      
            
    |
136 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . 19
      
          |
137 | 136 | imaeq2d 5168 |
. . . . . . . . . . . . . . . . . 18
               
         |
138 | 137 | sseq1d 3459 |
. . . . . . . . . . . . . . . . 17
          
 
              |
139 | 138 | imbi1d 319 |
. . . . . . . . . . . . . . . 16
                             
     |
140 | 135, 139 | syl5ibrcom 226 |
. . . . . . . . . . . . . . 15
      
          
 

     |
141 | 140 | rexlimdva 2879 |
. . . . . . . . . . . . . 14
 

                      |
142 | 141 | rexlimdvaa 2880 |
. . . . . . . . . . . . 13
                        |
143 | 142 | imp 431 |
. . . . . . . . . . . 12
 

  
                  |
144 | 67, 143 | syldan 473 |
. . . . . . . . . . 11
 
    
 
         
 

     |
145 | 65, 144 | sylbid 219 |
. . . . . . . . . 10
 
    
    
                    |
146 | 145 | impr 625 |
. . . . . . . . 9
 
    
                         |
147 | | imaeq2 5164 |
. . . . . . . . . . 11
          
    |
148 | 147 | sseq1d 3459 |
. . . . . . . . . 10
       
         |
149 | 148 | imbi1d 319 |
. . . . . . . . 9
                         |
150 | 146, 149 | syl5ibrcom 226 |
. . . . . . . 8
 
    
               
           |
151 | 150 | rexlimdvva 2886 |
. . . . . . 7
            
                     |
152 | 51, 59, 151 | 3jaod 1332 |
. . . . . 6
          
                 
                      |
153 | 49, 152 | sylbid 219 |
. . . . 5
                          |
154 | 153 | rexlimdv 2877 |
. . . 4
      
              
    |
155 | 154 | com23 81 |
. . 3
       
                  |
156 | 155 | impd 433 |
. 2
       
                  |
157 | 47, 156 | impbid 194 |
1
  
                       |