Theorem hleqnid

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

	Ref	Expression
Hypotheses	ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
Assertion	hleqnid	⊢ ( 𝜑 → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5		ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6		ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7		hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		neirr	⊢ ¬ 𝐴 ≠ 𝐴
9	8	a1i	⊢ ( 𝜑 → ¬ 𝐴 ≠ 𝐴 )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 ) → 𝐴 ∈ 𝑃 )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 ) → 𝐵 ∈ 𝑃 )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 ) → 𝐺 ∈ TarskiG )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 ) → 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 )
14	1 2 3 10 11 10 12 13	hlne1	⊢ ( ( 𝜑 ∧ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 ) → 𝐴 ≠ 𝐴 )
15	9 14	mtand	⊢ ( 𝜑 → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝐵 )