Description: Lemma for cycpmconjs . (Contributed by Thierry Arnoux, 14-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cycpmconjs.c | |
|
cycpmconjs.s | |
||
cycpmconjs.n | |
||
cycpmconjs.m | |
||
cycpmconjslem1.d | |
||
cycpmconjslem1.w | |
||
cycpmconjslem1.1 | |
||
cycpmconjslem1.2 | |
||
Assertion | cycpmconjslem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cycpmconjs.c | |
|
2 | cycpmconjs.s | |
|
3 | cycpmconjs.n | |
|
4 | cycpmconjs.m | |
|
5 | cycpmconjslem1.d | |
|
6 | cycpmconjslem1.w | |
|
7 | cycpmconjslem1.1 | |
|
8 | cycpmconjslem1.2 | |
|
9 | resco | |
|
10 | 9 | coeq1i | |
11 | ssid | |
|
12 | cores | |
|
13 | 11 12 | ax-mp | |
14 | coass | |
|
15 | 10 13 14 | 3eqtr3i | |
16 | 4 5 6 7 | tocycfvres1 | |
17 | 16 | coeq1d | |
18 | coass | |
|
19 | f1f1orn | |
|
20 | f1ococnv1 | |
|
21 | 7 19 20 | 3syl | |
22 | 21 | coeq2d | |
23 | coires1 | |
|
24 | 22 23 | eqtr2di | |
25 | 18 24 | eqtr4id | |
26 | 1zzd | |
|
27 | cshwfn | |
|
28 | 6 26 27 | syl2anc | |
29 | wrddm | |
|
30 | 6 29 | syl | |
31 | 30 | fneq2d | |
32 | 28 31 | mpbird | |
33 | fnresdm | |
|
34 | 32 33 | syl | |
35 | 17 25 34 | 3eqtrd | |
36 | 35 | coeq2d | |
37 | 15 36 | eqtrid | |
38 | wrdfn | |
|
39 | 6 38 | syl | |
40 | df-f | |
|
41 | 39 11 40 | sylanblrc | |
42 | iswrdi | |
|
43 | 41 42 | syl | |
44 | f1ocnv | |
|
45 | 7 19 44 | 3syl | |
46 | f1of | |
|
47 | 45 46 | syl | |
48 | cshco | |
|
49 | 43 26 47 48 | syl3anc | |
50 | 8 | oveq2d | |
51 | 30 50 | eqtrd | |
52 | 51 | reseq2d | |
53 | 21 52 | eqtrd | |
54 | 53 | oveq1d | |
55 | 37 49 54 | 3eqtrd | |