Theorem par2catid

Description: A concrete category with two objects and two parallel nonidentity arrows. The two identity arrows both have raw value 2o ; their sources and targets distinguish them. The parallel arrows have raw values the empty set and 1o . (Contributed by Zhi Wang, 14-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		par2catid.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		2on	⊢ 2o ∈ On
4		ontr	⊢ ( 2o ∈ On → Tr 2o )
5	3 4	ax-mp	⊢ Tr 2o
6		dftr4	⊢ ( Tr 2o ↔ 2o ⊆ 𝒫 2o )
7	5 6	mpbi	⊢ 2o ⊆ 𝒫 2o
8		df-3o	⊢ 3o = suc 2o
9		df-suc	⊢ suc 2o = ( 2o ∪ { 2o } )
10	8 9	eqtri	⊢ 3o = ( 2o ∪ { 2o } )
11		eqid	⊢ ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) ) = ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) )
12		eqid	⊢ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) = ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) )
13		eqid	⊢ ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( 𝑝 ∈ ( 2o × 2o ) , 𝑞 ∈ 2o ↦ ( 𝑟 ∈ 3o , 𝑠 ∈ 3o ↦ ( 𝑟 ∩ 𝑠 ) ) )
14	2 2 7 10 11 12 13 1	parcatid	⊢ ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 2o ↦ 2o ) )