Step | Hyp | Ref
| Expression |
1 | | df-sn 3741 |
. . . . . 6
0c ![{](lbrace.gif)
0c![}](rbrace.gif) |
2 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
3 | 2 | elimak 4259 |
. . . . . . . 8
![(](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![)](rp.gif) k Nn ![E.](exists.gif)
Nn ![<<](llangle.gif) ![x](_x.gif) ![n](_n.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![)](rp.gif) ![)](rp.gif) |
4 | | vex 2862 |
. . . . . . . . . . 11
![_V](rmcv.gif) |
5 | | opkelimagekg 4271 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
![_V](rmcv.gif) ![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![n](_n.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 ![(](lp.gif) ![(](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) k![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 4, 2, 5 | mp2an 653 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![n](_n.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 ![(](lp.gif) ![(](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) k![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | dfaddc2 4381 |
. . . . . . . . . . 11
![(](lp.gif) 1c
![(](lp.gif) ![(](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) k![x](_x.gif) ![)](rp.gif) |
8 | 7 | eqeq2i 2363 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](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) k![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 6, 8 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![n](_n.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 ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
10 | 9 | rexbii 2639 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif)
Nn ![<<](llangle.gif) ![x](_x.gif) ![n](_n.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 ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
11 | 3, 10 | bitri 240 |
. . . . . . 7
![(](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![)](rp.gif) k Nn ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
12 | 11 | abbi2i 2464 |
. . . . . 6
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) k Nn ![{](lbrace.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![}](rbrace.gif) |
13 | 1, 12 | uneq12i 3416 |
. . . . 5
![(](lp.gif) 0c 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) k Nn ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif)
0c ![{](lbrace.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
14 | | unab 3521 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif)
0c ![{](lbrace.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![{](lbrace.gif)
![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
15 | 13, 14 | eqtri 2373 |
. . . 4
![(](lp.gif) 0c 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) k Nn ![)](rp.gif)
![{](lbrace.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
16 | | snex 4111 |
. . . . 5
0c ![_V](rmcv.gif) |
17 | | addcexlem 4382 |
. . . . . . . 8
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) |
18 | | 1cex 4142 |
. . . . . . . . . 10
1c
![_V](rmcv.gif) |
19 | 18 | pw1ex 4303 |
. . . . . . . . 9
1
1c
![_V](rmcv.gif) |
20 | 19 | pw1ex 4303 |
. . . . . . . 8
1 1
1c
![_V](rmcv.gif) |
21 | 17, 20 | imakex 4300 |
. . . . . . 7
![(](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) |
22 | 21 | imagekex 4312 |
. . . . . 6
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) |
23 | | nncex 4396 |
. . . . . 6
Nn ![_V](rmcv.gif) |
24 | 22, 23 | imakex 4300 |
. . . . 5
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) k Nn ![_V](rmcv.gif) |
25 | 16, 24 | unex 4106 |
. . . 4
![(](lp.gif) 0c 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) k Nn ![)](rp.gif)
![_V](rmcv.gif) |
26 | 15, 25 | eqeltrri 2424 |
. . 3
![{](lbrace.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
27 | | eqeq1 2359 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) 0c
0c
0c![)](rp.gif) ![)](rp.gif) |
28 | | eqeq1 2359 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif)
1c
0c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | rexbidv 2635 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![E.](exists.gif) Nn 0c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 27, 29 | orbi12d 690 |
. . 3
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
0c
0c
![E.](exists.gif) Nn 0c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
32 | | eqeq1 2359 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | rexbidv 2635 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 31, 33 | orbi12d 690 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
0c
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 0c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 0c ![(](lp.gif) 1c
0c![)](rp.gif) ![)](rp.gif) |
36 | | eqeq1 2359 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | rexbidv 2635 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 35, 37 | orbi12d 690 |
. . 3
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) 1c
0c ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
40 | | eqeq1 2359 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | rexbidv 2635 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 39, 41 | orbi12d 690 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
0c
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 0c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | eqid 2353 |
. . . 4
0c
0c |
44 | 43 | orci 379 |
. . 3
0c 0c ![E.](exists.gif)
Nn 0c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
45 | | eqid 2353 |
. . . . . 6
![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) |
46 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 46 | eqeq2d 2364 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | rspcev 2955 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
49 | 45, 48 | mpan2 652 |
. . . . 5
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
50 | 49 | olcd 382 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c 0c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | a1d 22 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
1c
0c
![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 26, 30, 34, 38, 42, 44, 51 | finds 4411 |
. 2
![(](lp.gif) Nn ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | peano1 4402 |
. . . 4
0c
Nn |
54 | | eleq1 2413 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) Nn 0c Nn ![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | mpbiri 224 |
. . 3
![(](lp.gif) 0c Nn ![)](rp.gif) |
56 | | peano2 4403 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
57 | | eleq1 2413 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) |
58 | 56, 57 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) |
59 | 58 | rexlimiv 2732 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c Nn ![)](rp.gif) |
60 | 55, 59 | jaoi 368 |
. 2
![(](lp.gif) ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) Nn ![)](rp.gif) |
61 | 52, 60 | impbii 180 |
1
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |