Step | Hyp | Ref
| Expression |
1 | | tncveqnc1fin 4544 |
. . . . . 6
![(](lp.gif) Fin Tfin
Ncfin Ncfin
1c![)](rp.gif) |
2 | | 1cspfin 4543 |
. . . . . 6
![(](lp.gif) Fin Ncfin 1c Spfin ![)](rp.gif) |
3 | 1, 2 | eqeltrd 2427 |
. . . . 5
![(](lp.gif) Fin Tfin
Ncfin Spfin ![)](rp.gif) |
4 | | ncfinex 4472 |
. . . . . 6
Ncfin ![_V](rmcv.gif) |
5 | | tfineq 4488 |
. . . . . . 7
![(](lp.gif) Ncfin Tfin Tfin
Ncfin ![_V](rmcv.gif) ![)](rp.gif) |
6 | 5 | eleq1d 2419 |
. . . . . 6
![(](lp.gif) Ncfin Tfin Spfin Tfin Ncfin Spfin ![)](rp.gif) ![)](rp.gif) |
7 | 4, 6 | elab 2985 |
. . . . 5
Ncfin ![{](lbrace.gif) Tfin
Spfin Tfin Ncfin Spfin ![)](rp.gif) |
8 | 3, 7 | sylibr 203 |
. . . 4
![(](lp.gif) Fin Ncfin ![{](lbrace.gif) Tfin
Spfin ![}](rbrace.gif) ![)](rp.gif) |
9 | | simprl 732 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Tfin
Spfin Sfin
![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) Tfin Spfin
![)](rp.gif) |
10 | | sfintfin 4532 |
. . . . . . . . . 10
Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) Sfin Tfin ![z](_z.gif)
Tfin ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | ad2antll 709 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Tfin
Spfin Sfin
![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![z](_z.gif)
Tfin ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | spfinsfincl 4539 |
. . . . . . . . 9
![(](lp.gif) Tfin
Spfin Sfin Tfin ![z](_z.gif)
Tfin ![y](_y.gif) ![)](rp.gif) Tfin
Spfin ![)](rp.gif) |
13 | 9, 11, 12 | syl2anc 642 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Tfin
Spfin Sfin
![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) Tfin Spfin
![)](rp.gif) |
14 | 13 | ex 423 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) Tfin
Spfin Sfin
![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
15 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
16 | | tfineq 4488 |
. . . . . . . . . 10
![(](lp.gif) Tfin
Tfin ![y](_y.gif) ![)](rp.gif) |
17 | 16 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) Tfin
Spfin Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
18 | 15, 17 | elab 2985 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Tfin Spfin
![)](rp.gif) |
19 | 18 | anbi1i 676 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin Spfin
Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) Tfin
Spfin Sfin
![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
21 | | tfineq 4488 |
. . . . . . . . 9
![(](lp.gif) Tfin
Tfin ![z](_z.gif) ![)](rp.gif) |
22 | 21 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) Tfin
Spfin Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
23 | 20, 22 | elab 2985 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Tfin Spfin
![)](rp.gif) |
24 | 14, 19, 23 | 3imtr4g 261 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | alrimiv 1631 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif)
Tfin Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | ralrimiva 2697 |
. . . 4
![(](lp.gif) Fin ![A.](forall.gif)
Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
28 | 27 | elimak 4259 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin ![E.](exists.gif) Spfin ![<<](llangle.gif) ![y](_y.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 15, 27 | opkelcnvk 4250 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
31 | 30, 15 | eqtfinrelk 4486 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) Tfin
![x](_x.gif) ![)](rp.gif) |
32 | 29, 31 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) Tfin
![x](_x.gif) ![)](rp.gif) |
33 | 32 | rexbii 2639 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Spfin ![<<](llangle.gif) ![y](_y.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) |
34 | 28, 33 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
35 | 30 | eluni1 4173 |
. . . . . . . 8
![(](lp.gif) ⋃1![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin ![)](rp.gif) ![)](rp.gif) |
36 | | risset 2661 |
. . . . . . . 8
Tfin
Spfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
37 | 34, 35, 36 | 3bitr4i 268 |
. . . . . . 7
![(](lp.gif) ⋃1![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin Tfin Spfin
![)](rp.gif) |
38 | 37 | abbi2i 2464 |
. . . . . 6
⋃1![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin
![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) |
39 | | tfinrelkex 4487 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
40 | 39 | cnvkex 4287 |
. . . . . . . 8
k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
41 | | spfinex 4537 |
. . . . . . . 8
Spfin ![_V](rmcv.gif) |
42 | 40, 41 | imakex 4300 |
. . . . . . 7
![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin
![_V](rmcv.gif) |
43 | 42 | uni1ex 4293 |
. . . . . 6
⋃1![(](lp.gif) k![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k Spfin
![_V](rmcv.gif) |
44 | 38, 43 | eqeltrri 2424 |
. . . . 5
![{](lbrace.gif) Tfin Spfin
![_V](rmcv.gif) |
45 | | spfininduct 4540 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Ncfin ![{](lbrace.gif) Tfin
Spfin ![A.](forall.gif) Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) Spfin ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) |
46 | 44, 45 | mp3an1 1264 |
. . . 4
![(](lp.gif) Ncfin
![{](lbrace.gif) Tfin
Spfin ![A.](forall.gif) Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) Spfin ![{](lbrace.gif) Tfin Spfin
![}](rbrace.gif) ![)](rp.gif) |
47 | 8, 26, 46 | syl2anc 642 |
. . 3
![(](lp.gif) Fin Spfin ![{](lbrace.gif)
Tfin
Spfin ![}](rbrace.gif) ![)](rp.gif) |
48 | 47 | sselda 3273 |
. 2
![(](lp.gif) ![(](lp.gif) Fin Spfin ![{](lbrace.gif)
Tfin Spfin ![}](rbrace.gif) ![)](rp.gif) |
49 | | tfineq 4488 |
. . . . 5
![(](lp.gif) Tfin
Tfin ![X](_cx.gif) ![)](rp.gif) |
50 | 49 | eleq1d 2419 |
. . . 4
![(](lp.gif) Tfin
Spfin Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
51 | 50 | elabg 2986 |
. . 3
![(](lp.gif) Spfin ![(](lp.gif)
![{](lbrace.gif) Tfin Spfin
Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
52 | 51 | adantl 452 |
. 2
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![{](lbrace.gif) Tfin
Spfin Tfin Spfin ![)](rp.gif) ![)](rp.gif) |
53 | 48, 52 | mpbid 201 |
1
![(](lp.gif) ![(](lp.gif) Fin Spfin Tfin Spfin ![)](rp.gif) |