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 ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
Assertion parmapcl ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2 parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3 parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
4 parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
8 1 6 7 parhomideq ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
9 8 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ 𝐽 ) )
10 5 9 8 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = 𝐹 )
11 10 6 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
13 1 parhomvaln0 ⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ¬ 𝑈 = 𝑉 )
16 15 iffalsed ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
17 14 16 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
18 12 17 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
19 elif0 ⊢ ( 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ↔ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) )
20 18 19 sylib ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) )
21 20 simprd ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 ∈ 𝑆 )
22 21 4 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
23 20 simpld ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )
24 23 iftrued ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) = 𝑆 )
25 17 24 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = 𝑆 )
26 22 25 eleqtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )
27 11 26 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )