Theorem parhomid2

Description: Variant of parhomid . (Contributed by Zhi Wang, 14-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomid.j	|- J e. _V
	parhomid.u	|- ( ph -> U e. B )
	parhomid2.s	|- S e. _V
Assertion	parhomid2	|- ( ph -> J e. ( U H U ) )

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		parhomid.j	|- J e. _V
3		parhomid.u	|- ( ph -> U e. B )
4		parhomid2.s	|- S e. _V
5	2	snid	|- J e. { J }
6	1 4	parhomval	|- ( ( U e. B /\ U e. B ) -> ( U H U ) = if ( U = U , { J } , if ( ( U = X /\ U = Y ) , S , (/) ) ) )
7	3 3 6	syl2anc	|- ( ph -> ( U H U ) = if ( U = U , { J } , if ( ( U = X /\ U = Y ) , S , (/) ) ) )
8		eqid	|- U = U
9	8	iftruei	|- if ( U = U , { J } , if ( ( U = X /\ U = Y ) , S , (/) ) ) = { J }
10	7 9	eqtrdi	|- ( ph -> ( U H U ) = { J } )
11	5 10	eleqtrrid	|- ( ph -> J e. ( U H U ) )