Step | Hyp | Ref
| Expression |
1 | | cycpmconjvlem.f |
. . . 4
β’ (π β πΉ:π·β1-1-ontoβπ·) |
2 | | f1ofun 6787 |
. . . 4
β’ (πΉ:π·β1-1-ontoβπ· β Fun πΉ) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β Fun πΉ) |
4 | | funrel 6519 |
. . . . . . 7
β’ (Fun
πΉ β Rel πΉ) |
5 | | dfrel2 6142 |
. . . . . . 7
β’ (Rel
πΉ β β‘β‘πΉ = πΉ) |
6 | 4, 5 | sylib 217 |
. . . . . 6
β’ (Fun
πΉ β β‘β‘πΉ = πΉ) |
7 | 6 | reseq1d 5937 |
. . . . 5
β’ (Fun
πΉ β (β‘β‘πΉ βΎ (π· β π΅)) = (πΉ βΎ (π· β π΅))) |
8 | 7 | cnveqd 5832 |
. . . 4
β’ (Fun
πΉ β β‘(β‘β‘πΉ βΎ (π· β π΅)) = β‘(πΉ βΎ (π· β π΅))) |
9 | 8 | coeq2d 5819 |
. . 3
β’ (Fun
πΉ β ((πΉ βΎ (π· β π΅)) β β‘(β‘β‘πΉ βΎ (π· β π΅))) = ((πΉ βΎ (π· β π΅)) β β‘(πΉ βΎ (π· β π΅)))) |
10 | 3, 9 | syl 17 |
. 2
β’ (π β ((πΉ βΎ (π· β π΅)) β β‘(β‘β‘πΉ βΎ (π· β π΅))) = ((πΉ βΎ (π· β π΅)) β β‘(πΉ βΎ (π· β π΅)))) |
11 | | difssd 4093 |
. . . . . 6
β’ (π β (π· β π΅) β π·) |
12 | | f1odm 6789 |
. . . . . . 7
β’ (πΉ:π·β1-1-ontoβπ· β dom πΉ = π·) |
13 | 1, 12 | syl 17 |
. . . . . 6
β’ (π β dom πΉ = π·) |
14 | 11, 13 | sseqtrrd 3986 |
. . . . 5
β’ (π β (π· β π΅) β dom πΉ) |
15 | | ssdmres 5961 |
. . . . 5
β’ ((π· β π΅) β dom πΉ β dom (πΉ βΎ (π· β π΅)) = (π· β π΅)) |
16 | 14, 15 | sylib 217 |
. . . 4
β’ (π β dom (πΉ βΎ (π· β π΅)) = (π· β π΅)) |
17 | | ssidd 3968 |
. . . 4
β’ (π β (π· β π΅) β (π· β π΅)) |
18 | 16, 17 | eqsstrd 3983 |
. . 3
β’ (π β dom (πΉ βΎ (π· β π΅)) β (π· β π΅)) |
19 | | cores2 6212 |
. . 3
β’ (dom
(πΉ βΎ (π· β π΅)) β (π· β π΅) β ((πΉ βΎ (π· β π΅)) β β‘(β‘β‘πΉ βΎ (π· β π΅))) = ((πΉ βΎ (π· β π΅)) β β‘πΉ)) |
20 | 18, 19 | syl 17 |
. 2
β’ (π β ((πΉ βΎ (π· β π΅)) β β‘(β‘β‘πΉ βΎ (π· β π΅))) = ((πΉ βΎ (π· β π΅)) β β‘πΉ)) |
21 | | f1ocnv 6797 |
. . . . . 6
β’ (πΉ:π·β1-1-ontoβπ· β β‘πΉ:π·β1-1-ontoβπ·) |
22 | | f1ofun 6787 |
. . . . . 6
β’ (β‘πΉ:π·β1-1-ontoβπ· β Fun β‘πΉ) |
23 | 1, 21, 22 | 3syl 18 |
. . . . 5
β’ (π β Fun β‘πΉ) |
24 | | ssidd 3968 |
. . . . . . . 8
β’ (π β π· β π·) |
25 | 24, 13 | sseqtrrd 3986 |
. . . . . . 7
β’ (π β π· β dom πΉ) |
26 | | fores 6767 |
. . . . . . 7
β’ ((Fun
πΉ β§ π· β dom πΉ) β (πΉ βΎ π·):π·βontoβ(πΉ β π·)) |
27 | 3, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ βΎ π·):π·βontoβ(πΉ β π·)) |
28 | | df-ima 5647 |
. . . . . . 7
β’ (πΉ β π·) = ran (πΉ βΎ π·) |
29 | | foeq3 6755 |
. . . . . . 7
β’ ((πΉ β π·) = ran (πΉ βΎ π·) β ((πΉ βΎ π·):π·βontoβ(πΉ β π·) β (πΉ βΎ π·):π·βontoβran (πΉ βΎ π·))) |
30 | 28, 29 | ax-mp 5 |
. . . . . 6
β’ ((πΉ βΎ π·):π·βontoβ(πΉ β π·) β (πΉ βΎ π·):π·βontoβran (πΉ βΎ π·)) |
31 | 27, 30 | sylib 217 |
. . . . 5
β’ (π β (πΉ βΎ π·):π·βontoβran (πΉ βΎ π·)) |
32 | | cycpmconjvlem.b |
. . . . . . . 8
β’ (π β π΅ β π·) |
33 | 32, 13 | sseqtrrd 3986 |
. . . . . . 7
β’ (π β π΅ β dom πΉ) |
34 | | fores 6767 |
. . . . . . 7
β’ ((Fun
πΉ β§ π΅ β dom πΉ) β (πΉ βΎ π΅):π΅βontoβ(πΉ β π΅)) |
35 | 3, 33, 34 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ βΎ π΅):π΅βontoβ(πΉ β π΅)) |
36 | | df-ima 5647 |
. . . . . . 7
β’ (πΉ β π΅) = ran (πΉ βΎ π΅) |
37 | | foeq3 6755 |
. . . . . . 7
β’ ((πΉ β π΅) = ran (πΉ βΎ π΅) β ((πΉ βΎ π΅):π΅βontoβ(πΉ β π΅) β (πΉ βΎ π΅):π΅βontoβran (πΉ βΎ π΅))) |
38 | 36, 37 | ax-mp 5 |
. . . . . 6
β’ ((πΉ βΎ π΅):π΅βontoβ(πΉ β π΅) β (πΉ βΎ π΅):π΅βontoβran (πΉ βΎ π΅)) |
39 | 35, 38 | sylib 217 |
. . . . 5
β’ (π β (πΉ βΎ π΅):π΅βontoβran (πΉ βΎ π΅)) |
40 | | resdif 6806 |
. . . . 5
β’ ((Fun
β‘πΉ β§ (πΉ βΎ π·):π·βontoβran (πΉ βΎ π·) β§ (πΉ βΎ π΅):π΅βontoβran (πΉ βΎ π΅)) β (πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(ran
(πΉ βΎ π·) β ran (πΉ βΎ π΅))) |
41 | 23, 31, 39, 40 | syl3anc 1372 |
. . . 4
β’ (π β (πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(ran
(πΉ βΎ π·) β ran (πΉ βΎ π΅))) |
42 | | f1ofn 6786 |
. . . . . . . . 9
β’ (πΉ:π·β1-1-ontoβπ· β πΉ Fn π·) |
43 | | fnresdm 6621 |
. . . . . . . . 9
β’ (πΉ Fn π· β (πΉ βΎ π·) = πΉ) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . . 8
β’ (π β (πΉ βΎ π·) = πΉ) |
45 | 44 | rneqd 5894 |
. . . . . . 7
β’ (π β ran (πΉ βΎ π·) = ran πΉ) |
46 | | f1ofo 6792 |
. . . . . . . 8
β’ (πΉ:π·β1-1-ontoβπ· β πΉ:π·βontoβπ·) |
47 | | forn 6760 |
. . . . . . . 8
β’ (πΉ:π·βontoβπ· β ran πΉ = π·) |
48 | 1, 46, 47 | 3syl 18 |
. . . . . . 7
β’ (π β ran πΉ = π·) |
49 | 45, 48 | eqtrd 2773 |
. . . . . 6
β’ (π β ran (πΉ βΎ π·) = π·) |
50 | 49 | difeq1d 4082 |
. . . . 5
β’ (π β (ran (πΉ βΎ π·) β ran (πΉ βΎ π΅)) = (π· β ran (πΉ βΎ π΅))) |
51 | 50 | f1oeq3d 6782 |
. . . 4
β’ (π β ((πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(ran
(πΉ βΎ π·) β ran (πΉ βΎ π΅)) β (πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(π· β ran (πΉ βΎ π΅)))) |
52 | 41, 51 | mpbid 231 |
. . 3
β’ (π β (πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(π· β ran (πΉ βΎ π΅))) |
53 | | f1ococnv2 6812 |
. . 3
β’ ((πΉ βΎ (π· β π΅)):(π· β π΅)β1-1-ontoβ(π· β ran (πΉ βΎ π΅)) β ((πΉ βΎ (π· β π΅)) β β‘(πΉ βΎ (π· β π΅))) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) |
54 | 52, 53 | syl 17 |
. 2
β’ (π β ((πΉ βΎ (π· β π΅)) β β‘(πΉ βΎ (π· β π΅))) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) |
55 | 10, 20, 54 | 3eqtr3d 2781 |
1
β’ (π β ((πΉ βΎ (π· β π΅)) β β‘πΉ) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) |