Metamath Proof Explorer

Theorem fcoresf1

Description: If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024) (Revised by AV, 7-Oct-2024)

Ref Expression
Hypotheses fcores.f 
|- ( ph -> F : A --> B )
fcores.e 
|- E = ( ran F i^i C )
fcores.p 
|- P = ( `' F " C )
fcores.x 
|- X = ( F |` P )
fcores.g 
|- ( ph -> G : C --> D )
fcores.y 
|- Y = ( G |` E )
fcoresf1.i 
|- ( ph -> ( G o. F ) : P -1-1-> D )
Assertion fcoresf1 
|- ( ph -> ( X : P -1-1-> E /\ Y : E -1-1-> D ) )

Proof

Step Hyp Ref Expression
1 fcores.f 
 |-  ( ph -> F : A --> B )
2 fcores.e 
 |-  E = ( ran F i^i C )
3 fcores.p 
 |-  P = ( `' F " C )
4 fcores.x 
 |-  X = ( F |` P )
5 fcores.g 
 |-  ( ph -> G : C --> D )
6 fcores.y 
 |-  Y = ( G |` E )
7 fcoresf1.i 
 |-  ( ph -> ( G o. F ) : P -1-1-> D )
8 1 2 3 4 fcoreslem3 
 |-  ( ph -> X : P -onto-> E )
9 fof 
 |-  ( X : P -onto-> E -> X : P --> E )
10 8 9 syl 
 |-  ( ph -> X : P --> E )
11 dff13 
 |-  ( ( G o. F ) : P -1-1-> D <-> ( ( G o. F ) : P --> D /\ A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) ) )
12 1 2 3 4 5 6 fcoresf1lem 
 |-  ( ( ph /\ x e. P ) -> ( ( G o. F ) ` x ) = ( Y ` ( X ` x ) ) )
13 12 adantrr 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( G o. F ) ` x ) = ( Y ` ( X ` x ) ) )
14 1 2 3 4 5 6 fcoresf1lem 
 |-  ( ( ph /\ y e. P ) -> ( ( G o. F ) ` y ) = ( Y ` ( X ` y ) ) )
15 14 adantrl 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( G o. F ) ` y ) = ( Y ` ( X ` y ) ) )
16 13 15 eqeq12d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) <-> ( Y ` ( X ` x ) ) = ( Y ` ( X ` y ) ) ) )
17 16 imbi1d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) <-> ( ( Y ` ( X ` x ) ) = ( Y ` ( X ` y ) ) -> x = y ) ) )
18 fveq2 
 |-  ( ( X ` x ) = ( X ` y ) -> ( Y ` ( X ` x ) ) = ( Y ` ( X ` y ) ) )
19 18 a1i 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( X ` x ) = ( X ` y ) -> ( Y ` ( X ` x ) ) = ( Y ` ( X ` y ) ) ) )
20 19 imim1d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( ( Y ` ( X ` x ) ) = ( Y ` ( X ` y ) ) -> x = y ) -> ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
21 17 20 sylbid 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
22 21 ralimdvva 
 |-  ( ph -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> A. x e. P A. y e. P ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
23 22 adantld 
 |-  ( ph -> ( ( ( G o. F ) : P --> D /\ A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) ) -> A. x e. P A. y e. P ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
24 11 23 syl5bi 
 |-  ( ph -> ( ( G o. F ) : P -1-1-> D -> A. x e. P A. y e. P ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
25 7 24 mpd 
 |-  ( ph -> A. x e. P A. y e. P ( ( X ` x ) = ( X ` y ) -> x = y ) )
26 dff13 
 |-  ( X : P -1-1-> E <-> ( X : P --> E /\ A. x e. P A. y e. P ( ( X ` x ) = ( X ` y ) -> x = y ) ) )
27 10 25 26 sylanbrc 
 |-  ( ph -> X : P -1-1-> E )
28 2 a1i 
 |-  ( ph -> E = ( ran F i^i C ) )
29 inss2 
 |-  ( ran F i^i C ) C_ C
30 28 29 eqsstrdi 
 |-  ( ph -> E C_ C )
31 5 30 fssresd 
 |-  ( ph -> ( G |` E ) : E --> D )
32 6 feq1i 
 |-  ( Y : E --> D <-> ( G |` E ) : E --> D )
33 31 32 sylibr 
 |-  ( ph -> Y : E --> D )
34 1 2 3 4 fcoreslem2 
 |-  ( ph -> ran X = E )
35 34 eqcomd 
 |-  ( ph -> E = ran X )
36 35 eleq2d 
 |-  ( ph -> ( x e. E <-> x e. ran X ) )
37 fofn 
 |-  ( X : P -onto-> E -> X Fn P )
38 8 37 syl 
 |-  ( ph -> X Fn P )
39 fvelrnb 
 |-  ( X Fn P -> ( x e. ran X <-> E. a e. P ( X ` a ) = x ) )
40 38 39 syl 
 |-  ( ph -> ( x e. ran X <-> E. a e. P ( X ` a ) = x ) )
41 36 40 bitrd 
 |-  ( ph -> ( x e. E <-> E. a e. P ( X ` a ) = x ) )
42 35 eleq2d 
 |-  ( ph -> ( y e. E <-> y e. ran X ) )
43 fvelrnb 
 |-  ( X Fn P -> ( y e. ran X <-> E. b e. P ( X ` b ) = y ) )
44 38 43 syl 
 |-  ( ph -> ( y e. ran X <-> E. b e. P ( X ` b ) = y ) )
45 42 44 bitrd 
 |-  ( ph -> ( y e. E <-> E. b e. P ( X ` b ) = y ) )
46 41 45 anbi12d 
 |-  ( ph -> ( ( x e. E /\ y e. E ) <-> ( E. a e. P ( X ` a ) = x /\ E. b e. P ( X ` b ) = y ) ) )
47 fveqeq2 
 |-  ( x = a -> ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) <-> ( ( G o. F ) ` a ) = ( ( G o. F ) ` y ) ) )
48 eqeq1 
 |-  ( x = a -> ( x = y <-> a = y ) )
49 47 48 imbi12d 
 |-  ( x = a -> ( ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) <-> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` y ) -> a = y ) ) )
50 fveq2 
 |-  ( y = b -> ( ( G o. F ) ` y ) = ( ( G o. F ) ` b ) )
51 50 eqeq2d 
 |-  ( y = b -> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` y ) <-> ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) ) )
52 equequ2 
 |-  ( y = b -> ( a = y <-> a = b ) )
53 51 52 imbi12d 
 |-  ( y = b -> ( ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` y ) -> a = y ) <-> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) -> a = b ) ) )
54 49 53 rspc2v 
 |-  ( ( a e. P /\ b e. P ) -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) -> a = b ) ) )
55 54 adantl 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) -> a = b ) ) )
56 1 2 3 4 5 6 fcoresf1lem 
 |-  ( ( ph /\ a e. P ) -> ( ( G o. F ) ` a ) = ( Y ` ( X ` a ) ) )
57 56 adantrr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( G o. F ) ` a ) = ( Y ` ( X ` a ) ) )
58 1 2 3 4 5 6 fcoresf1lem 
 |-  ( ( ph /\ b e. P ) -> ( ( G o. F ) ` b ) = ( Y ` ( X ` b ) ) )
59 58 adantrl 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( G o. F ) ` b ) = ( Y ` ( X ` b ) ) )
60 57 59 eqeq12d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) <-> ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) ) )
61 60 imbi1d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) -> a = b ) <-> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> a = b ) ) )
62 fveq2 
 |-  ( a = b -> ( X ` a ) = ( X ` b ) )
63 62 a1i 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( a = b -> ( X ` a ) = ( X ` b ) ) )
64 63 imim2d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> a = b ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) )
65 61 64 sylbid 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( ( G o. F ) ` a ) = ( ( G o. F ) ` b ) -> a = b ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) )
66 55 65 syld 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) )
67 66 ex 
 |-  ( ph -> ( ( a e. P /\ b e. P ) -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) ) )
68 67 com23 
 |-  ( ph -> ( A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) -> ( ( a e. P /\ b e. P ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) ) )
69 68 adantld 
 |-  ( ph -> ( ( ( G o. F ) : P --> D /\ A. x e. P A. y e. P ( ( ( G o. F ) ` x ) = ( ( G o. F ) ` y ) -> x = y ) ) -> ( ( a e. P /\ b e. P ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) ) )
70 11 69 syl5bi 
 |-  ( ph -> ( ( G o. F ) : P -1-1-> D -> ( ( a e. P /\ b e. P ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) ) )
71 7 70 mpd 
 |-  ( ph -> ( ( a e. P /\ b e. P ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) ) )
72 71 impl 
 |-  ( ( ( ph /\ a e. P ) /\ b e. P ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) )
73 fveq2 
 |-  ( ( X ` a ) = x -> ( Y ` ( X ` a ) ) = ( Y ` x ) )
74 fveq2 
 |-  ( ( X ` b ) = y -> ( Y ` ( X ` b ) ) = ( Y ` y ) )
75 73 74 eqeqan12rd 
 |-  ( ( ( X ` b ) = y /\ ( X ` a ) = x ) -> ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) <-> ( Y ` x ) = ( Y ` y ) ) )
76 eqeq12 
 |-  ( ( ( X ` a ) = x /\ ( X ` b ) = y ) -> ( ( X ` a ) = ( X ` b ) <-> x = y ) )
77 76 ancoms 
 |-  ( ( ( X ` b ) = y /\ ( X ` a ) = x ) -> ( ( X ` a ) = ( X ` b ) <-> x = y ) )
78 75 77 imbi12d 
 |-  ( ( ( X ` b ) = y /\ ( X ` a ) = x ) -> ( ( ( Y ` ( X ` a ) ) = ( Y ` ( X ` b ) ) -> ( X ` a ) = ( X ` b ) ) <-> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) )
79 72 78 syl5ibcom 
 |-  ( ( ( ph /\ a e. P ) /\ b e. P ) -> ( ( ( X ` b ) = y /\ ( X ` a ) = x ) -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) )
80 79 expd 
 |-  ( ( ( ph /\ a e. P ) /\ b e. P ) -> ( ( X ` b ) = y -> ( ( X ` a ) = x -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) ) )
81 80 rexlimdva 
 |-  ( ( ph /\ a e. P ) -> ( E. b e. P ( X ` b ) = y -> ( ( X ` a ) = x -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) ) )
82 81 com23 
 |-  ( ( ph /\ a e. P ) -> ( ( X ` a ) = x -> ( E. b e. P ( X ` b ) = y -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) ) )
83 82 rexlimdva 
 |-  ( ph -> ( E. a e. P ( X ` a ) = x -> ( E. b e. P ( X ` b ) = y -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) ) )
84 83 impd 
 |-  ( ph -> ( ( E. a e. P ( X ` a ) = x /\ E. b e. P ( X ` b ) = y ) -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) )
85 46 84 sylbid 
 |-  ( ph -> ( ( x e. E /\ y e. E ) -> ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) )
86 85 ralrimivv 
 |-  ( ph -> A. x e. E A. y e. E ( ( Y ` x ) = ( Y ` y ) -> x = y ) )
87 dff13 
 |-  ( Y : E -1-1-> D <-> ( Y : E --> D /\ A. x e. E A. y e. E ( ( Y ` x ) = ( Y ` y ) -> x = y ) ) )
88 33 86 87 sylanbrc 
 |-  ( ph -> Y : E -1-1-> D )
89 27 88 jca 
 |-  ( ph -> ( X : P -1-1-> E /\ Y : E -1-1-> D ) )