Step | Hyp | Ref
| Expression |
1 | | vfinspeqtncv 4554 |
. . 3
 Fin Spfin   
Spfin
Tfin  Ncfin     |
2 | | ncfineq 4474 |
. . 3
Spfin   
Spfin
Tfin  Ncfin   Ncfin Spfin Ncfin  
 Spfin Tfin
 Ncfin     |
3 | 1, 2 | syl 15 |
. 2
 Fin Ncfin Spfin Ncfin  
 Spfin Tfin
 Ncfin     |
4 | | vfinncvntsp 4550 |
. . . 4
 Fin Ncfin   Spfin Tfin
   |
5 | | disjsn 3787 |
. . . 4
   
Spfin Tfin  Ncfin   Ncfin
  Spfin Tfin
   |
6 | 4, 5 | sylibr 203 |
. . 3
 Fin   
Spfin Tfin  Ncfin     |
7 | | vex 2863 |
. . . . . . . . 9
 |
8 | 7 | elimak 4260 |
. . . . . . . 8
        k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     k 1 Spfin  1 Spfin  
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
9 | | df-rex 2621 |
. . . . . . . . 9
 
1 Spfin  
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      
1 Spfin          k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
10 | | elpw1 4145 |
. . . . . . . . . . . . 13
 1 Spfin  Spfin     |
11 | 10 | anbi1i 676 |
. . . . . . . . . . . 12
  1 Spfin          k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       Spfin
           k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
12 | | r19.41v 2765 |
. . . . . . . . . . . 12
 
Spfin             k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       Spfin
           k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
13 | 11, 12 | bitr4i 243 |
. . . . . . . . . . 11
  1 Spfin          k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      Spfin 
    
      k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
14 | 13 | exbii 1582 |
. . . . . . . . . 10
    1 Spfin          k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k        Spfin             k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
15 | | rexcom4 2879 |
. . . . . . . . . 10
 
Spfin               k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k        Spfin             k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
16 | 14, 15 | bitr4i 243 |
. . . . . . . . 9
    1 Spfin          k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      Spfin               k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
17 | 9, 16 | bitri 240 |
. . . . . . . 8
 
1 Spfin  
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     Spfin   
    
      k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
18 | 8, 17 | bitri 240 |
. . . . . . 7
        k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     k 1 Spfin  Spfin               k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
19 | | snex 4112 |
. . . . . . . . . 10
 
 |
20 | | opkeq1 4060 |
. . . . . . . . . . 11
             |
21 | 20 | eleq1d 2419 |
. . . . . . . . . 10
             k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
22 | 19, 21 | ceqsexv 2895 |
. . . . . . . . 9
        
      k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k                k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
23 | | vex 2863 |
. . . . . . . . . 10
 |
24 | 23, 7 | eqtfinrelk 4487 |
. . . . . . . . 9
            k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k    Tfin
  |
25 | 22, 24 | bitri 240 |
. . . . . . . 8
        
      k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     Tfin   |
26 | 25 | rexbii 2640 |
. . . . . . 7
 
Spfin               k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      Spfin
Tfin   |
27 | 18, 26 | bitri 240 |
. . . . . 6
        k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     k 1 Spfin  Spfin
Tfin   |
28 | 27 | eqabi 2465 |
. . . . 5
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     k 1 Spfin
  Spfin
Tfin   |
29 | | tfinrelkex 4488 |
. . . . . 6
      k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     |
30 | | spfinex 4538 |
. . . . . . 7
Spfin  |
31 | 30 | pw1ex 4304 |
. . . . . 6
1 Spfin  |
32 | 29, 31 | imakex 4301 |
. . . . 5
       k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k     k 1 Spfin
 |
33 | 28, 32 | eqeltrri 2424 |
. . . 4
  Spfin
Tfin   |
34 | | snex 4112 |
. . . . 5
Ncfin   |
35 | | ncfindi 4476 |
. . . . 5
   Fin  
Spfin
Tfin   Ncfin 
 
 Spfin Tfin
 Ncfin  
 Ncfin  
 Spfin Tfin
 Ncfin  
