Theorem hlgrcl1

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

	Ref	Expression
Hypotheses	ishlg.p	|- P = ( Base ` G )
	ishlg.i	|- I = ( Itv ` G )
	ishlg.k	|- K = ( hlG ` G )
	ishlg2.g	|- ( ph -> G e. V )
	ishlg2.1	|- ( ph -> C e. P )
	hlgrcl1.1	|- ( ph -> A ( K ` C ) B )
Assertion	hlgrcl1	|- ( ph -> A e. P )

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	|- P = ( Base ` G )
2		ishlg.i	|- I = ( Itv ` G )
3		ishlg.k	|- K = ( hlG ` G )
4		ishlg2.g	|- ( ph -> G e. V )
5		ishlg2.1	|- ( ph -> C e. P )
6		hlgrcl1.1	|- ( ph -> A ( K ` C ) B )
7	1 2 3 4 5	ishlg2	|- ( ph -> ( A ( K ` C ) B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) )
8	6 7	mpbid	|- ( ph -> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
9	8	simplld	|- ( ph -> A e. P )