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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
Assertion	parhomvaln0	⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		nfcv	⊢ Ⅎ 𝑎 if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) )
3		nfcv	⊢ Ⅎ 𝑏 if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) )
4		nfcv	⊢ Ⅎ 𝑥 if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) )
5		nfcv	⊢ Ⅎ 𝑦 if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) )
6		eqeq12	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 = 𝑦 ↔ 𝑎 = 𝑏 ) )
7		simpl	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
8	7	eqeq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 = 𝑋 ↔ 𝑎 = 𝑋 ) )
9		simpr	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑦 = 𝑏 )
10	9	eqeq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑦 = 𝑌 ↔ 𝑏 = 𝑌 ) )
11	8 10	anbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ↔ ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) ) )
12	11	ifbid	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) = if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) )
13	6 12	ifbieq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) = if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) ) )
14	2 3 4 5 13	cbvmpo	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) ) )
15	1 14	eqtri	⊢ 𝐻 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) ) )
16		eqeq12	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 𝑎 = 𝑏 ↔ 𝑈 = 𝑉 ) )
17		simpl	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑎 = 𝑈 )
18	17	eqeq1d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 𝑎 = 𝑋 ↔ 𝑈 = 𝑋 ) )
19		simpr	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑏 = 𝑉 )
20	19	eqeq1d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 𝑏 = 𝑌 ↔ 𝑉 = 𝑌 ) )
21	18 20	anbi12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) ↔ ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ) )
22	21	ifbid	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
23	16 22	ifbieq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → if ( 𝑎 = 𝑏 , { 𝐽 } , if ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) , 𝑆 , ∅ ) ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
24	15 23	elovmpoeq	⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )