Step | Hyp | Ref
| Expression |
1 | | simpl 443 |
. . . . . 6
  Fin Spfin Fin  |
2 | | vfinspnn 4542 |
. . . . . . . 8
 Fin Spfin Nn      |
3 | | difss 3394 |
. . . . . . . 8
Nn    Nn |
4 | 2, 3 | syl6ss 3285 |
. . . . . . 7
 Fin Spfin Nn  |
5 | 4 | sselda 3274 |
. . . . . 6
  Fin Spfin Nn  |
6 | 2 | sselda 3274 |
. . . . . . 7
  Fin Spfin Nn      |
7 | | eldifsn 3840 |
. . . . . . . 8
 Nn    
Nn    |
8 | 7 | simprbi 450 |
. . . . . . 7
 Nn      |
9 | 6, 8 | syl 15 |
. . . . . 6
  Fin Spfin   |
10 | | vfintle 4547 |
. . . . . 6
  Fin Nn  Tfin  Ncfin 1c fin  |
11 | 1, 5, 9, 10 | syl3anc 1182 |
. . . . 5
  Fin Spfin
Tfin  Ncfin
1c fin  |
12 | 11 | ad2ant2r 727 |
. . . 4
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin 
Ncfin 1c fin  |
13 | | t1csfin1c 4546 |
. . . . . . . 8
 Fin Sfin
Tfin Ncfin 1c Ncfin 1c  |
14 | 13 | adantr 451 |
. . . . . . 7
  Fin Tfin Spfin Sfin
Tfin Ncfin 1c Ncfin 1c  |
15 | | simpr 447 |
. . . . . . 7
  Spfin Sfin   Tfin  
Sfin   Tfin    |
16 | | sfinltfin 4536 |
. . . . . . . 8
  Sfin Tfin Ncfin 1c Ncfin 1c Sfin   Tfin  
Tfin Ncfin 1c  fin Ncfin 1c Tfin  fin  |
17 | 16 | ex 423 |
. . . . . . 7
 Sfin
Tfin Ncfin 1c Ncfin 1c Sfin   Tfin  
 Tfin Ncfin 1c  fin
Ncfin 1c Tfin  fin   |
18 | 14, 15, 17 | syl2an 463 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin     Tfin Ncfin 1c  fin
Ncfin 1c Tfin  fin   |
19 | 18 | con3d 125 |
. . . . 5
   Fin Tfin Spfin 
Spfin Sfin   Tfin     Ncfin
1c
Tfin  fin Tfin Ncfin 1c  fin   |
20 | 5 | ad2ant2r 727 |
. . . . . . 7
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Nn  |
21 | | tfincl 4493 |
. . . . . . 7
 Nn Tfin Nn  |
22 | 20, 21 | syl 15 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin
Nn  |
23 | | 1cex 4143 |
. . . . . . . . 9
1c
 |
24 | | ncfinprop 4475 |
. . . . . . . . 9
  Fin 1c  Ncfin
1c
Nn 1c Ncfin
1c  |
25 | 23, 24 | mpan2 652 |
. . . . . . . 8
 Fin Ncfin
1c
Nn 1c Ncfin
1c  |
26 | 25 | ad2antrr 706 |
. . . . . . 7
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Ncfin 1c Nn 1c
Ncfin 1c  |
27 | 26 | simpld 445 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Ncfin 1c Nn  |
28 | | lenltfin 4470 |
. . . . . 6
 Tfin
Nn Ncfin 1c Nn  Tfin  Ncfin
1c fin Ncfin 1c Tfin  fin   |
29 | 22, 27, 28 | syl2anc 642 |
. . . . 5
   Fin Tfin Spfin 
Spfin Sfin   Tfin     Tfin  Ncfin 1c fin Ncfin 1c Tfin  fin   |
30 | | df-sfin 4447 |
. . . . . . . 8
Sfin   Tfin 
 Nn Tfin
Nn    1

Tfin     |
31 | 30 | simp1bi 970 |
. . . . . . 7
Sfin   Tfin 
Nn  |
32 | 31 | ad2antll 709 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Nn  |
33 | | tfincl 4493 |
. . . . . . 7
Ncfin 1c Nn Tfin Ncfin 1c Nn  |
34 | 27, 33 | syl 15 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin Ncfin 1c Nn  |
35 | | lenltfin 4470 |
. . . . . 6
  Nn Tfin Ncfin 1c Nn    Tfin Ncfin 1c fin Tfin Ncfin 1c  fin   |
36 | 32, 34, 35 | syl2anc 642 |
. . . . 5
   Fin Tfin Spfin 
Spfin Sfin   Tfin       Tfin Ncfin 1c fin Tfin Ncfin 1c  fin   |
37 | 19, 29, 36 | 3imtr4d 259 |
. . . 4
   Fin Tfin Spfin 
Spfin Sfin   Tfin     Tfin  Ncfin 1c fin  
Tfin Ncfin 1c fin   |
38 | 12, 37 | mpd 14 |
. . 3
   Fin Tfin Spfin 
Spfin Sfin   Tfin      Tfin Ncfin 1c fin  |
39 | | vex 2863 |
. . . 4
 |
40 | | tfinex 4486 |
. . . 4
Tfin Ncfin 1c  |
41 | | opklefing 4449 |
. . . 4
  Tfin Ncfin 1c 
   Tfin Ncfin 1c fin  Nn Tfin Ncfin 1c 
    |
42 | 39, 40, 41 | mp2an 653 |
. . 3
   Tfin Ncfin 1c fin  Nn Tfin Ncfin 1c 
   |
43 | 38, 42 | sylib 188 |
. 2
   Fin Tfin Spfin 
Spfin Sfin   Tfin    
Nn Tfin
Ncfin 1c     |
44 | | df1c2 4169 |
. . . . . . 7
1c
1  |
45 | | pw1eq 4144 |
. . . . . . 7
1c 1 1 1c 1 1   |
46 | 44, 45 | ax-mp 5 |
. . . . . 6
1
1c
1 1  |
47 | | tfinpw1 4495 |
. . . . . . 7
 Ncfin
1c
Nn 1c Ncfin
1c
1
1c
Tfin Ncfin 1c |
48 | 26, 47 | syl 15 |
. . . . . 6
   Fin Tfin Spfin 
Spfin Sfin   Tfin    1 1c Tfin Ncfin 1c |
49 | 46, 48 | syl5eqelr 2438 |
. . . . 5
   Fin Tfin Spfin 
Spfin Sfin   Tfin    1 1 Tfin Ncfin 1c |
50 | | eleq2 2414 |
. . . . 5
Tfin Ncfin 1c 
  1 1 Tfin Ncfin 1c 1 1 
    |
51 | 49, 50 | syl5ibcom 211 |
. . . 4
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin Ncfin 1c 
 1 1      |
52 | | eladdc 4399 |
. . . . 5
 1 1  


   1 1      |
53 | | ssun1 3427 |
. . . . . . . . . . 11

  |
54 | | sseq2 3294 |
. . . . . . . . . . 11
 1 1    1 1      |
55 | 53, 54 | mpbiri 224 |
. . . . . . . . . 10
 1 1   1 1   |
56 | | vex 2863 |
. . . . . . . . . . . 12
 |
57 | 56 | sspw1 4336 |
. . . . . . . . . . 11
 1 1   
1
1    |
58 | | vex 2863 |
. . . . . . . . . . . . . . . 16
 |
59 | 58 | sspw1 4336 |
. . . . . . . . . . . . . . 15
 1   
1    |
60 | | ssv 3292 |
. . . . . . . . . . . . . . . . 17
 |
61 | 60 | biantrur 492 |
. . . . . . . . . . . . . . . 16
 1
 1    |
62 | 61 | exbii 1582 |
. . . . . . . . . . . . . . 15
 
1    1    |
63 | 59, 62 | bitr4i 243 |
. . . . . . . . . . . . . 14
 1  1   |
64 | 63 | anbi1i 676 |
. . . . . . . . . . . . 13
 
1
1    1
1    |
65 | | 19.41v 1901 |
. . . . . . . . . . . . 13
    1
1   
1
1    |
66 | 64, 65 | bitr4i 243 |
. . . . . . . . . . . 12
 
1
1     1
1    |
67 | 66 | exbii 1582 |
. . . . . . . . . . 11
    1 1      
