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