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=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
	parhomid.j	$$⊢J\in \mathrm{V}$$
	parhomid.u	$$⊢\phi \to U\in B$$
	parhomid2.s	$$⊢S\in \mathrm{V}$$
Assertion	parhomid2	$$⊢\phi \to J\in \left(UHU\right)$$

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
2		parhomid.j	$$⊢J\in \mathrm{V}$$
3		parhomid.u	$$⊢\phi \to U\in B$$
4		parhomid2.s	$$⊢S\in \mathrm{V}$$
5	2	snid	$$⊢J\in \left\{J\right\}$$
6	1 4	parhomval	$$⊢\left(U\in B\wedge U\in B\right)\to UHU=if\left(U=U,\left\{J\right\},if\left(\left(U=X\wedge U=Y\right),S,\varnothing \right)\right)$$
7	3 3 6	syl2anc	$$⊢\phi \to UHU=if\left(U=U,\left\{J\right\},if\left(\left(U=X\wedge U=Y\right),S,\varnothing \right)\right)$$
8		eqid	$$⊢U=U$$
9	8	iftruei	$$⊢if\left(U=U,\left\{J\right\},if\left(\left(U=X\wedge U=Y\right),S,\varnothing \right)\right)=\left\{J\right\}$$
10	7 9	eqtrdi	$$⊢\phi \to UHU=\left\{J\right\}$$
11	5 10	eleqtrrid	$$⊢\phi \to J\in \left(UHU\right)$$