Proof of Theorem dfop2lem2
Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . 4
![_V](rmcv.gif) |
2 | 1 | elimak 4259 |
. . 3
![(](lp.gif) ∼ ![(](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) k![B](_cb.gif) ![E.](exists.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ∼ ![(](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) |
3 | | dfop2lem1 4573 |
. . . 4
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ ![(](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 Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | rexbii 2639 |
. . 3
![(](lp.gif) ![E.](exists.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
∼ ![(](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 ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 4 | bitri 240 |
. 2
![(](lp.gif) ∼ ![(](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) k![B](_cb.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 5 | abbi2i 2464 |
1
∼ ![(](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) k![B](_cb.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) |