Step | Hyp | Ref
| Expression |
1 | | df-ne 2634 |
. . . . . . . . 9
      
        |
2 | 1 | ralbii 2830 |
. . . . . . . 8
 
               |
3 | | tz7.49.2 |
. . . . . . . . 9
        
             |
4 | | ralim 2788 |
. . . . . . . . 9
 
      
          
 
                    |
5 | 3, 4 | sylbi 200 |
. . . . . . . 8
                       |
6 | 2, 5 | syl5bir 226 |
. . . . . . 7
                       |
7 | | tz7.49.1 |
. . . . . . . . 9
 |
8 | 7 | tz7.48-3 7186 |
. . . . . . . 8
 
         
  |
9 | | elex 3065 |
. . . . . . . 8
   |
10 | 8, 9 | nsyl3 124 |
. . . . . . 7
              |
11 | 6, 10 | nsyli 148 |
. . . . . 6
            |
12 | | dfrex2 2849 |
. . . . . 6
                 |
13 | 11, 12 | syl6ibr 235 |
. . . . 5
   
        |
14 | | imaeq2 5182 |
. . . . . . . 8
           |
15 | 14 | difeq2d 3562 |
. . . . . . 7
               |
16 | 15 | eqeq1d 2463 |
. . . . . 6
       
         |
17 | 16 | onminex 6660 |
. . . . 5
                          |
18 | 13, 17 | syl6 34 |
. . . 4
                     |
19 | | df-ne 2634 |
. . . . . . 7
      
        |
20 | 19 | ralbii 2830 |
. . . . . 6
 
               |
21 | 20 | anbi2i 705 |
. . . . 5
       

      
                 |
22 | 21 | rexbii 2900 |
. . . 4
        

      
                  |
23 | 18, 22 | syl6ibr 235 |
. . 3
           
         |
24 | | nfra1 2780 |
. . . . 5
  
                   |
25 | 3, 24 | nfxfr 1706 |
. . . 4
   |
26 | | simpllr 774 |
. . . . . . . . 9
                   

        |
27 | | fnfun 5694 |
. . . . . . . . . . . . . . . . 17
   |
28 | 7, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
29 | | fvelima 5939 |
. . . . . . . . . . . . . . . 16
       
      |
30 | 28, 29 | mpan 681 |
. . . . . . . . . . . . . . 15
     
      |
31 | | nfv 1771 |
. . . . . . . . . . . . . . . . 17
   |
32 | | nfra1 2780 |
. . . . . . . . . . . . . . . . 17
   
      |
33 | 31, 32 | nfan 2021 |
. . . . . . . . . . . . . . . 16
   
        |
34 | | nfv 1771 |
. . . . . . . . . . . . . . . 16
     |
35 | | rsp 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      
         |
36 | 35 | adantld 473 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                  |
37 | | onelon 5466 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
38 | 15 | neeq1d 2694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
39 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
40 | 39, 15 | eleq12d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
41 | 38, 40 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                         |
42 | 41 | rspcv 3157 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
                 
                     |
43 | 3, 42 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
44 | 43 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
               |
45 | 37, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                       |
46 | 36, 45 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . 21
 
                        |
47 | 46 | com3r 82 |
. . . . . . . . . . . . . . . . . . . 20
                          |
48 | 47 | imp 435 |
. . . . . . . . . . . . . . . . . . 19
 

                       |
49 | 48 | expcomd 444 |
. . . . . . . . . . . . . . . . . 18
 

                       |
50 | | eldifi 3566 |
. . . . . . . . . . . . . . . . . . 19
                 |
51 | | eleq1 2527 |
. . . . . . . . . . . . . . . . . . 19
         
   |
52 | 50, 51 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . . 18
                   |
53 | 49, 52 | syl8 72 |
. . . . . . . . . . . . . . . . 17
 

                   |
54 | 53 | com34 86 |
. . . . . . . . . . . . . . . 16
 

             
     |
55 | 33, 34, 54 | rexlimd 2882 |
. . . . . . . . . . . . . . 15
 

             
    |
