Step | Hyp | Ref
| Expression |
1 | | snex 4111 |
. . . . . . . 8
![{](lbrace.gif) ![A](_ca.gif)
![_V](rmcv.gif) |
2 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
3 | | opkelsikg 4264 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![_V](rmcv.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif)
![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif)
![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 2, 3 | mp2an 653 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif)
![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | excom 1741 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif)
![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | 3anass 938 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif)
![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | eqcom 2355 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![)](rp.gif) |
8 | | vex 2862 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
9 | 8 | sneqb 3876 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![A](_ca.gif) ![A](_ca.gif) ![)](rp.gif) |
10 | 7, 9 | bitri 240 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![A](_ca.gif) ![)](rp.gif) |
11 | 10 | anbi1i 676 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 6, 11 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif)
![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | exbii 1582 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | setconslem1.1 |
. . . . . . . . . 10
![_V](rmcv.gif) |
15 | | opkeq1 4059 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) ![>>](rrangle.gif) ![)](rp.gif) |
16 | 15 | eleq1d 2419 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | anbi2d 684 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 14, 17 | ceqsexv 2894 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 13, 18 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![z](_z.gif) ![x](_x.gif)
kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 4, 5, 20 | 3bitri 262 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | anbi1i 676 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) |
23 | | 19.41v 1901 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) |
24 | | anass 630 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 22, 23, 25 | 3bitr2i 264 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | exbii 1582 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif)
SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | | excom 1741 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | snex 4111 |
. . . . . 6
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
30 | | opkeq1 4059 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) ![>>](rrangle.gif) ![)](rp.gif) |
31 | 30 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![B](_cb.gif) Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) |
32 | 31 | anbi2d 684 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 29, 32 | ceqsexv 2894 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) |
34 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
35 | 34, 14 | opkelimagek 4272 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![A](_ca.gif)
Imagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 14, 34 | opkelcnvk 4250 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![x](_x.gif) ![A](_ca.gif)
Imagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | dfphi2 4569 |
. . . . . . . 8
Phi ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![x](_x.gif) ![)](rp.gif) |
38 | 37 | eqeq2i 2363 |
. . . . . . 7
![(](lp.gif) Phi ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 35, 36, 38 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) Phi ![x](_x.gif) ![)](rp.gif) |
40 | | setconslem1.2 |
. . . . . . 7
![_V](rmcv.gif) |
41 | 34, 40 | elssetk 4270 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![B](_cb.gif) ![)](rp.gif) |
42 | 39, 41 | anbi12i 678 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![(](lp.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | ancom 437 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Phi ![B](_cb.gif) ![(](lp.gif) Phi ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 33, 42, 43 | 3bitri 262 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif)
![(](lp.gif) Phi ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | exbii 1582 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![x](_x.gif) kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
Phi ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 27, 28, 45 | 3bitr2i 264 |
. 2
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif)
SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) Phi ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 1, 40 | opkelcok 4262 |
. 2
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk k SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![t](_t.gif) SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![t](_t.gif)
![B](_cb.gif) Sk ![)](rp.gif) ![)](rp.gif) |
48 | | df-rex 2620 |
. 2
![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) Phi ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 46, 47, 48 | 3bitr4i 268 |
1
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk k SIk kImagek![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Phi ![x](_x.gif) ![)](rp.gif) |