Theorem hlgrcl2

Description: Reverse closure for rays. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	ishlg.p	$$⊢P={\mathrm{Base}}_G$$
	ishlg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	ishlg.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	ishlg2.g	$$⊢\phi \to G\in V$$
	ishlg2.1	$$⊢\phi \to C\in P$$
	hlgrcl1.1	$$⊢\phi \to AK\left(C\right)B$$
Assertion	hlgrcl2	$$⊢\phi \to B\in P$$

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	$$⊢P={\mathrm{Base}}_G$$
2		ishlg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		ishlg.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		ishlg2.g	$$⊢\phi \to G\in V$$
5		ishlg2.1	$$⊢\phi \to C\in P$$
6		hlgrcl1.1	$$⊢\phi \to AK\left(C\right)B$$
7	1 2 3 4 5	ishlg2	$$⊢\phi \to \left(AK\left(C\right)B\leftrightarrow \left(\left(A\in P\wedge B\in P\right)\wedge \left(A\ne C\wedge B\ne C\wedge \left(A\in \left(CIB\right)\vee B\in \left(CIA\right)\right)\right)\right)\right)$$
8	6 7	mpbid	$$⊢\phi \to \left(\left(A\in P\wedge B\in P\right)\wedge \left(A\ne C\wedge B\ne C\wedge \left(A\in \left(CIB\right)\vee B\in \left(CIA\right)\right)\right)\right)$$
9	8	simplrd	$$⊢\phi \to B\in P$$