Step | Hyp | Ref
| Expression |
1 | | opex 4664 |
. . . . . . . . 9
            |
2 | | fvex 5889 |
. . . . . . . . 9
       |
3 | 1, 2 | relsnop 4944 |
. . . . . . . 8
             
         |
4 | 3 | rgenw 2768 |
. . . . . . 7

                 
     |
5 | | reliun 4959 |
. . . . . . 7
 
             
       

                 
      |
6 | 4, 5 | mpbir 214 |
. . . . . 6

                       |
7 | 6 | rgenw 2768 |
. . . . 5


                       |
8 | | reliun 4959 |
. . . . 5
 
              
       


                        |
9 | 7, 8 | mpbir 214 |
. . . 4

                        |
10 | | imasaddflem.a |
. . . . 5
 
                         |
11 | 10 | releqd 4924 |
. . . 4
 

                          |
12 | 9, 11 | mpbiri 241 |
. . 3

 |
13 | | imasaddf.f |
. . . . . . . . . . . . . . . . . 18
       |
14 | | fof 5806 |
. . . . . . . . . . . . . . . . . 18
           |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
16 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . 18
     
       |
17 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . 18
     
       |
18 | 16, 17 | anim12dan 855 |
. . . . . . . . . . . . . . . . 17
      
              |
19 | 15, 18 | sylan 479 |
. . . . . . . . . . . . . . . 16
 

              |
20 | | opelxpi 4871 |
. . . . . . . . . . . . . . . 16
                          |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
 

                 |
22 | | opelxpi 4871 |
. . . . . . . . . . . . . . 15
              
                   
             |
23 | 21, 2, 22 | sylancl 675 |
. . . . . . . . . . . . . 14
 

              
             |
24 | 23 | snssd 4108 |
. . . . . . . . . . . . 13
 

               
              |
25 | 24 | anassrs 660 |
. . . . . . . . . . . 12
                      
          |
26 | 25 | ralrimiva 2809 |
. . . . . . . . . . 11
 
 
                     
      |
27 | | iunss 4310 |
. . . . . . . . . . 11
 
             
                          
              |
28 | 26, 27 | sylibr 217 |
. . . . . . . . . 10
 
 
                     
      |
29 | 28 | ralrimiva 2809 |
. . . . . . . . 9
                
              |
30 | | iunss 4310 |
. . . . . . . . 9
 

                     
   

                      
      |
31 | 29, 30 | sylibr 217 |
. . . . . . . 8
                
              |
32 | 10, 31 | eqsstrd 3452 |
. . . . . . 7
       |
33 | | dmss 5039 |
. . . . . . 7
   
      |
34 | 32, 33 | syl 17 |
. . . . . 6

      |
35 | | vn0 3730 |
. . . . . . 7
 |
36 | | dmxp 5059 |
. . . . . . 7

        |
37 | 35, 36 | ax-mp 5 |
. . . . . 6
       |
38 | 34, 37 | syl6sseq 3464 |
. . . . 5

    |
39 | | forn 5809 |
. . . . . . 7
       |
40 | 13, 39 | syl 17 |
. . . . . 6
   |
41 | 40 | sqxpeqd 4865 |
. . . . 5
       |
42 | 38, 41 | sseqtr4d 3455 |
. . . 4

    |
43 | 10 | eleq2d 2534 |
. . . . . . . . . . . . 13
              
             
                
           |
44 | 43 | adantr 472 |
. . . . . . . . . . . 12
 

               
             
                
           |
45 | | df-br 4396 |
. . . . . . . . . . . 12
                        
  |
46 | | eliun 4274 |
. . . . . . . . . . . . 13
              

                                    
               
          |
47 | | eliun 4274 |
. . . . . . . . . . . . . 14
              

                                   
              
          |
48 | 47 | rexbii 2881 |
. . . . . . . . . . . . 13
               

                       
            
              
          |
49 | 46, 48 | bitr2i 258 |
. . . . . . . . . . . 12
  
             
                 
   
                                        |
50 | 44, 45, 49 | 3bitr4g 296 |
. . . . . . . . . . 11
 

             


                                       |
51 | | opex 4664 |
. . . . . . . . . . . . . . 15
               |
52 | 51 | elsnc 3984 |
. . . . . . . . . . . . . 14
              
                 
   
                          
         |
53 | | opex 4664 |
. . . . . . . . . . . . . . . 16
            |
54 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
55 | 53, 54 | opth 4676 |
. . . . . . . . . . . . . . 15
              
                
  
                          
     |
56 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . 19
     |
57 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . 19
     |
58 | 56, 57 | opth 4676 |
. . . . . . . . . . . . . . . . . 18
                                           |
59 | | imasaddf.e |
. . . . . . . . . . . . . . . . . 18
 

 
 
                      
           |
60 | 58, 59 | syl5bi 225 |
. . . . . . . . . . . . . . . . 17
 

 
 
                                
     |
61 | | eqeq2 2482 |
. . . . . . . . . . . . . . . . . 18
          
 
      
         |
62 | 61 | biimprd 231 |
. . . . . . . . . . . . . . . . 17
          
 
    
 
         |
63 | 60, 62 | syl6 33 |
. . . . . . . . . . . . . . . 16
 

 
 
                             
          |
64 | 63 | impd 438 |
. . . . . . . . . . . . . . 15
 

 
 
                              
         |
65 | 55, 64 | syl5bi 225 |
. . . . . . . . . . . . . 14
 

 
 
              
                
  
   
     |
