Theorem hleqnid

Description: The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020)

	Ref	Expression
Hypotheses	ishlg.p	$$⊢P={\mathrm{Base}}_G$$
	ishlg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	ishlg.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	ishlg.a	$$⊢\phi \to A\in P$$
	ishlg.b	$$⊢\phi \to B\in P$$
	ishlg.c	$$⊢\phi \to C\in P$$
	hlln.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
Assertion	hleqnid	$$⊢\phi \to \neg AK\left(A\right)B$$

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		ishlg.a	$$⊢\phi \to A\in P$$
5		ishlg.b	$$⊢\phi \to B\in P$$
6		ishlg.c	$$⊢\phi \to C\in P$$
7		hlln.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
8		neirr	$$⊢\neg A\ne A$$
9	8	a1i	$$⊢\phi \to \neg A\ne A$$
10	4	adantr	$$⊢\left(\phi \wedge AK\left(A\right)B\right)\to A\in P$$
11	5	adantr	$$⊢\left(\phi \wedge AK\left(A\right)B\right)\to B\in P$$
12	7	adantr	$$⊢\left(\phi \wedge AK\left(A\right)B\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
13		simpr	$$⊢\left(\phi \wedge AK\left(A\right)B\right)\to AK\left(A\right)B$$
14	1 2 3 10 11 10 12 13	hlne1	$$⊢\left(\phi \wedge AK\left(A\right)B\right)\to A\ne A$$
15	9 14	mtand	$$⊢\phi \to \neg AK\left(A\right)B$$