1
1    |
68 | | excom 1741 |
. . . . . . . . . . . 12
      1
1       1 1    |
69 | | vex 2863 |
. . . . . . . . . . . . . . 15
 |
70 | 69 | pw1ex 4304 |
. . . . . . . . . . . . . 14
1  |
71 | | pw1eq 4144 |
. . . . . . . . . . . . . . 15
 1
1 1 1   |
72 | 71 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
 1

1 1 1    |
73 | 70, 72 | ceqsexv 2895 |
. . . . . . . . . . . . 13
    1
1  1 1   |
74 | 73 | exbii 1582 |
. . . . . . . . . . . 12
      1
1  
1 1   |
75 | 68, 74 | bitri 240 |
. . . . . . . . . . 11
      1
1  
1 1   |
76 | 57, 67, 75 | 3bitri 262 |
. . . . . . . . . 10
 1 1  1 1   |
77 | 55, 76 | sylib 188 |
. . . . . . . . 9
 1 1   
1 1   |
78 | | eleq1 2413 |
. . . . . . . . . . . . 13
 1 1

1 1    |
79 | 78 | biimpac 472 |
. . . . . . . . . . . 12
 
1 1  1 1
  |
80 | 32 | adantr 451 |
. . . . . . . . . . . . . . 15
    Fin Tfin
Spfin  Spfin Sfin   Tfin    1 1 
Nn  |
81 | | ncfinprop 4475 |
. . . . . . . . . . . . . . . . . . . 20
  Fin 1
 Ncfin 1 Nn 1
Ncfin 1    |
82 | 70, 81 | mpan2 652 |
. . . . . . . . . . . . . . . . . . 19
 Fin Ncfin 1 Nn 1 Ncfin 1    |
83 | 82 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . 18
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Ncfin 1 Nn 1
Ncfin 1    |
84 | 83 | simpld 445 |
. . . . . . . . . . . . . . . . 17
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Ncfin 1 Nn  |
85 | | tfincl 4493 |
. . . . . . . . . . . . . . . . 17
Ncfin 1 Nn Tfin Ncfin 1 Nn  |
86 | 84, 85 | syl 15 |
. . . . . . . . . . . . . . . 16
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin Ncfin 1 Nn  |
87 | 86 | adantr 451 |
. . . . . . . . . . . . . . 15
    Fin Tfin
Spfin  Spfin Sfin   Tfin    1 1  Tfin
Ncfin 1
Nn  |
88 | | simpr 447 |
. . . . . . . . . . . . . . 15
    Fin Tfin
Spfin  Spfin Sfin   Tfin    1 1  1 1   |
89 | | tfinpw1 4495 |
. . . . . . . . . . . . . . . . 17
 Ncfin
1 Nn 1 Ncfin 1  1 1 Tfin
Ncfin 1   |
90 | 83, 89 | syl 15 |
. . . . . . . . . . . . . . . 16
   Fin Tfin Spfin 
Spfin Sfin   Tfin    1 1 Tfin Ncfin 1   |
91 | 90 | adantr 451 |
. . . . . . . . . . . . . . 15
    Fin Tfin
Spfin  Spfin Sfin   Tfin    1 1  1 1 Tfin Ncfin 1   |
92 | | nnceleq 4431 |
. . . . . . . . . . . . . . 15
   Nn Tfin Ncfin 1 Nn  1 1
1 1 Tfin Ncfin 1  
Tfin Ncfin 1   |
93 | 80, 87, 88, 91, 92 | syl22anc 1183 |
. . . . . . . . . . . . . 14
    Fin Tfin
Spfin  Spfin Sfin   Tfin    1 1 
Tfin Ncfin 1   |
94 | 93 | ex 423 |
. . . . . . . . . . . . 13
   Fin Tfin Spfin 
Spfin Sfin   Tfin     1 1
Tfin Ncfin 1    |
95 | 5 | ad2ant2r 727 |
. . . . . . . . . . . . . . . . . . 19
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin   
Nn  |
96 | 69 | pwex 4330 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
97 | | ncfinprop 4475 |
. . . . . . . . . . . . . . . . . . . . . 22
  Fin  
