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	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
	parswapfunc.a	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
	parswapfunc.l	⊢ 𝐿 = ( 𝑢 ∈ 2o , 𝑣 ∈ 2o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
Assertion	parswapfunc	⊢ ⟨ ( I ↾ 2o ) , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		parswapfunc.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
2		parswapfunc.a	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
3		parswapfunc.l	⊢ 𝐿 = ( 𝑢 ∈ 2o , 𝑣 ∈ 2o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
4	1	par2str	⊢ ( 2o = ( Base ‘ 𝐶 ) ∧ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( Hom ‘ 𝐶 ) ∧ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( comp ‘ 𝐶 ) )
5	4	simp1i	⊢ 2o = ( Base ‘ 𝐶 )
6	4	simp2i	⊢ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( Hom ‘ 𝐶 )
7	1	par2catid	⊢ ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑡 ∈ 2o ↦ 2o ) )
8	7	simpli	⊢ 𝐶 ∈ Cat
9		eqid	⊢ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) )
10	2	parswapprop	⊢ ( ( 𝐴 ‘ 2o ) = 2o ∧ ∀ 𝑡 ∈ 2o ( 𝐴 ‘ 𝑡 ) ∈ 2o ∧ ( 𝐴 ‘ ∅ ) = 1o )
11	10	simp1i	⊢ ( 𝐴 ‘ 2o ) = 2o
12	10	simp2i	⊢ ∀ 𝑡 ∈ 2o ( 𝐴 ‘ 𝑡 ) ∈ 2o
13	5 6 8 9 3 11 12	parmapfunc	⊢ ( I ↾ 2o ) ( 𝐶 Func 𝐶 ) 𝐿
14		df-br	⊢ ( ( I ↾ 2o ) ( 𝐶 Func 𝐶 ) 𝐿 ↔ ⟨ ( I ↾ 2o ) , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐶 ) )
15	13 14	mpbi	⊢ ⟨ ( I ↾ 2o ) , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐶 )