Step | Hyp | Ref
| Expression |
1 | | eleq1 2413 |
. . . . . . . . . . . . 13
0c 0c |
2 | 1 | biimpcd 215 |
. . . . . . . . . . . 12
0c 0c |
3 | 2 | con3d 125 |
. . . . . . . . . . 11
0c 0c |
4 | 3 | impcom 419 |
. . . . . . . . . 10
0c
0c |
5 | 4 | adantll 694 |
. . . . . . . . 9
Nn
0c
0c |
6 | | ssel2 3268 |
. . . . . . . . . . 11
Nn
Nn |
7 | 6 | adantlr 695 |
. . . . . . . . . 10
Nn
0c
Nn |
8 | | nnc0suc 4412 |
. . . . . . . . . 10
Nn
0c Nn
1c |
9 | 7, 8 | sylib 188 |
. . . . . . . . 9
Nn
0c
0c
Nn 1c |
10 | | orel1 371 |
. . . . . . . . 9
0c 0c Nn 1c
Nn 1c |
11 | 5, 9, 10 | sylc 56 |
. . . . . . . 8
Nn
0c
Nn
1c |
12 | | anidm 625 |
. . . . . . . . . 10
1c
1c
1c |
13 | | eqeq1 2359 |
. . . . . . . . . . 11
1c 1c |
14 | 13 | anbi2d 684 |
. . . . . . . . . 10
1c
1c 1c
1c |
15 | 12, 14 | syl5bbr 250 |
. . . . . . . . 9
1c
1c
1c |
16 | 15 | rexbidv 2635 |
. . . . . . . 8
Nn 1c Nn
1c
1c |
17 | 11, 16 | syl5ibcom 211 |
. . . . . . 7
Nn
0c
Nn 1c
1c |
18 | | eqtr3 2372 |
. . . . . . . 8
1c
1c |
19 | 18 | rexlimivw 2734 |
. . . . . . 7
Nn
1c
1c |
20 | 17, 19 | impbid1 194 |
. . . . . 6
Nn
0c
Nn 1c
1c |
21 | 20 | rexbidva 2631 |
. . . . 5
Nn 0c
Nn 1c
1c |
22 | | risset 2661 |
. . . . 5
|
23 | | rexcom 2772 |
. . . . 5
Nn
1c
1c Nn 1c
1c |
24 | 21, 22, 23 | 3bitr4g 279 |
. . . 4
Nn 0c
Nn
1c
1c |
25 | 24 | abbi2dv 2468 |
. . 3
Nn 0c
Nn
1c
1c |
26 | | df-phi 4565 |
. . . 4
Phi Nn
1c
Nn
1c Nn 1c |
27 | | addceq1 4383 |
. . . . . . . . 9
1c 1c |
28 | 27 | eqeq2d 2364 |
. . . . . . . 8
1c 1c |
29 | 28 | rexbidv 2635 |
. . . . . . 7
1c
1c |
30 | 29 | rexrab 3000 |
. . . . . 6
Nn
1c
Nn 1c Nn
1c
Nn 1c |
31 | | iftrue 3668 |
. . . . . . . . . 10
Nn Nn 1c 1c |
32 | 31 | eqeq2d 2364 |
. . . . . . . . 9
Nn
Nn 1c
1c |
33 | 32 | anbi2d 684 |
. . . . . . . 8
Nn
1c
Nn 1c
1c
1c |
34 | | r19.41v 2764 |
. . . . . . . 8
1c
1c
1c
1c |
35 | 33, 34 | syl6bbr 254 |
. . . . . . 7
Nn
1c
Nn 1c
1c
1c |
36 | 35 | rexbiia 2647 |
. . . . . 6
Nn
1c
Nn 1c Nn
1c
1c |
37 | 30, 36 | bitri 240 |
. . . . 5
Nn
1c
Nn 1c Nn
1c
1c |
38 | 37 | abbii 2465 |
. . . 4
Nn
1c Nn 1c Nn
1c
1c |
39 | 26, 38 | eqtri 2373 |
. . 3
Phi Nn
1c
Nn
1c
1c |
40 | 25, 39 | syl6eqr 2403 |
. 2
Nn 0c
Phi
Nn
1c |
41 | | dfrab2 3530 |
. . . 4
Nn
1c
1c Nn |
42 | | vex 2862 |
. . . . . . . . 9
|
43 | 42 | elimak 4259 |
. . . . . . . 8
kImagek 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 kImagek 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 |
44 | | vex 2862 |
. . . . . . . . . . 11
|
45 | 42, 44 | opkelimagek 4272 |
. . . . . . . . . 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 |
46 | 44, 42 | opkelcnvk 4250 |
. . . . . . . . . 10
kImagek 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 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 |
47 | | 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 |
48 | 47 | 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 |
49 | 45, 46, 48 | 3bitr4i 268 |
. . . . . . . . 9
kImagek 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 |
50 | 49 | rexbii 2639 |
. . . . . . . 8
kImagek 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 |
51 | 43, 50 | bitri 240 |
. . . . . . 7
kImagek 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
1c |
52 | 51 | abbi2i 2464 |
. . . . . 6
kImagek 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
1c |
53 | | addcexlem 4382 |
. . . . . . . . . 10
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
|
54 | | 1cex 4142 |
. . . . . . . . . . . 12
1c
|
55 | 54 | pw1ex 4303 |
. . . . . . . . . . 11
1
1c
|
56 | 55 | pw1ex 4303 |
. . . . . . . . . 10
1 1
1c
|
57 | 53, 56 | imakex 4300 |
. . . . . . . . 9
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
|
58 | 57 | imagekex 4312 |
. . . . . . . 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 1c
|
59 | 58 | cnvkex 4287 |
. . . . . . 7
kImagek 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
|
60 | | phiall.1 |
. . . . . . 7
|
61 | 59, 60 | imakex 4300 |
. . . . . 6
kImagek 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 |
62 | 52, 61 | eqeltrri 2424 |
. . . . 5
1c |
63 | | nncex 4396 |
. . . . 5
Nn |
64 | 62, 63 | inex 4105 |
. . . 4
1c Nn |
65 | 41, 64 | eqeltri 2423 |
. . 3
Nn
1c |
66 | | phieq 4570 |
. . . 4
Nn
1c
Phi Phi
Nn
1c |
67 | 66 | eqeq2d 2364 |
. . 3
Nn
1c
Phi Phi Nn
1c |
68 | 65, 67 | spcev 2946 |
. 2
Phi Nn
1c
Phi |
69 | 40, 68 | syl 15 |
1
Nn 0c
Phi |