Ncfin 
 Spfin Tfin
 Ncfin Ncfin     |
36 | 34, 35 | mp3an2 1265 |
. . . 4
   Fin  
Spfin
Tfin     
Spfin
Tfin  Ncfin    Ncfin  
 Spfin Tfin
 Ncfin  
Ncfin 
 Spfin Tfin
 Ncfin Ncfin     |
37 | 33, 36 | mpanl2 662 |
. . 3
  Fin    Spfin
Tfin  Ncfin    Ncfin  
 Spfin Tfin
 Ncfin  
Ncfin 
 Spfin Tfin
 Ncfin Ncfin     |
38 | 6, 37 | mpdan 649 |
. 2
 Fin Ncfin   
Spfin Tfin  Ncfin   Ncfin
  Spfin
Tfin  Ncfin Ncfin     |
39 | | ncfinprop 4475 |
. . . . . 6
  Fin  
Spfin
Tfin   Ncfin 
 Spfin Tfin
 Nn   Spfin Tfin
 Ncfin   Spfin
Tfin     |
40 | 33, 39 | mpan2 652 |
. . . . 5
 Fin Ncfin   Spfin
Tfin  Nn  
Spfin
Tfin  Ncfin 
 Spfin Tfin
    |
41 | 40 | simpld 445 |
. . . 4
 Fin Ncfin 
 Spfin Tfin
 Nn  |
42 | | ncfinprop 4475 |
. . . . . . 7
  Fin Spfin 
Ncfin Spfin Nn Spfin Ncfin Spfin   |
43 | 30, 42 | mpan2 652 |
. . . . . 6
 Fin Ncfin Spfin Nn Spfin Ncfin Spfin   |
44 | 43 | simpld 445 |
. . . . 5
 Fin Ncfin Spfin Nn  |
45 | | tfincl 4493 |
. . . . 5
Ncfin Spfin Nn Tfin Ncfin Spfin Nn  |
46 | 44, 45 | syl 15 |
. . . 4
 Fin Tfin
Ncfin Spfin Nn  |
47 | 40 | simprd 449 |
. . . 4
 Fin 
 Spfin Tfin
 Ncfin   Spfin
Tfin    |
48 | | vfinspnn 4542 |
. . . . . 6
 Fin Spfin Nn      |
49 | | difss 3394 |
. . . . . 6
Nn    Nn |
50 | 48, 49 | syl6ss 3285 |
. . . . 5
 Fin Spfin Nn  |
51 | 43 | simprd 449 |
. . . . 5
 Fin Spfin Ncfin Spfin  |
52 | | tfinnn 4535 |
. . . . 5
 Ncfin
Spfin Nn Spfin Nn Spfin Ncfin Spfin  
Spfin
Tfin  Tfin Ncfin Spfin  |
53 | 44, 50, 51, 52 | syl3anc 1182 |
. . . 4
 Fin 
 Spfin Tfin
 Tfin Ncfin Spfin  |
54 | | nnceleq 4431 |
. . . 4
  Ncfin 
 Spfin Tfin
 Nn Tfin Ncfin Spfin Nn   
Spfin
Tfin  Ncfin 
 Spfin Tfin
  
Spfin Tfin 
Tfin Ncfin Spfin 
Ncfin 
 Spfin Tfin
 Tfin Ncfin Spfin  |
55 | 41, 46, 47, 53, 54 | syl22anc 1183 |
. . 3
 Fin Ncfin 
 Spfin Tfin
 Tfin Ncfin Spfin  |
56 | | ncfinex 4473 |
. . . 4
Ncfin  |
57 | | ncfinsn 4477 |
. . . 4
  Fin Ncfin  Ncfin Ncfin  1c |
58 | 56, 57 | mpan2 652 |
. . 3
 Fin Ncfin Ncfin  1c |
59 | 55, 58 | addceq12d 4392 |
. 2
 Fin Ncfin   Spfin
Tfin  Ncfin Ncfin  
Tfin Ncfin Spfin 1c  |
60 | 3, 38, 59 | 3eqtrd 2389 |
1
 Fin Ncfin Spfin
Tfin Ncfin Spfin 1c  |