Proof of Theorem ssetex
Step | Hyp | Ref
| Expression |
1 | | dfsset2 4743 |
. 2
S ⋃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 Sk
![)](rp.gif) |
2 | | vvex 4109 |
. . . . . . . 8
![_V](rmcv.gif) |
3 | 2, 2 | xpkex 4289 |
. . . . . . 7
![(](lp.gif) k ![_V](rmcv.gif)
![_V](rmcv.gif) |
4 | 3, 2 | xpkex 4289 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif)
k
![_V](rmcv.gif) ![_V](rmcv.gif) |
5 | | setconslem5 4735 |
. . . . . . 7
∼ ![(](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
![_V](rmcv.gif) |
6 | 5 | cnvkex 4287 |
. . . . . 6
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
![_V](rmcv.gif) |
7 | 4, 6 | inex 4105 |
. . . . 5
![(](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)
![_V](rmcv.gif) |
8 | | ssetkex 4294 |
. . . . 5
Sk ![_V](rmcv.gif) |
9 | 7, 8 | imakex 4300 |
. . . 4
![(](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 Sk
![_V](rmcv.gif) |
10 | 9 | uni1ex 4293 |
. . 3
⋃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 Sk
![_V](rmcv.gif) |
11 | 10 | uni1ex 4293 |
. 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 Sk
![_V](rmcv.gif) |
12 | 1, 11 | eqeltri 2423 |
1
S ![_V](rmcv.gif) |