Proof of Theorem nncex
Step | Hyp | Ref
| Expression |
1 | | dfnnc2 4395 |
. 2
Nn ![|^|](bigcap.gif) ![(](lp.gif) ![{](lbrace.gif)
0c
![x](_x.gif) ![(](lp.gif) Sk Sk k SIk 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![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
2 | | setswithex 4322 |
. . . 4
![{](lbrace.gif) 0c ![x](_x.gif) ![_V](rmcv.gif) |
3 | | ssetkex 4294 |
. . . . . 6
Sk ![_V](rmcv.gif) |
4 | | addcexlem 4382 |
. . . . . . . . . 10
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)
![_V](rmcv.gif) |
5 | | 1cex 4142 |
. . . . . . . . . . . 12
1c
![_V](rmcv.gif) |
6 | 5 | pw1ex 4303 |
. . . . . . . . . . 11
1
1c
![_V](rmcv.gif) |
7 | 6 | pw1ex 4303 |
. . . . . . . . . 10
1 1
1c
![_V](rmcv.gif) |
8 | 4, 7 | imakex 4300 |
. . . . . . . . 9
![(](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
![_V](rmcv.gif) |
9 | 8 | imagekex 4312 |
. . . . . . . 8
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
![_V](rmcv.gif) |
10 | 9 | sikex 4297 |
. . . . . . 7
SIk 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
![_V](rmcv.gif) |
11 | 3, 10 | cokex 4310 |
. . . . . 6
Sk k SIk 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![)](rp.gif)
![_V](rmcv.gif) |
12 | 3, 11 | difex 4107 |
. . . . 5
Sk Sk k SIk 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![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
13 | 12, 5 | imakex 4300 |
. . . 4
![(](lp.gif) Sk Sk k SIk 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![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k1c ![_V](rmcv.gif) |
14 | 2, 13 | difex 4107 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
0c
![x](_x.gif) ![(](lp.gif) Sk Sk k SIk 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![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![_V](rmcv.gif) |
15 | 14 | intex 4320 |
. 2
![|^|](bigcap.gif) ![(](lp.gif) ![{](lbrace.gif)
0c
![x](_x.gif) ![(](lp.gif) Sk Sk k SIk 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![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![_V](rmcv.gif) |
16 | 1, 15 | eqeltri 2423 |
1
Nn ![_V](rmcv.gif) |