Metamath Proof Explorer

Theorem parhomco

Description: When every member of the parallel-arrow class S is a subset of J , intersection of composable arrows belongs to the hom-set from the first object to the last. The subset hypothesis supplies the required intersection identity laws; it does not follow from the hom construction alone. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parhomval.h 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parhomeqor.f 
|- ( ph -> F e. ( U H V ) )
parhomeqor.g 
|- ( ph -> G e. ( V H W ) )
parhomco.p 
|- S C_ ~P J
Assertion parhomco 
|- ( ph -> ( G i^i F ) e. ( U H W ) )

Proof

Step Hyp Ref Expression
1 parhomval.h 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2 parhomeqor.f 
 |-  ( ph -> F e. ( U H V ) )
3 parhomeqor.g 
 |-  ( ph -> G e. ( V H W ) )
4 parhomco.p 
 |-  S C_ ~P J
5 3 adantr 
 |-  ( ( ph /\ U = V ) -> G e. ( V H W ) )
6 2 adantr 
 |-  ( ( ph /\ U = V ) -> F e. ( U H V ) )
7 simpr 
 |-  ( ( ph /\ U = V ) -> U = V )
8 1 6 7 parhomideq 
 |-  ( ( ph /\ U = V ) -> F = J )
9 8 ineq2d 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = ( G i^i J ) )
10 1 4 3 parhomss 
 |-  ( ph -> G C_ J )
11 10 adantr 
 |-  ( ( ph /\ U = V ) -> G C_ J )
12 dfss2 
 |-  ( G C_ J <-> ( G i^i J ) = G )
13 11 12 sylib 
 |-  ( ( ph /\ U = V ) -> ( G i^i J ) = G )
14 9 13 eqtrd 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = G )
15 7 oveq1d 
 |-  ( ( ph /\ U = V ) -> ( U H W ) = ( V H W ) )
16 5 14 15 3eltr4d 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) e. ( U H W ) )
17 3 adantr 
 |-  ( ( ph /\ V = W ) -> G e. ( V H W ) )
18 simpr 
 |-  ( ( ph /\ V = W ) -> V = W )
19 1 17 18 parhomideq 
 |-  ( ( ph /\ V = W ) -> G = J )
20 19 ineq1d 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = ( J i^i F ) )
21 1 4 2 parhomss 
 |-  ( ph -> F C_ J )
22 21 adantr 
 |-  ( ( ph /\ V = W ) -> F C_ J )
23 sseqin2 
 |-  ( F C_ J <-> ( J i^i F ) = F )
24 22 23 sylib 
 |-  ( ( ph /\ V = W ) -> ( J i^i F ) = F )
25 20 24 eqtrd 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = F )
26 2 adantr 
 |-  ( ( ph /\ V = W ) -> F e. ( U H V ) )
27 18 oveq2d 
 |-  ( ( ph /\ V = W ) -> ( U H V ) = ( U H W ) )
28 26 27 eleqtrd 
 |-  ( ( ph /\ V = W ) -> F e. ( U H W ) )
29 25 28 eqeltrd 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) e. ( U H W ) )
30 1 2 3 parhomeqor 
 |-  ( ph -> ( U = V \/ V = W ) )
31 16 29 30 mpjaodan 
 |-  ( ph -> ( G i^i F ) e. ( U H W ) )