Step | Hyp | Ref
| Expression |
1 | | spfinex 4537 |
. . 3
Spfin  |
2 | | inexg 4100 |
. . 3
 Spfin
 Spfin 
  |
3 | 1, 2 | mpan 651 |
. 2
 Spfin    |
4 | | ncvspfin 4538 |
. . 3
Ncfin Spfin |
5 | | elin 3219 |
. . . 4
Ncfin Spfin  Ncfin Spfin Ncfin    |
6 | 5 | biimpri 197 |
. . 3
 Ncfin
Spfin Ncfin 
Ncfin Spfin    |
7 | 4, 6 | mpan 651 |
. 2
Ncfin Ncfin Spfin    |
8 | | elin 3219 |
. . . . 5
 Spfin   Spfin
   |
9 | | spfinsfincl 4539 |
. . . . . . . . . . . . . 14
  Spfin Sfin     Spfin  |
10 | 9 | adantrl 696 |
. . . . . . . . . . . . 13
  Spfin  Sfin      Spfin
 |
11 | 10 | a1d 22 |
. . . . . . . . . . . 12
  Spfin  Sfin       Spfin   |
12 | 11 | ancrd 537 |
. . . . . . . . . . 11
  Spfin  Sfin       
Spfin     |
13 | | elin 3219 |
. . . . . . . . . . 11
 Spfin   Spfin
   |
14 | 12, 13 | syl6ibr 218 |
. . . . . . . . . 10
  Spfin  Sfin      
Spfin     |
15 | 14 | ex 423 |
. . . . . . . . 9
 Spfin   Sfin      Spfin      |
16 | 15 | a2d 23 |
. . . . . . . 8
 Spfin    Sfin       
Sfin     Spfin      |
17 | 16 | exp4a 589 |
. . . . . . 7
 Spfin    Sfin      
Sfin   
Spfin       |
18 | 17 | a2i 12 |
. . . . . 6
  Spfin   Sfin       
Spfin  Sfin  
 Spfin       |
19 | 18 | imp3a 420 |
. . . . 5
  Spfin   Sfin         Spfin
 Sfin    Spfin      |
20 | 8, 19 | syl5bi 208 |
. . . 4
  Spfin   Sfin       
Spfin  Sfin    Spfin      |
21 | 20 | 2alimi 1560 |
. . 3
      Spfin   Sfin            Spfin 
Sfin    Spfin      |
22 | | df-ral 2619 |
. . . 4
 
Spfin     Sfin        
Spfin     Sfin         |
23 | | 19.21v 1890 |
. . . . 5
    Spfin   Sfin        Spfin     Sfin         |
24 | 23 | albii 1566 |
. . . 4
      Spfin   Sfin          Spfin     Sfin         |
25 | 22, 24 | bitr4i 243 |
. . 3
 
Spfin     Sfin           Spfin
 
Sfin         |
26 | | df-ral 2619 |
. . . 4
 
Spfin     Sfin   
Spfin     
Spfin   
Sfin    Spfin      |
27 | | 19.21v 1890 |
. . . . 5
    Spfin
 Sfin    Spfin     Spfin
   Sfin
  
Spfin      |
28 | 27 | albii 1566 |
. . . 4
      Spfin  Sfin    Spfin       Spfin 
  Sfin   
Spfin      |
29 | 26, 28 | bitr4i 243 |
. . 3
 
Spfin     Sfin   
Spfin        Spfin 
Sfin    Spfin      |
30 | 21, 25, 29 | 3imtr4i 257 |
. 2
 
Spfin     Sfin      
Spfin     Sfin   
Spfin     |
31 | | df-spfin 4447 |
. . . 4
Spfin   Ncfin

  Sfin   
    |
32 | | eleq2 2414 |
. . . . . . . . 9
 Spfin  Ncfin Ncfin Spfin     |
33 | | eleq2 2414 |
. . . . . . . . . . . 12
 Spfin  
Spfin     |
34 | 33 | imbi2d 307 |
. . . . . . . . . . 11
 Spfin   Sfin   
 Sfin   
Spfin      |
35 | 34 | albidv 1625 |
. . . . . . . . . 10
 Spfin     Sfin       Sfin    Spfin      |
36 | 35 | raleqbi1dv 2815 |
. . . . . . . . 9
 Spfin   
  Sfin     
Spfin     Sfin   
Spfin      |
37 | 32, 36 | anbi12d 691 |
. . . . . . . 8
 Spfin   Ncfin    Sfin
     Ncfin Spfin  
Spfin     Sfin   
Spfin       |
38 | 37 | elabg 2986 |
. . . . . . 7
 Spfin


Spfin 

Ncfin 
 
Sfin       Ncfin Spfin  
Spfin     Sfin   
Spfin       |
39 | 38 | biimprd 214 |
. . . . . 6
 Spfin


Ncfin Spfin  
Spfin     Sfin   
Spfin    Spfin 

Ncfin 
 
Sfin          |
40 | 39 | 3impib 1149 |
. . . . 5
  Spfin 
Ncfin
Spfin   Spfin     Sfin
  
Spfin    Spfin 

Ncfin 
 
Sfin         |
41 | | intss1 3941 |
. . . . 5
 Spfin


Ncfin 
 
Sfin         Ncfin 
 
Sfin       Spfin    |
42 | 40, 41 | syl 15 |
. . . 4
  Spfin 
Ncfin
Spfin   Spfin     Sfin
  
Spfin      Ncfin
   Sfin
      Spfin    |
43 | 31, 42 | syl5eqss 3315 |
. . 3
  Spfin 
Ncfin
Spfin   Spfin     Sfin
  
Spfin    Spfin Spfin    |
44 | | inss2 3476 |
. . 3
Spfin   |
45 | 43, 44 | syl6ss 3284 |
. 2
  Spfin 
Ncfin
Spfin   Spfin     Sfin
  
Spfin    Spfin   |
46 | 3, 7, 30, 45 | syl3an 1224 |
1
  Ncfin 
Spfin     Sfin       Spfin   |