Metamath Proof Explorer

Theorem cycpmconjvlem

Description: Lemma for cycpmconjv . (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Hypotheses cycpmconjvlem.f 
|- ( ph -> F : D -1-1-onto-> D )
cycpmconjvlem.b 
|- ( ph -> B C_ D )
Assertion cycpmconjvlem 
|- ( ph -> ( ( F |` ( D \ B ) ) o. `' F ) = ( _I |` ( D \ ran ( F |` B ) ) ) )

Proof

Step Hyp Ref Expression
1 cycpmconjvlem.f 
 |-  ( ph -> F : D -1-1-onto-> D )
2 cycpmconjvlem.b 
 |-  ( ph -> B C_ D )
3 f1ofun 
 |-  ( F : D -1-1-onto-> D -> Fun F )
4 1 3 syl 
 |-  ( ph -> Fun F )
5 funrel 
 |-  ( Fun F -> Rel F )
6 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
7 5 6 sylib 
 |-  ( Fun F -> `' `' F = F )
8 7 reseq1d 
 |-  ( Fun F -> ( `' `' F |` ( D \ B ) ) = ( F |` ( D \ B ) ) )
9 8 cnveqd 
 |-  ( Fun F -> `' ( `' `' F |` ( D \ B ) ) = `' ( F |` ( D \ B ) ) )
10 9 coeq2d 
 |-  ( Fun F -> ( ( F |` ( D \ B ) ) o. `' ( `' `' F |` ( D \ B ) ) ) = ( ( F |` ( D \ B ) ) o. `' ( F |` ( D \ B ) ) ) )
11 4 10 syl 
 |-  ( ph -> ( ( F |` ( D \ B ) ) o. `' ( `' `' F |` ( D \ B ) ) ) = ( ( F |` ( D \ B ) ) o. `' ( F |` ( D \ B ) ) ) )
12 difssd 
 |-  ( ph -> ( D \ B ) C_ D )
13 f1odm 
 |-  ( F : D -1-1-onto-> D -> dom F = D )
14 1 13 syl 
 |-  ( ph -> dom F = D )
15 12 14 sseqtrrd 
 |-  ( ph -> ( D \ B ) C_ dom F )
16 ssdmres 
 |-  ( ( D \ B ) C_ dom F <-> dom ( F |` ( D \ B ) ) = ( D \ B ) )
17 15 16 sylib 
 |-  ( ph -> dom ( F |` ( D \ B ) ) = ( D \ B ) )
18 ssidd 
 |-  ( ph -> ( D \ B ) C_ ( D \ B ) )
19 17 18 eqsstrd 
 |-  ( ph -> dom ( F |` ( D \ B ) ) C_ ( D \ B ) )
20 cores2 
 |-  ( dom ( F |` ( D \ B ) ) C_ ( D \ B ) -> ( ( F |` ( D \ B ) ) o. `' ( `' `' F |` ( D \ B ) ) ) = ( ( F |` ( D \ B ) ) o. `' F ) )
21 19 20 syl 
 |-  ( ph -> ( ( F |` ( D \ B ) ) o. `' ( `' `' F |` ( D \ B ) ) ) = ( ( F |` ( D \ B ) ) o. `' F ) )
22 f1ocnv 
 |-  ( F : D -1-1-onto-> D -> `' F : D -1-1-onto-> D )
23 f1ofun 
 |-  ( `' F : D -1-1-onto-> D -> Fun `' F )
24 1 22 23 3syl 
 |-  ( ph -> Fun `' F )
25 ssidd 
 |-  ( ph -> D C_ D )
26 25 14 sseqtrrd 
 |-  ( ph -> D C_ dom F )
27 fores 
 |-  ( ( Fun F /\ D C_ dom F ) -> ( F |` D ) : D -onto-> ( F " D ) )
28 4 26 27 syl2anc 
 |-  ( ph -> ( F |` D ) : D -onto-> ( F " D ) )
29 df-ima 
 |-  ( F " D ) = ran ( F |` D )
30 foeq3 
 |-  ( ( F " D ) = ran ( F |` D ) -> ( ( F |` D ) : D -onto-> ( F " D ) <-> ( F |` D ) : D -onto-> ran ( F |` D ) ) )
31 29 30 ax-mp 
 |-  ( ( F |` D ) : D -onto-> ( F " D ) <-> ( F |` D ) : D -onto-> ran ( F |` D ) )
32 28 31 sylib 
 |-  ( ph -> ( F |` D ) : D -onto-> ran ( F |` D ) )
33 2 14 sseqtrrd 
 |-  ( ph -> B C_ dom F )
34 fores 
 |-  ( ( Fun F /\ B C_ dom F ) -> ( F |` B ) : B -onto-> ( F " B ) )
35 4 33 34 syl2anc 
 |-  ( ph -> ( F |` B ) : B -onto-> ( F " B ) )
36 df-ima 
 |-  ( F " B ) = ran ( F |` B )
37 foeq3 
 |-  ( ( F " B ) = ran ( F |` B ) -> ( ( F |` B ) : B -onto-> ( F " B ) <-> ( F |` B ) : B -onto-> ran ( F |` B ) ) )
38 36 37 ax-mp 
 |-  ( ( F |` B ) : B -onto-> ( F " B ) <-> ( F |` B ) : B -onto-> ran ( F |` B ) )
39 35 38 sylib 
 |-  ( ph -> ( F |` B ) : B -onto-> ran ( F |` B ) )
40 resdif 
 |-  ( ( Fun `' F /\ ( F |` D ) : D -onto-> ran ( F |` D ) /\ ( F |` B ) : B -onto-> ran ( F |` B ) ) -> ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( ran ( F |` D ) \ ran ( F |` B ) ) )
41 24 32 39 40 syl3anc 
 |-  ( ph -> ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( ran ( F |` D ) \ ran ( F |` B ) ) )
42 f1ofn 
 |-  ( F : D -1-1-onto-> D -> F Fn D )
43 fnresdm 
 |-  ( F Fn D -> ( F |` D ) = F )
44 1 42 43 3syl 
 |-  ( ph -> ( F |` D ) = F )
45 44 rneqd 
 |-  ( ph -> ran ( F |` D ) = ran F )
46 f1ofo 
 |-  ( F : D -1-1-onto-> D -> F : D -onto-> D )
47 forn 
 |-  ( F : D -onto-> D -> ran F = D )
48 1 46 47 3syl 
 |-  ( ph -> ran F = D )
49 45 48 eqtrd 
 |-  ( ph -> ran ( F |` D ) = D )
50 49 difeq1d 
 |-  ( ph -> ( ran ( F |` D ) \ ran ( F |` B ) ) = ( D \ ran ( F |` B ) ) )
51 50 f1oeq3d 
 |-  ( ph -> ( ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( ran ( F |` D ) \ ran ( F |` B ) ) <-> ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( D \ ran ( F |` B ) ) ) )
52 41 51 mpbid 
 |-  ( ph -> ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( D \ ran ( F |` B ) ) )
53 f1ococnv2 
 |-  ( ( F |` ( D \ B ) ) : ( D \ B ) -1-1-onto-> ( D \ ran ( F |` B ) ) -> ( ( F |` ( D \ B ) ) o. `' ( F |` ( D \ B ) ) ) = ( _I |` ( D \ ran ( F |` B ) ) ) )
54 52 53 syl 
 |-  ( ph -> ( ( F |` ( D \ B ) ) o. `' ( F |` ( D \ B ) ) ) = ( _I |` ( D \ ran ( F |` B ) ) ) )
55 11 21 54 3eqtr3d 
 |-  ( ph -> ( ( F |` ( D \ B ) ) o. `' F ) = ( _I |` ( D \ ran ( F |` B ) ) ) )