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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parmapcl.f ⊢ φ → F ∈ U H V
parmapcl.i ⊢ φ → A ⁡ J = J
parmapcl.a ⊢ φ ∧ F ∈ S → A ⁡ F ∈ S
Assertion parmapcl ⊢ φ → A ⁡ F ∈ U H V

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parmapcl.f ⊢ φ → F ∈ U H V
3 parmapcl.i ⊢ φ → A ⁡ J = J
4 parmapcl.a ⊢ φ ∧ F ∈ S → A ⁡ F ∈ S
5 3 adantr ⊢ φ ∧ U = V → A ⁡ J = J
6 2 adantr ⊢ φ ∧ U = V → F ∈ U H V
7 simpr ⊢ φ ∧ U = V → U = V
8 1 6 7 parhomideq ⊢ φ ∧ U = V → F = J
9 8 fveq2d ⊢ φ ∧ U = V → A ⁡ F = A ⁡ J
10 5 9 8 3eqtr4d ⊢ φ ∧ U = V → A ⁡ F = F
11 10 6 eqeltrd ⊢ φ ∧ U = V → A ⁡ F ∈ U H V
12 2 adantr ⊢ φ ∧ ¬ U = V → F ∈ U H V
13 1 parhomvaln0 ⊢ F ∈ U H V → U H V = if U = V J if U = X ∧ V = Y S ∅
14 12 13 syl ⊢ φ ∧ ¬ U = V → U H V = if U = V J if U = X ∧ V = Y S ∅
15 simpr ⊢ φ ∧ ¬ U = V → ¬ U = V
16 15 iffalsed ⊢ φ ∧ ¬ U = V → if U = V J if U = X ∧ V = Y S ∅ = if U = X ∧ V = Y S ∅
17 14 16 eqtrd ⊢ φ ∧ ¬ U = V → U H V = if U = X ∧ V = Y S ∅
18 12 17 eleqtrd ⊢ φ ∧ ¬ U = V → F ∈ if U = X ∧ V = Y S ∅
19 elif0 ⊢ F ∈ if U = X ∧ V = Y S ∅ ↔ U = X ∧ V = Y ∧ F ∈ S
20 18 19 sylib ⊢ φ ∧ ¬ U = V → U = X ∧ V = Y ∧ F ∈ S
21 20 simprd ⊢ φ ∧ ¬ U = V → F ∈ S
22 21 4 syldan ⊢ φ ∧ ¬ U = V → A ⁡ F ∈ S
23 20 simpld ⊢ φ ∧ ¬ U = V → U = X ∧ V = Y
24 23 iftrued ⊢ φ ∧ ¬ U = V → if U = X ∧ V = Y S ∅ = S
25 17 24 eqtrd ⊢ φ ∧ ¬ U = V → U H V = S
26 22 25 eleqtrrd ⊢ φ ∧ ¬ U = V → A ⁡ F ∈ U H V
27 11 26 pm2.61dan ⊢ φ → A ⁡ F ∈ U H V