Ncfin 
Nn  Ncfin
    |
98 | 96, 97 | mpan2 652 |
. . . . . . . . . . . . . . . . . . . . 21
 Fin Ncfin  Nn 
Ncfin     |
99 | 98 | simpld 445 |
. . . . . . . . . . . . . . . . . . . 20
 Fin Ncfin 
Nn  |
100 | 99 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . 19
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Ncfin 
Nn  |
101 | | simprr 733 |
. . . . . . . . . . . . . . . . . . . 20
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Sfin
Tfin Ncfin 1  Tfin    |
102 | 82 | simpld 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Fin Ncfin 1 Nn  |
103 | 82 | simprd 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 Fin 1 Ncfin 1   |
104 | 98 | simprd 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 Fin 
Ncfin    |
105 | | pw1eq 4144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 1 1   |
106 | 105 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  1 Ncfin 1 1
Ncfin 1    |
107 | | pweq 3726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
108 | 107 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
Ncfin 
 Ncfin     |
109 | 106, 108 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   1
Ncfin 1  Ncfin    1
Ncfin 1  Ncfin      |
110 | 69, 109 | spcev 2947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  1
Ncfin 1  Ncfin      1
Ncfin 1  Ncfin     |
111 | 103, 104,
110 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Fin    1 Ncfin
1 
Ncfin     |
112 | | df-sfin 4447 |
. . . . . . . . . . . . . . . . . . . . . . 23
Sfin Ncfin 1  Ncfin
  Ncfin 1 Nn Ncfin
 Nn    1 Ncfin
1 
Ncfin      |
113 | 102, 99, 111, 112 | syl3anbrc 1136 |
. . . . . . . . . . . . . . . . . . . . . 22
 Fin Sfin
Ncfin 1  Ncfin     |
114 | 113 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . 21
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Sfin
Ncfin 1  Ncfin     |
115 | | sfintfin 4533 |
. . . . . . . . . . . . . . . . . . . . 21
Sfin Ncfin 1  Ncfin
  Sfin Tfin Ncfin 1  Tfin Ncfin     |
116 | 114, 115 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Sfin
Tfin Ncfin 1  Tfin Ncfin     |
117 | | sfin112 4530 |
. . . . . . . . . . . . . . . . . . . 20
 Sfin
Tfin Ncfin 1  Tfin 
Sfin Tfin Ncfin 1  Tfin Ncfin    Tfin
Tfin Ncfin    |
118 | 101, 116,
117 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . 19
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Tfin
Tfin Ncfin    |
119 | | tfin11 4494 |
. . . . . . . . . . . . . . . . . . 19
  Nn Ncfin 
Nn Tfin Tfin
Ncfin   Ncfin    |
120 | 95, 100, 118, 119 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . 18
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin   
Ncfin    |
121 | | simprl 732 |
. . . . . . . . . . . . . . . . . 18
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin   
Spfin  |
122 | 120, 121 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . . 17
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Ncfin 
Spfin  |
123 | | spfinsfincl 4540 |
. . . . . . . . . . . . . . . . 17
 Ncfin
 Spfin Sfin Ncfin 1  Ncfin
  
Ncfin 1 Spfin  |
124 | 122, 114,
123 | syl2anc 642 |
. . . . . . . . . . . . . . . 16
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    Ncfin 1 Spfin  |
125 | | risset 2662 |
. . . . . . . . . . . . . . . . 17
Ncfin 1 Spfin 
Spfin
Ncfin 1   |
126 | | tfineq 4489 |
. . . . . . . . . . . . . . . . . . 19
 Ncfin 1 Tfin Tfin
Ncfin 1   |
127 | 126 | eqcomd 2358 |
. . . . . . . . . . . . . . . . . 18
 Ncfin 1 Tfin Ncfin 1 Tfin   |
128 | 127 | reximi 2722 |
. . . . . . . . . . . . . . . . 17
 
Spfin Ncfin 1  Spfin Tfin Ncfin 1 Tfin   |
129 | 125, 128 | sylbi 187 |
. . . . . . . . . . . . . . . 16
Ncfin 1 Spfin  Spfin Tfin Ncfin 1 Tfin   |
130 | 124, 129 | syl 15 |
. . . . . . . . . . . . . . 15
   Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin    
Spfin Tfin Ncfin 1 Tfin   |
131 | | sfineq1 4527 |
. . . . . . . . . . . . . . . . . 18
 Tfin Ncfin 1 Sfin   Tfin 
Sfin Tfin
Ncfin 1 
Tfin     |
132 | 131 | anbi2d 684 |
. . . . . . . . . . . . . . . . 17
 Tfin Ncfin 1   Spfin Sfin   Tfin  
 Spfin Sfin Tfin Ncfin 1  Tfin      |
133 | 132 | anbi2d 684 |
. . . . . . . . . . . . . . . 16
 Tfin Ncfin 1    Fin Tfin Spfin 
Spfin Sfin   Tfin      Fin Tfin Spfin 
Spfin Sfin Tfin Ncfin 1  Tfin       |
134 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . 17
 Tfin Ncfin 1  Tfin Tfin Ncfin 1 Tfin    |
135 | 134 | rexbidv 2636 |
. . . . . . . . . . . . . . . 16
 Tfin Ncfin 1  
Spfin Tfin 
Spfin Tfin Ncfin 1 Tfin    |
136 | 133, 135 | imbi12d 311 |
. . . . . . . . . . . . . . 15
 Tfin Ncfin 1     Fin Tfin
Spfin  Spfin Sfin   Tfin    
Spfin Tfin     Fin Tfin
Spfin  Spfin
Sfin Tfin Ncfin 1  Tfin    
Spfin Tfin Ncfin 1 Tfin     |
137 | 130, 136 | mpbiri 224 |
. . . . . . . . . . . . . 14
 Tfin Ncfin 1    Fin Tfin Spfin 
Spfin Sfin   Tfin    
Spfin Tfin    |
138 | 137 | com12 27 |
. . . . . . . . . . . . 13
   Fin Tfin Spfin 
Spfin Sfin   Tfin    
Tfin Ncfin 1  Spfin Tfin
   |
139 | 94, 138 | syld 40 |
. . . . . . . . . . . 12
   Fin Tfin Spfin 
Spfin Sfin   Tfin     1 1 
Spfin
Tfin    |
140 | 79, 139 | syl5 28 |
. . . . . . . . . . 11
   Fin Tfin Spfin 
Spfin Sfin   Tfin     
1 1   Spfin Tfin
   |
141 | 140 | expdimp 426 |
. . . . . . . . . 10
    Fin Tfin
Spfin  Spfin Sfin   Tfin     
1 1 
Spfin
Tfin    |
142 | 141 | exlimdv 1636 |
. . . . . . . . 9
    Fin Tfin
Spfin  Spfin Sfin   Tfin      
1 1  Spfin Tfin
   |
143 | 77, 142 | syl5 28 |
. . . . . . . 8
    Fin Tfin
Spfin  Spfin Sfin   Tfin      1 1
  
Spfin Tfin    |
144 | 143 | adantld 453 |
. . . . . . 7
    Fin Tfin
Spfin  Spfin Sfin   Tfin        
1 1   
 Spfin Tfin
   |
145 | 144 | adantrr 697 |
. . . . . 6
    Fin Tfin
Spfin  Spfin Sfin   Tfin    
     
1 1 
 
 Spfin Tfin
   |
146 | 145 | rexlimdvva 2746 |
. . . . 5
   Fin Tfin Spfin 
Spfin Sfin   Tfin     

  
1 1   
 Spfin Tfin
   |
147 | 52, 146 | syl5bi 208 |
. . . 4
   Fin Tfin Spfin 
Spfin Sfin   Tfin     1 1  
 Spfin Tfin
   |
148 | 51, 147 | syld 40 |
. . 3
   Fin Tfin Spfin 
Spfin Sfin   Tfin    Tfin Ncfin 1c 
  Spfin
Tfin    |
149 | 148 | rexlimdvw 2742 |
. 2
   Fin Tfin Spfin 
Spfin Sfin   Tfin     
Nn Tfin Ncfin 1c 
  Spfin
Tfin    |
150 | 43, 149 | mpd 14 |
1
   Fin Tfin Spfin 
Spfin Sfin   Tfin    
Spfin Tfin   |