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	|- C = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
Assertion	par2catid	|- ( C e. Cat /\ ( Id ` C ) = ( y e. 2o |-> 2o ) )

Proof

Step	Hyp	Ref	Expression
1		par2catid.c	|- C = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
2		2oex	|- 2o e. _V
3		2on	|- 2o e. On
4		ontr	|- ( 2o e. On -> Tr 2o )
5	3 4	ax-mp	|- Tr 2o
6		dftr4	|- ( Tr 2o <-> 2o C_ ~P 2o )
7	5 6	mpbi	|- 2o C_ ~P 2o
8		df-3o	|- 3o = suc 2o
9		df-suc	|- suc 2o = ( 2o u. { 2o } )
10	8 9	eqtri	|- 3o = ( 2o u. { 2o } )
11		eqid	|- ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) )
12		eqid	|- ( r e. 3o , s e. 3o |-> ( r i^i s ) ) = ( r e. 3o , s e. 3o |-> ( r i^i s ) )
13		eqid	|- ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) = ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) )
14	2 2 7 10 11 12 13 1	parcatid	|- ( C e. Cat /\ ( Id ` C ) = ( y e. 2o |-> 2o ) )