Theorem par2str

Description: The object set, hom operation, and composition of the concrete two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypothesis	par2str.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
Assertion	par2str	⊢ ( 2o = ( Base ‘ 𝐶 ) ∧ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( Hom ‘ 𝐶 ) ∧ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( comp ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		par2str.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
2		2oex	⊢ 2o ∈ V
3	1 2	catbas	⊢ 2o = ( Base ‘ 𝐶 )
4	2 2	mpoex	⊢ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ∈ V
5	1 4	cathomfval	⊢ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( Hom ‘ 𝐶 )
6	2 2	xpex	⊢ ( 2o × 2o ) ∈ V
7	6 2	mpoex	⊢ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ∈ V
8	1 7	catcofval	⊢ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( comp ‘ 𝐶 )
9	3 5 8	3pm3.2i	⊢ ( 2o = ( Base ‘ 𝐶 ) ∧ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( Hom ‘ 𝐶 ) ∧ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( comp ‘ 𝐶 ) )