Metamath Proof Explorer

Theorem parmapcl

Description: A map fixing the identity value and preserving the parallel-arrow class preserves each hom-set. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parmapcl.h 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parmapcl.f 
|- ( ph -> F e. ( U H V ) )
parmapcl.i 
|- ( ph -> ( A ` J ) = J )
parmapcl.a 
|- ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
Assertion parmapcl 
|- ( ph -> ( A ` F ) e. ( U H V ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2 parmapcl.f 
 |-  ( ph -> F e. ( U H V ) )
3 parmapcl.i 
 |-  ( ph -> ( A ` J ) = J )
4 parmapcl.a 
 |-  ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
5 3 adantr 
 |-  ( ( ph /\ U = V ) -> ( A ` J ) = J )
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 fveq2d 
 |-  ( ( ph /\ U = V ) -> ( A ` F ) = ( A ` J ) )
10 5 9 8 3eqtr4d 
 |-  ( ( ph /\ U = V ) -> ( A ` F ) = F )
11 10 6 eqeltrd 
 |-  ( ( ph /\ U = V ) -> ( A ` F ) e. ( U H V ) )
12 2 adantr 
 |-  ( ( ph /\ -. U = V ) -> F e. ( U H V ) )
13 1 parhomvaln0 
 |-  ( F e. ( U H V ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
14 12 13 syl 
 |-  ( ( ph /\ -. U = V ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
15 simpr 
 |-  ( ( ph /\ -. U = V ) -> -. U = V )
16 15 iffalsed 
 |-  ( ( ph /\ -. U = V ) -> if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
17 14 16 eqtrd 
 |-  ( ( ph /\ -. U = V ) -> ( U H V ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
18 12 17 eleqtrd 
 |-  ( ( ph /\ -. U = V ) -> F e. if ( ( U = X /\ V = Y ) , S , (/) ) )
19 elif0 
 |-  ( F e. if ( ( U = X /\ V = Y ) , S , (/) ) <-> ( ( U = X /\ V = Y ) /\ F e. S ) )
20 18 19 sylib 
 |-  ( ( ph /\ -. U = V ) -> ( ( U = X /\ V = Y ) /\ F e. S ) )
21 20 simprd 
 |-  ( ( ph /\ -. U = V ) -> F e. S )
22 21 4 syldan 
 |-  ( ( ph /\ -. U = V ) -> ( A ` F ) e. S )
23 20 simpld 
 |-  ( ( ph /\ -. U = V ) -> ( U = X /\ V = Y ) )
24 23 iftrued 
 |-  ( ( ph /\ -. U = V ) -> if ( ( U = X /\ V = Y ) , S , (/) ) = S )
25 17 24 eqtrd 
 |-  ( ( ph /\ -. U = V ) -> ( U H V ) = S )
26 22 25 eleqtrrd 
 |-  ( ( ph /\ -. U = V ) -> ( A ` F ) e. ( U H V ) )
27 11 26 pm2.61dan 
 |-  ( ph -> ( A ` F ) e. ( U H V ) )