Theorem par2cat

Description: The explicitly given two-object, two-parallel-arrow category exists. This closed theorem discharges the constructor premises in par2catid . (Contributed by Zhi Wang, 14-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
2	1	par2catid	⊢ ( { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ∈ Cat ∧ ( Id ‘ { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) = ( 𝑦 ∈ 2o ↦ 2o ) )
3	2	simpli	⊢ { ⟨ ( Base ‘ ndx ) , 2o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ∈ Cat