56 | 30, 55 | syl5 33 |
. . . . . . . . . . . . . 14
 

            
    |
57 | 56 | com23 81 |
. . . . . . . . . . . . 13
 

                 |
58 | 57 | imp 435 |
. . . . . . . . . . . 12
   
      
         |
59 | 58 | ssrdv 3449 |
. . . . . . . . . . 11
   
      
       |
60 | | ssdif0 3834 |
. . . . . . . . . . . 12
    
        |
61 | 60 | biimpri 211 |
. . . . . . . . . . 11
      
      |
62 | 59, 61 | anim12i 574 |
. . . . . . . . . 10
                   
            |
63 | | eqss 3458 |
. . . . . . . . . 10
    
            |
64 | 62, 63 | sylibr 217 |
. . . . . . . . 9
                   
      |
65 | | onss 6643 |
. . . . . . . . . . . . 13
   |
66 | 32, 31 | nfan 2021 |
. . . . . . . . . . . . . . . . 17
            |
67 | | nfv 1771 |
. . . . . . . . . . . . . . . . 17

 |
68 | 66, 67 | nfan 2021 |
. . . . . . . . . . . . . . . 16
    
         |
69 | | nfv 1771 |
. . . . . . . . . . . . . . . . . 18
     
       
  |
70 | | ssel 3437 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
71 | | onss 6643 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
72 | | fndm 5696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
73 | 7, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
74 | 71, 73 | syl6sseqr 3490 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
75 | | funfvima2 6165 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
76 | 28, 74, 75 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
77 | 70, 76 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . 21

              |
78 | 35 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  

    
         |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  

    
          |
80 | 70, 79, 44 | syl10 75 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  

    
                |
81 | 80 | imp4a 598 |
. . . . . . . . . . . . . . . . . . . . . . 23

                         |
82 | | eldifn 3567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
83 | | eleq1a 2534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
84 | 83 | con3d 140 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
85 | 82, 84 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               |
86 | 81, 85 | syl8 72 |
. . . . . . . . . . . . . . . . . . . . . 22

                   
             |
87 | 86 | com34 86 |
. . . . . . . . . . . . . . . . . . . . 21

            
      
             |
88 | 77, 87 | syldd 68 |
. . . . . . . . . . . . . . . . . . . 20

    
      
             |
89 | 88 | com4r 89 |
. . . . . . . . . . . . . . . . . . 19
   
        
             |
90 | 89 | imp31 438 |
. . . . . . . . . . . . . . . . . 18
    
        

           |
91 | 69, 90 | ralrimi 2799 |
. . . . . . . . . . . . . . . . 17
    
        

          |
92 | 91 | ex 440 |
. . . . . . . . . . . . . . . 16
            

           |
93 | 68, 92 | ralrimi 2799 |
. . . . . . . . . . . . . . 15
             
          |
94 | 93 | ex 440 |
. . . . . . . . . . . . . 14
   
        
           |
95 | 94 | ancld 560 |
. . . . . . . . . . . . 13
   
         
            |
96 | 7 | tz7.48lem 7183 |
. . . . . . . . . . . . 13
 


              |
97 | 65, 95, 96 | syl56 35 |
. . . . . . . . . . . 12
   
             |
98 | 97 | ancoms 459 |
. . . . . . . . . . 11
 

              |
99 | 98 | imp 435 |
. . . . . . . . . 10
   
      
      |
100 | 99 | adantr 471 |
. . . . . . . . 9
                   
 
   |
101 | 26, 64, 100 | 3jca 1194 |
. . . . . . . 8
                   
 
           
    |
102 | 101 | exp41 619 |
. . . . . . 7
                
 
           
       |
103 | 102 | com23 81 |
. . . . . 6
                
 
           
       |
104 | 103 | com34 86 |
. . . . 5
                  

          
       |
105 | 104 | imp4a 598 |
. . . 4
                               
      |
106 | 25, 105 | reximdai 2867 |
. . 3
                  
  
          
     |
107 | 23, 106 | syld 45 |
. 2
     
          
     |
108 | 107 | impcom 436 |
1
  
  
           
    |