Step | Hyp | Ref
| Expression |
1 | | dffun7 5076 |
. . . . . . . . . 10
          |
2 | 1 | simprbi 270 |
. . . . . . . . 9

       |
3 | 2 | 3ad2ant1 967 |
. . . . . . . 8
 
        |
4 | | ssralv 3100 |
. . . . . . . . 9

     

      |
5 | 4 | 3ad2ant3 969 |
. . . . . . . 8
 
  
   

      |
6 | 3, 5 | mpd 13 |
. . . . . . 7
 
 
     |
7 | 6 | alrimiv 1809 |
. . . . . 6
 
   

    |
8 | | sseq1 3062 |
. . . . . . . . . . . . . . . . 17
 
   |
9 | 8 | biimpar 292 |
. . . . . . . . . . . . . . . 16
     |
10 | 9 | 3adant1 964 |
. . . . . . . . . . . . . . 15
 
   |
11 | | simp1 946 |
. . . . . . . . . . . . . . 15
 
   |
12 | 10, 11 | jca 301 |
. . . . . . . . . . . . . 14
 
 
   |
13 | | dffun8 5077 |
. . . . . . . . . . . . . . . . . 18
          |
14 | 13 | simprbi 270 |
. . . . . . . . . . . . . . . . 17

       |
15 | 14 | adantl 272 |
. . . . . . . . . . . . . . . 16
 
        |
16 | | ssel 3033 |
. . . . . . . . . . . . . . . . 17


   |
17 | 16 | adantr 271 |
. . . . . . . . . . . . . . . 16
 
 
   |
18 | | rsp 2434 |
. . . . . . . . . . . . . . . 16
 
    
      |
19 | 15, 17, 18 | sylsyld 58 |
. . . . . . . . . . . . . . 15
 
  
     |
20 | 19 | ralrimiv 2457 |
. . . . . . . . . . . . . 14
 
 
     |
21 | | zfrep6 3977 |
. . . . . . . . . . . . . 14
 
           |
22 | 12, 20, 21 | 3syl 17 |
. . . . . . . . . . . . 13
 
   

    |
23 | | raleq 2576 |
. . . . . . . . . . . . . . 15
  

 


     |
24 | 23 | exbidv 1760 |
. . . . . . . . . . . . . 14
                 |
25 | 24 | 3ad2ant2 968 |
. . . . . . . . . . . . 13
 
                 |
26 | 22, 25 | mpbid 146 |
. . . . . . . . . . . 12
 
   

    |
27 | 26 | 3com12 1150 |
. . . . . . . . . . 11
     

    |
28 | 27 | 3expib 1149 |
. . . . . . . . . 10
  
   

     |
29 | 28 | vtocleg 2704 |
. . . . . . . . 9
  
   

     |
30 | 29 | 3impib 1144 |
. . . . . . . 8
     

    |
31 | 30 | 3com12 1150 |
. . . . . . 7
 
   

    |
32 | | df-rex 2376 |
. . . . . . . . . 10
   
        |
33 | | exancom 1551 |
. . . . . . . . . 10
      
        |
34 | 32, 33 | bitri 183 |
. . . . . . . . 9
   
        |
35 | 34 | ralbii 2395 |
. . . . . . . 8
 

 

        |
36 | 35 | exbii 1548 |
. . . . . . 7
              
   |
37 | 31, 36 | sylib 121 |
. . . . . 6
 
   
        |
38 | | 19.29 1563 |
. . . . . . 7
    
                
   
         |
39 | | nfcv 2235 |
. . . . . . . . . . 11
   |
40 | | nfmo1 1967 |
. . . . . . . . . . 11
      |
41 | 39, 40 | nfralxy 2425 |
. . . . . . . . . 10
   
   |
42 | | nfe1 1437 |
. . . . . . . . . . 11
         |
43 | 39, 42 | nfralxy 2425 |
. . . . . . . . . 10
          |
44 | 41, 43 | nfan 1509 |
. . . . . . . . 9
       
        |
45 | | r19.26 2511 |
. . . . . . . . . 10
 
 
 
      
 
             |
46 | | mopick 2033 |
. . . . . . . . . . 11
                  |
47 | 46 | ralimi 2449 |
. . . . . . . . . 10
 
 
 
       
      |
48 | 45, 47 | sylbir 134 |
. . . . . . . . 9
   
 

       
      |
49 | 44, 48 | alrimi 1467 |
. . . . . . . 8
   
 

         
      |
50 | 49 | eximi 1543 |
. . . . . . 7
    
   
           
      |
51 | 38, 50 | syl 14 |
. . . . . 6
    
                 
      |
52 | 7, 37, 51 | syl2anc 404 |
. . . . 5
 
        
   |
53 | | r19.23v 2494 |
. . . . . . 7
 
           |
54 | 53 | albii 1411 |
. . . . . 6
                 |
55 | 54 | exbii 1548 |
. . . . 5
     
               |
56 | 52, 55 | sylib 121 |
. . . 4
 
      
 
   |
57 | | abss 3105 |
. . . . 5
  
      
 
   |
58 | 57 | exbii 1548 |
. . . 4
                   |
59 | 56, 58 | sylibr 133 |
. . 3
 
    
     |
60 | | dfima2 4809 |
. . . . 5
     
    |
61 | 60 | sseq1i 3065 |
. . . 4
    
       |
62 | 61 | exbii 1548 |
. . 3
                |
63 | 59, 62 | sylibr 133 |
. 2
 
      
  |
64 | | vex 2636 |
. . . 4
 |
65 | 64 | ssex 3997 |
. . 3
           |
66 | 65 | exlimiv 1541 |
. 2
             |
67 | 63, 66 | syl 14 |
1
 
       |