Theorem parhomvaln0

Description: Evaluate an inhabited parallel-arrow hom-set. Membership certifies the selected branch even when sethood hypotheses are unavailable. Compare parhomval for evaluation throughout the object domain. (Contributed by Zhi Wang, 17-Sep-2026)

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

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		nfcv	|- F/_ a if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) )
3		nfcv	|- F/_ b if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) )
4		nfcv	|- F/_ x if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) )
5		nfcv	|- F/_ y if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) )
6		eqeq12	|- ( ( x = a /\ y = b ) -> ( x = y <-> a = b ) )
7		simpl	|- ( ( x = a /\ y = b ) -> x = a )
8	7	eqeq1d	|- ( ( x = a /\ y = b ) -> ( x = X <-> a = X ) )
9		simpr	|- ( ( x = a /\ y = b ) -> y = b )
10	9	eqeq1d	|- ( ( x = a /\ y = b ) -> ( y = Y <-> b = Y ) )
11	8 10	anbi12d	|- ( ( x = a /\ y = b ) -> ( ( x = X /\ y = Y ) <-> ( a = X /\ b = Y ) ) )
12	11	ifbid	|- ( ( x = a /\ y = b ) -> if ( ( x = X /\ y = Y ) , S , (/) ) = if ( ( a = X /\ b = Y ) , S , (/) ) )
13	6 12	ifbieq2d	|- ( ( x = a /\ y = b ) -> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) = if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) ) )
14	2 3 4 5 13	cbvmpo	|- ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) ) = ( a e. B , b e. B |-> if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) ) )
15	1 14	eqtri	|- H = ( a e. B , b e. B |-> if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) ) )
16		eqeq12	|- ( ( a = U /\ b = V ) -> ( a = b <-> U = V ) )
17		simpl	|- ( ( a = U /\ b = V ) -> a = U )
18	17	eqeq1d	|- ( ( a = U /\ b = V ) -> ( a = X <-> U = X ) )
19		simpr	|- ( ( a = U /\ b = V ) -> b = V )
20	19	eqeq1d	|- ( ( a = U /\ b = V ) -> ( b = Y <-> V = Y ) )
21	18 20	anbi12d	|- ( ( a = U /\ b = V ) -> ( ( a = X /\ b = Y ) <-> ( U = X /\ V = Y ) ) )
22	21	ifbid	|- ( ( a = U /\ b = V ) -> if ( ( a = X /\ b = Y ) , S , (/) ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
23	16 22	ifbieq2d	|- ( ( a = U /\ b = V ) -> if ( a = b , { J } , if ( ( a = X /\ b = Y ) , S , (/) ) ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
24	15 23	elovmpoeq	|- ( F e. ( U H V ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )