Step | Hyp | Ref
| Expression |
1 | | df-spfin 4447 |
. . 3
Spfin ![|^|](bigcap.gif) ![{](lbrace.gif) Ncfin
![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
2 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
3 | 2 | elimak 4259 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) 1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | el1c 4139 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
5 | 4 | anbi1i 676 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | 19.41v 1901 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | bitr4i 243 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | df-rex 2620 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1c
![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | excom 1741 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 8, 9, 10 | 3bitr4i 268 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | snex 4111 |
. . . . . . . . . . . . . 14
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
13 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) ![)](rp.gif) |
14 | 13 | eleq1d 2419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 12, 14 | ceqsexv 2894 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | elin 3219 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
18 | 17, 2 | elssetk 4270 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![a](_a.gif) ![)](rp.gif) |
19 | | opkex 4113 |
. . . . . . . . . . . . . . . . 17
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![_V](rmcv.gif) |
20 | 19 | elimak 4259 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
21 | | df-rex 2620 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
23 | 22 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 23, 24 | bitr4i 243 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | exbii 1582 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 26, 27 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 20, 21, 28 | 3bitri 262 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | snex 4111 |
. . . . . . . . . . . . . . . . . 18
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
31 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
32 | 31 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 30, 32 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
34 | | eldif 3221 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins2k
Sk ![)](rp.gif) ![)](rp.gif) |
35 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
![{](lbrace.gif) ![z](_z.gif)
![_V](rmcv.gif) |
36 | 35, 12, 2 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins3k
SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . 20
![_V](rmcv.gif) |
38 | 37, 17 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 37, 17 | srelk 4524 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 36, 38, 39 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins3k
SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 35, 12, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins2k
Sk ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![)](rp.gif) |
42 | 37, 2 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![a](_a.gif) ![)](rp.gif) |
43 | 41, 42 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins2k
Sk ![a](_a.gif) ![)](rp.gif) |
44 | 43 | notbii 287 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins2k Sk ![a](_a.gif) ![)](rp.gif) |
45 | 40, 44 | anbi12i 678 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif) Ins2k
Sk Sfin ![(](lp.gif) ![z](_z.gif)
![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 33, 34, 45 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | exbii 1582 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
48 | | exanali 1585 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 29, 47, 48 | 3bitri 262 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![A.](forall.gif) ![z](_z.gif) Sfin
![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 18, 49 | anbi12i 678 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif)
![A.](forall.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 15, 16, 50 | 3bitri 262 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 51 | exbii 1582 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![A.](forall.gif) ![z](_z.gif) Sfin
![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 3, 11, 52 | 3bitri 262 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | df-rex 2620 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 55 | notbii 287 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 2 | elcompl 3225 |
. . . . . . . 8
![(](lp.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
58 | | dfral2 2626 |
. . . . . . . 8
![(](lp.gif) ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![E.](exists.gif) ![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 56, 57, 58 | 3bitr4i 268 |
. . . . . . 7
![(](lp.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | abbi2i 2464 |
. . . . . 6
∼ ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![{](lbrace.gif) ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) |
61 | 60 | ineq2i 3454 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ![{](lbrace.gif) ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
62 | | inab 3522 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ![{](lbrace.gif) ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif)
![{](lbrace.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
63 | 61, 62 | eqtri 2373 |
. . . 4
![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![{](lbrace.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
64 | 63 | inteqi 3930 |
. . 3
![|^|](bigcap.gif) ![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![|^|](bigcap.gif) ![{](lbrace.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![z](_z.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
65 | 1, 64 | eqtr4i 2376 |
. 2
Spfin ![|^|](bigcap.gif) ![(](lp.gif) ![{](lbrace.gif) Ncfin ![a](_a.gif) ∼
![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
66 | | setswithex 4322 |
. . . 4
![{](lbrace.gif) Ncfin ![a](_a.gif) ![_V](rmcv.gif) |
67 | | ssetkex 4294 |
. . . . . . 7
Sk ![_V](rmcv.gif) |
68 | | srelkex 4525 |
. . . . . . . . . . 11
![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
69 | 68 | sikex 4297 |
. . . . . . . . . 10
SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
70 | 69 | ins3kex 4308 |
. . . . . . . . 9
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
71 | 67 | ins2kex 4307 |
. . . . . . . . 9
Ins2k Sk ![_V](rmcv.gif) |
72 | 70, 71 | difex 4107 |
. . . . . . . 8
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk
![_V](rmcv.gif) |
73 | | 1cex 4142 |
. . . . . . . . . 10
1c
![_V](rmcv.gif) |
74 | 73 | pw1ex 4303 |
. . . . . . . . 9
1
1c
![_V](rmcv.gif) |
75 | 74 | pw1ex 4303 |
. . . . . . . 8
1 1
1c
![_V](rmcv.gif) |
76 | 72, 75 | imakex 4300 |
. . . . . . 7
![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
77 | 67, 76 | inex 4105 |
. . . . . 6
Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
78 | 77, 73 | imakex 4300 |
. . . . 5
![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![_V](rmcv.gif) |
79 | 78 | complex 4104 |
. . . 4
∼ ![(](lp.gif) Sk ![(](lp.gif) Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c ![_V](rmcv.gif) |
80 | 66, 79 | inex 4105 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![_V](rmcv.gif) |
81 | 80 | intex 4320 |
. 2
![|^|](bigcap.gif) ![(](lp.gif) ![{](lbrace.gif)
Ncfin ![a](_a.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif)
Ins3k SIk ![(](lp.gif) Nn k Nn ![(](lp.gif) 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 Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![_V](rmcv.gif) |
82 | 65, 81 | eqeltri 2423 |
1
Spfin ![_V](rmcv.gif) |