Theorem parhomcl2

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

	Ref	Expression
Hypotheses	parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomval.s	|- S e. _V
	parhomel.j	|- J e. _V
	parhomcl2.k	|- K = ( S u. { J } )
	parhomcl2.u	|- ( ph -> U e. B )
	parhomcl2.v	|- ( ph -> V e. B )
	parhomcl2.f	|- ( ph -> F e. ( U H V ) )
Assertion	parhomcl2	|- ( ph -> F e. K )

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		parhomval.s	|- S e. _V
3		parhomel.j	|- J e. _V
4		parhomcl2.k	|- K = ( S u. { J } )
5		parhomcl2.u	|- ( ph -> U e. B )
6		parhomcl2.v	|- ( ph -> V e. B )
7		parhomcl2.f	|- ( ph -> F e. ( U H V ) )
8	1 2 3	parhomel	|- ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
9	5 6 8	syl2anc	|- ( ph -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
10	7 9	mpbid	|- ( ph -> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) )
11	3	elsn2	|- ( F e. { J } <-> F = J )
12	11	bilanri	|- ( ( U = V /\ F = J ) -> F e. { J } )
13	12	olcd	|- ( ( U = V /\ F = J ) -> ( F e. S \/ F e. { J } ) )
14		simprr	|- ( ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) -> F e. S )
15	14	orcd	|- ( ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) -> ( F e. S \/ F e. { J } ) )
16	13 15	jaoi	|- ( ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> ( F e. S \/ F e. { J } ) )
17	10 16	syl	|- ( ph -> ( F e. S \/ F e. { J } ) )
18		elun	|- ( F e. ( S u. { J } ) <-> ( F e. S \/ F e. { J } ) )
19	17 18	sylibr	|- ( ph -> F e. ( S u. { J } ) )
20	19 4	eleqtrrdi	|- ( ph -> F e. K )