Step | Hyp | Ref
| Expression |
1 | | fnse.2 |
. . . . . . . 8
       |
2 | 1 | ffvelrnda 6045 |
. . . . . . 7
 
       |
3 | | fnse.3 |
. . . . . . . 8
 Se   |
4 | | seex 4816 |
. . . . . . . 8
  Se      
         |
5 | 3, 4 | sylan 478 |
. . . . . . 7
 
    

         |
6 | 2, 5 | syldan 477 |
. . . . . 6
 
 
         |
7 | | snex 4655 |
. . . . . 6
       |
8 | | unexg 6619 |
. . . . . 6
                  
                |
9 | 6, 7, 8 | sylancl 673 |
. . . . 5
 
  
                |
10 | | imaeq2 5183 |
. . . . . . . . 9
  
                                          |
11 | 10 | eleq1d 2524 |
. . . . . . . 8
  
                                            |
12 | 11 | imbi2d 322 |
. . . . . . 7
  
                     
                          |
13 | | fnse.4 |
. . . . . . 7
        |
14 | 12, 13 | vtoclg 3119 |
. . . . . 6
                                          |
15 | 14 | impcom 436 |
. . . . 5
 
                                        |
16 | 9, 15 | syldan 477 |
. . . 4
 
                        |
17 | | inss2 3665 |
. . . . . 6
        
        |
18 | | vex 3060 |
. . . . . . . . 9
 |
19 | | vex 3060 |
. . . . . . . . . 10
 |
20 | 19 | eliniseg 5216 |
. . . . . . . . 9
        
     |
21 | 18, 20 | ax-mp 5 |
. . . . . . . 8
            |
22 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
23 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
24 | 22, 23 | breqan12d 4432 |
. . . . . . . . . . 11
 
                         |
25 | 22, 23 | eqeqan12d 2478 |
. . . . . . . . . . . 12
 
                     |
26 | | breq12 4421 |
. . . . . . . . . . . 12
 
         |
27 | 25, 26 | anbi12d 722 |
. . . . . . . . . . 11
 
          
  
               |
28 | 24, 27 | orbi12d 721 |
. . . . . . . . . 10
 
                                             
       |
29 | | fnse.1 |
. . . . . . . . . 10
   
 
                    
       |
30 | 28, 29 | brab2ga 4929 |
. . . . . . . . 9
  
 
                    
       |
31 | 1 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . 17
 
       |
32 | 31 | adantrr 728 |
. . . . . . . . . . . . . . . 16
 

        |
33 | | breq1 4419 |
. . . . . . . . . . . . . . . . 17
           
             |
34 | 33 | elrab3 3209 |
. . . . . . . . . . . . . . . 16
          
      
             |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . 15
 

              
             |
36 | 35 | biimprd 231 |
. . . . . . . . . . . . . 14
 

                            |
37 | | simpl 463 |
. . . . . . . . . . . . . . . 16
                       |
38 | | fvex 5898 |
. . . . . . . . . . . . . . . . 17
     |
39 | 38 | elsnc 4004 |
. . . . . . . . . . . . . . . 16
                     |
40 | 37, 39 | sylibr 217 |
. . . . . . . . . . . . . . 15
                         |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
 

           
                |
42 | 36, 41 | orim12d 854 |
. . . . . . . . . . . . 13
 

                                                      |
43 | | elun 3586 |
. . . . . . . . . . . . 13
      
             
                          |
44 | 42, 43 | syl6ibr 235 |
. . . . . . . . . . . 12
 

                                                  |
45 | | simprl 769 |
. . . . . . . . . . . 12
 

 
  |
46 | 44, 45 | jctild 550 |
. . . . . . . . . . 11
 

                                                    |
47 | | ffn 5751 |
. . . . . . . . . . . . . 14
    
  |
48 | 1, 47 | syl 17 |
. . . . . . . . . . . . 13
   |
49 | 48 | adantr 471 |
. . . . . . . . . . . 12
 

 
  |
50 | | elpreima 6025 |
. . . . . . . . . . . 12
                                                |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
 

                                                 |
52 | 46, 51 | sylibrd 242 |
. . . . . . . . . 10
 

                                                   |
53 | 52 | expimpd 612 |
. . . . . . . . 9
                             
     
                  |
54 | 30, 53 | syl5bi 225 |
. . . . . . . 8
                            |
55 | 21, 54 | syl5bi 225 |
. . . . . . 7
                                 |
56 | 55 | ssrdv 3450 |
. . . . . 6
                               |
57 | 17, 56 | syl5ss 3455 |
. . . . 5
                                 |
58 | 57 | adantr 471 |
. . . 4
 
         
     
                 |
59 | 16, 58 | ssexd 4564 |
. . 3
 
            |
60 | 59 | ralrimiva 2814 |
. 2
  
          |
61 | | dfse2 5221 |
. 2
 Se  
          |
62 | 60, 61 | sylibr 217 |
1
 Se   |