66 | 52, 65 | syl5bi 225 |
. . . . . . . . . . . . 13
 

 
 
              
                 
             |
67 | 66 | 3expa 1231 |
. . . . . . . . . . . 12
   
 

               
              
                 |
68 | 67 | rexlimdvva 2878 |
. . . . . . . . . . 11
 

                 
              
                 |
69 | 50, 68 | sylbid 223 |
. . . . . . . . . 10
 

                       |
70 | 69 | alrimiv 1781 |
. . . . . . . . 9
 

                         |
71 | | mo2icl 3205 |
. . . . . . . . 9
                                     |
72 | 70, 71 | syl 17 |
. . . . . . . 8
 

                 |
73 | 72 | ralrimivva 2814 |
. . . . . . 7
  
               |
74 | | fofn 5808 |
. . . . . . . . . 10
    
  |
75 | 13, 74 | syl 17 |
. . . . . . . . 9
   |
76 | | opeq2 4159 |
. . . . . . . . . . . 12
                         |
77 | 76 | breq1d 4405 |
. . . . . . . . . . 11
                           |
78 | 77 | mobidv 2340 |
. . . . . . . . . 10
              
                |
79 | 78 | ralrn 6040 |
. . . . . . . . 9
  
                           |
80 | 75, 79 | syl 17 |
. . . . . . . 8
                              |
81 | 80 | ralbidv 2829 |
. . . . . . 7
               
                |
82 | 73, 81 | mpbird 240 |
. . . . . 6
  
            |
83 | | opeq1 4158 |
. . . . . . . . . . 11
                 |
84 | 83 | breq1d 4405 |
. . . . . . . . . 10
                   |
85 | 84 | mobidv 2340 |
. . . . . . . . 9
          
            |
86 | 85 | ralbidv 2829 |
. . . . . . . 8
      
                    |
87 | 86 | ralrn 6040 |
. . . . . . 7
  
         
             |
88 | 75, 87 | syl 17 |
. . . . . 6
            
             |
89 | 82, 88 | mpbird 240 |
. . . . 5
            |
90 | | breq1 4398 |
. . . . . . 7
           |
91 | 90 | mobidv 2340 |
. . . . . 6
     
        |
92 | 91 | ralxp 4981 |
. . . . 5
 
               |
93 | 89, 92 | sylibr 217 |
. . . 4
        |
94 | | ssralv 3479 |
. . . 4
         
    |
95 | 42, 93, 94 | sylc 61 |
. . 3
     |
96 | | dffun7 5615 |
. . 3
  
    |
97 | 12, 95, 96 | sylanbrc 677 |
. 2

 |
98 | | eqimss2 3471 |
. . . . . . . . . . 11
               
         
             
         |
99 | 10, 98 | syl 17 |
. . . . . . . . . 10
                
         |
100 | | iunss 4310 |
. . . . . . . . . 10
 

                     

                      
 |
101 | 99, 100 | sylib 201 |
. . . . . . . . 9
                
         |
102 | | iunss 4310 |
. . . . . . . . . . 11
 
             
                      
         |
103 | | opex 4664 |
. . . . . . . . . . . . . 14
                     |
104 | 103 | snss 4087 |
. . . . . . . . . . . . 13
                 
  
                     
 |
105 | 1, 2 | opeldm 5044 |
. . . . . . . . . . . . 13
                 
  
          
 |
106 | 104, 105 | sylbir 218 |
. . . . . . . . . . . 12
              
                    |
107 | 106 | ralimi 2796 |
. . . . . . . . . . 11
 
             
                   
 |
108 | 102, 107 | sylbi 200 |
. . . . . . . . . 10
 
             
                   
 |
109 | 108 | ralimi 2796 |
. . . . . . . . 9
 

                     


            |
110 | 101, 109 | syl 17 |
. . . . . . . 8
  
          
 |
111 | | opeq2 4159 |
. . . . . . . . . . . 12
                         |
112 | 111 | eleq1d 2533 |
. . . . . . . . . . 11
            
             |
113 | 112 | ralrn 6040 |
. . . . . . . . . 10
  
       
           
  |
114 | 75, 113 | syl 17 |
. . . . . . . . 9
                         |
115 | 114 | ralbidv 2829 |
. . . . . . . 8
             
             |
116 | 110, 115 | mpbird 240 |
. . . . . . 7
  
       
 |
117 | | opeq1 4158 |
. . . . . . . . . . 11
                 |
118 | 117 | eleq1d 2533 |
. . . . . . . . . 10
        
         |
119 | 118 | ralbidv 2829 |
. . . . . . . . 9
      
   
        
  |
120 | 119 | ralrn 6040 |
. . . . . . . 8
  
     
 
       
  |
121 | 75, 120 | syl 17 |
. . . . . . 7
          
          |
122 | 116, 121 | mpbird 240 |
. . . . . 6
       
 |
123 | | eleq1 2537 |
. . . . . . 7
          |
124 | 123 | ralxp 4981 |
. . . . . 6
 
  
        |
125 | 122, 124 | sylibr 217 |
. . . . 5
      |
126 | | dfss3 3408 |
. . . . 5
  
     |
127 | 125, 126 | sylibr 217 |
. . . 4
    |
128 | 41, 127 | eqsstr3d 3453 |
. . 3
  
 |
129 | 38, 128 | eqssd 3435 |
. 2

    |
130 | | df-fn 5592 |
. 2
        |
131 | 97, 129, 130 | sylanbrc 677 |
1

    |