Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . 5
![_V](rmcv.gif) |
2 | | vex 2862 |
. . . . 5
![_V](rmcv.gif) |
3 | 1, 2 | opkelcok 4262 |
. . . 4
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | setconslem6 4736 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![{](lbrace.gif)
![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![<<](llangle.gif) ![a](_a.gif) ![b](_b.gif) ![<.](langle.gif) ![a](_a.gif) ![b](_b.gif) ![B](_cb.gif) ![)](rp.gif) ![}](rbrace.gif) |
5 | | opeq1 4578 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![a](_a.gif)
![b](_b.gif) ![<.](langle.gif) ![x](_x.gif) ![b](_b.gif) ![>.](rangle.gif) ![)](rp.gif) |
6 | 5 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![a](_a.gif) ![b](_b.gif) ![<.](langle.gif) ![x](_x.gif) ![b](_b.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | opeq2 4579 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![x](_x.gif)
![b](_b.gif) ![<.](langle.gif) ![x](_x.gif) ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
8 | 7 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![b](_b.gif) ![<.](langle.gif) ![x](_x.gif) ![z](_z.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
10 | 4, 6, 8, 1, 9 | opkelopkab 4246 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![<.](langle.gif) ![x](_x.gif) ![z](_z.gif) ![B](_cb.gif) ![)](rp.gif) |
11 | | df-br 4640 |
. . . . . . 7
![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![<.](langle.gif) ![x](_x.gif) ![z](_z.gif) ![B](_cb.gif) ![)](rp.gif) |
12 | 10, 11 | bitr4i 243 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![)](rp.gif) |
13 | | setconslem6 4736 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![{](lbrace.gif)
![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![<<](llangle.gif) ![a](_a.gif) ![b](_b.gif) ![<.](langle.gif) ![a](_a.gif) ![b](_b.gif) ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) |
14 | | opeq1 4578 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![a](_a.gif)
![b](_b.gif) ![<.](langle.gif) ![z](_z.gif) ![b](_b.gif) ![>.](rangle.gif) ![)](rp.gif) |
15 | 14 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![a](_a.gif) ![b](_b.gif) ![<.](langle.gif) ![z](_z.gif) ![b](_b.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | opeq2 4579 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![b](_b.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
17 | 16 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![b](_b.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 13, 15, 17, 9, 2 | opkelopkab 4246 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) |
19 | | df-br 4640 |
. . . . . . 7
![(](lp.gif) ![z](_z.gif) ![A](_ca.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) |
20 | 18, 19 | bitr4i 243 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) |
21 | 12, 20 | anbi12i 678 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | exbii 1582 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 3, 22 | bitri 240 |
. . 3
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | opabbii 4626 |
. 2
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![<<](llangle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
25 | | setconslem4 4734 |
. 2
⋃1⋃1![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif)
k
![_V](rmcv.gif) k ∼ ![(](lp.gif)
Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![<<](llangle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
26 | | df-co 4726 |
. 2
![(](lp.gif) ![B](_cb.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![x](_x.gif) ![B](_cb.gif) ![z](_z.gif) ![A](_ca.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
27 | 24, 25, 26 | 3eqtr4ri 2384 |
1
![(](lp.gif) ![B](_cb.gif) ⋃1⋃1![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) k ![_V](rmcv.gif)
k
∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![A](_ca.gif) k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ∼ ![(](lp.gif) Ins3k SIk SIk Sk Ins2k Ins3k 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) Ins2k ![(](lp.gif) Ins2k Sk Ins3k SIk ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |