Theorem parhomideq

Description: An endomorphism in the parallel-arrow construction has the identity value. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 16-Sep-2026)

	Ref	Expression
Hypotheses	parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomideq.f	|- ( ph -> F e. ( U H V ) )
	parhomideq.e	|- ( ph -> U = V )
Assertion	parhomideq	|- ( ph -> F = J )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2		parhomideq.f	|- ( ph -> F e. ( U H V ) )
3		parhomideq.e	|- ( ph -> U = V )
4	3	oveq2d	|- ( ph -> ( U H U ) = ( U H V ) )
5	2 4	eleqtrrd	|- ( ph -> F e. ( U H U ) )
6	1	elmpocl1	|- ( F e. ( U H V ) -> U e. B )
7	1	parhomidval	|- ( U e. B -> ( U H U ) = { J } )
8	2 6 7	3syl	|- ( ph -> ( U H U ) = { J } )
9	5 8	eleqtrd	|- ( ph -> F e. { J } )
10	9	elsnd	|- ( ph -> F = J )