This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imaf1hom

Description: The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imaf1hom.s 
|- S = ( F " A )
imaf1hom.1 
|- ( ph -> F : B -1-1-> C )
imaf1hom.x 
|- ( ph -> X e. S )
imaf1hom.y 
|- ( ph -> Y e. S )
imaf1hom.f 
|- ( ph -> F e. V )
imaf1hom.k 
|- K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
Assertion imaf1hom 
|- ( ph -> ( X K Y ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 imaf1hom.s 
 |-  S = ( F " A )
2 imaf1hom.1 
 |-  ( ph -> F : B -1-1-> C )
3 imaf1hom.x 
 |-  ( ph -> X e. S )
4 imaf1hom.y 
 |-  ( ph -> Y e. S )
5 imaf1hom.f 
 |-  ( ph -> F e. V )
6 imaf1hom.k 
 |-  K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
7 5 5 3 4 6 imasubclem3 
 |-  ( ph -> ( X K Y ) = U_ p e. ( ( `' F " { X } ) X. ( `' F " { Y } ) ) ( ( G ` p ) " ( H ` p ) ) )
8 1 2 3 imaf1homlem 
 |-  ( ph -> ( { ( `' F ` X ) } = ( `' F " { X } ) /\ ( F ` ( `' F ` X ) ) = X /\ ( `' F ` X ) e. B ) )
9 8 simp1d 
 |-  ( ph -> { ( `' F ` X ) } = ( `' F " { X } ) )
10 1 2 4 imaf1homlem 
 |-  ( ph -> ( { ( `' F ` Y ) } = ( `' F " { Y } ) /\ ( F ` ( `' F ` Y ) ) = Y /\ ( `' F ` Y ) e. B ) )
11 10 simp1d 
 |-  ( ph -> { ( `' F ` Y ) } = ( `' F " { Y } ) )
12 9 11 xpeq12d 
 |-  ( ph -> ( { ( `' F ` X ) } X. { ( `' F ` Y ) } ) = ( ( `' F " { X } ) X. ( `' F " { Y } ) ) )
13 fvex 
 |-  ( `' F ` X ) e. _V
14 fvex 
 |-  ( `' F ` Y ) e. _V
15 13 14 xpsn 
 |-  ( { ( `' F ` X ) } X. { ( `' F ` Y ) } ) = { <. ( `' F ` X ) , ( `' F ` Y ) >. }
16 12 15 eqtr3di 
 |-  ( ph -> ( ( `' F " { X } ) X. ( `' F " { Y } ) ) = { <. ( `' F ` X ) , ( `' F ` Y ) >. } )
17 16 iuneq1d 
 |-  ( ph -> U_ p e. ( ( `' F " { X } ) X. ( `' F " { Y } ) ) ( ( G ` p ) " ( H ` p ) ) = U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) )
18 7 17 eqtrd 
 |-  ( ph -> ( X K Y ) = U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) )
19 opex 
 |-  <. ( `' F ` X ) , ( `' F ` Y ) >. e. _V
20 fveq2 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( G ` p ) = ( G ` <. ( `' F ` X ) , ( `' F ` Y ) >. ) )
21 df-ov 
 |-  ( ( `' F ` X ) G ( `' F ` Y ) ) = ( G ` <. ( `' F ` X ) , ( `' F ` Y ) >. )
22 20 21 eqtr4di 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( G ` p ) = ( ( `' F ` X ) G ( `' F ` Y ) ) )
23 fveq2 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( H ` p ) = ( H ` <. ( `' F ` X ) , ( `' F ` Y ) >. ) )
24 df-ov 
 |-  ( ( `' F ` X ) H ( `' F ` Y ) ) = ( H ` <. ( `' F ` X ) , ( `' F ` Y ) >. )
25 23 24 eqtr4di 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( H ` p ) = ( ( `' F ` X ) H ( `' F ` Y ) ) )
26 22 25 imaeq12d 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( ( G ` p ) " ( H ` p ) ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )
27 19 26 iunxsn 
 |-  U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) )
28 18 27 eqtrdi 
 |-  ( ph -> ( X K Y ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )