Metamath Proof Explorer

Theorem parswapfunc

Description: The explicit exchange of the two parallel nonidentity arrows is an endofunctor with identity object function. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses parswapfunc.c ⊢ C = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
parswapfunc.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
parswapfunc.l ⊢ L = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
Assertion parswapfunc ⊢ I ↾ 2 𝑜 L ∈ C Func C

Proof

Step Hyp Ref Expression
1 parswapfunc.c ⊢ C = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
2 parswapfunc.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
3 parswapfunc.l ⊢ L = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
4 1 par2str ⊢ 2 𝑜 = Base C ∧ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = Hom ⁡ C ∧ p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s = comp ⁡ C
5 4 simp1i ⊢ 2 𝑜 = Base C
6 4 simp2i ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = Hom ⁡ C
7 1 par2catid ⊢ C ∈ Cat ∧ Id ⁡ C = t ∈ 2 𝑜 ⟼ 2 𝑜
8 7 simpli ⊢ C ∈ Cat
9 eqid ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅
10 2 parswapprop ⊢ A ⁡ 2 𝑜 = 2 𝑜 ∧ ∀ t ∈ 2 𝑜 A ⁡ t ∈ 2 𝑜 ∧ A ⁡ ∅ = 1 𝑜
11 10 simp1i ⊢ A ⁡ 2 𝑜 = 2 𝑜
12 10 simp2i ⊢ ∀ t ∈ 2 𝑜 A ⁡ t ∈ 2 𝑜
13 5 6 8 9 3 11 12 parmapfunc ⊢ I ↾ 2 𝑜 C Func C L
14 df-br ⊢ I ↾ 2 𝑜 C Func C L ↔ I ↾ 2 𝑜 L ∈ C Func C
15 13 14 mpbi ⊢ I ↾ 2 𝑜 L ∈ C Func C