Theorem tglngne

Description: It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglngval.p	$$⊢P={\mathrm{Base}}_G$$
	tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglngval.x	$$⊢\phi \to X\in P$$
	tglngval.y	$$⊢\phi \to Y\in P$$
	tglngne.1	$$⊢\phi \to Z\in \left(XLY\right)$$
Assertion	tglngne	$$⊢\phi \to X\ne Y$$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$$⊢P={\mathrm{Base}}_G$$
2		tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglngval.x	$$⊢\phi \to X\in P$$
6		tglngval.y	$$⊢\phi \to Y\in P$$
7		tglngne.1	$$⊢\phi \to Z\in \left(XLY\right)$$
8		df-ov	$$⊢XLY=L\left(⟨X,Y⟩\right)$$
9	7 8	eleqtrdi	$$⊢\phi \to Z\in L\left(⟨X,Y⟩\right)$$
10		elfvdm	$$⊢Z\in L\left(⟨X,Y⟩\right)\to ⟨X,Y⟩\in \mathrm{dom}L$$
11	9 10	syl	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}L$$
12	1 2 3	tglnfn	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to LFn\left(\left(P\times P\right)\setminus \mathrm{I}\right)$$
13		fndm	$$⊢LFn\left(\left(P\times P\right)\setminus \mathrm{I}\right)\to \mathrm{dom}L=\left(P\times P\right)\setminus \mathrm{I}$$
14	4 12 13	3syl	$$⊢\phi \to \mathrm{dom}L=\left(P\times P\right)\setminus \mathrm{I}$$
15	11 14	eleqtrd	$$⊢\phi \to ⟨X,Y⟩\in \left(\left(P\times P\right)\setminus \mathrm{I}\right)$$
16	15	eldifbd	$$⊢\phi \to \neg ⟨X,Y⟩\in \mathrm{I}$$
17		df-br	$$⊢X\mathrm{I}Y\leftrightarrow ⟨X,Y⟩\in \mathrm{I}$$
18		ideqg	$$⊢Y\in P\to \left(X\mathrm{I}Y\leftrightarrow X=Y\right)$$
19	6 18	syl	$$⊢\phi \to \left(X\mathrm{I}Y\leftrightarrow X=Y\right)$$
20	17 19	bitr3id	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{I}\leftrightarrow X=Y\right)$$
21	20	necon3bbid	$$⊢\phi \to \left(\neg ⟨X,Y⟩\in \mathrm{I}\leftrightarrow X\ne Y\right)$$
22	16 21	mpbid	$$⊢\phi \to X\ne Y$$