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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomval.s	⊢ 𝑆 ∈ V
	parhomel.j	⊢ 𝐽 ∈ V
	parhomcl2.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
	parhomcl2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parhomcl2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	parhomcl2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
Assertion	parhomcl2	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomval.s	⊢ 𝑆 ∈ V
3		parhomel.j	⊢ 𝐽 ∈ V
4		parhomcl2.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
5		parhomcl2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
6		parhomcl2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
7		parhomcl2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
8	1 2 3	parhomel	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
9	5 6 8	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
10	7 9	mpbid	⊢ ( 𝜑 → ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) )
11	3	elsn2	⊢ ( 𝐹 ∈ { 𝐽 } ↔ 𝐹 = 𝐽 )
12	11	bilanri	⊢ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) → 𝐹 ∈ { 𝐽 } )
13	12	olcd	⊢ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) → ( 𝐹 ∈ 𝑆 ∨ 𝐹 ∈ { 𝐽 } ) )
14		simprr	⊢ ( ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) → 𝐹 ∈ 𝑆 )
15	14	orcd	⊢ ( ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) → ( 𝐹 ∈ 𝑆 ∨ 𝐹 ∈ { 𝐽 } ) )
16	13 15	jaoi	⊢ ( ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → ( 𝐹 ∈ 𝑆 ∨ 𝐹 ∈ { 𝐽 } ) )
17	10 16	syl	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ∨ 𝐹 ∈ { 𝐽 } ) )
18		elun	⊢ ( 𝐹 ∈ ( 𝑆 ∪ { 𝐽 } ) ↔ ( 𝐹 ∈ 𝑆 ∨ 𝐹 ∈ { 𝐽 } ) )
19	17 18	sylibr	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 ∪ { 𝐽 } ) )
20	19 4	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )