Theorem tgelrnln

Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	$$⊢B={\mathrm{Base}}_G$$
	tglineelsb2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglineelsb2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglineelsb2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgelrnln.x	$$⊢\phi \to X\in B$$
	tgelrnln.y	$$⊢\phi \to Y\in B$$
	tgelrnln.d	$$⊢\phi \to X\ne Y$$
Assertion	tgelrnln	$$⊢\phi \to XLY\in \mathrm{ran}L$$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$$⊢B={\mathrm{Base}}_G$$
2		tglineelsb2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		tglineelsb2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
4		tglineelsb2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgelrnln.x	$$⊢\phi \to X\in B$$
6		tgelrnln.y	$$⊢\phi \to Y\in B$$
7		tgelrnln.d	$$⊢\phi \to X\ne Y$$
8		df-ov	$$⊢XLY=L\left(⟨X,Y⟩\right)$$
9	1 3 2	tglnfn	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to LFn\left(\left(B\times B\right)\setminus \mathrm{I}\right)$$
10	4 9	syl	$$⊢\phi \to LFn\left(\left(B\times B\right)\setminus \mathrm{I}\right)$$
11	5 6	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(B\times B\right)$$
12		df-br	$$⊢X\mathrm{I}Y\leftrightarrow ⟨X,Y⟩\in \mathrm{I}$$
13		ideqg	$$⊢Y\in B\to \left(X\mathrm{I}Y\leftrightarrow X=Y\right)$$
14	12 13	bitr3id	$$⊢Y\in B\to \left(⟨X,Y⟩\in \mathrm{I}\leftrightarrow X=Y\right)$$
15	14	necon3bbid	$$⊢Y\in B\to \left(\neg ⟨X,Y⟩\in \mathrm{I}\leftrightarrow X\ne Y\right)$$
16	15	biimpar	$$⊢\left(Y\in B\wedge X\ne Y\right)\to \neg ⟨X,Y⟩\in \mathrm{I}$$
17	6 7 16	syl2anc	$$⊢\phi \to \neg ⟨X,Y⟩\in \mathrm{I}$$
18	11 17	eldifd	$$⊢\phi \to ⟨X,Y⟩\in \left(\left(B\times B\right)\setminus \mathrm{I}\right)$$
19		fnfvelrn	$$⊢\left(LFn\left(\left(B\times B\right)\setminus \mathrm{I}\right)\wedge ⟨X,Y⟩\in \left(\left(B\times B\right)\setminus \mathrm{I}\right)\right)\to L\left(⟨X,Y⟩\right)\in \mathrm{ran}L$$
20	10 18 19	syl2anc	$$⊢\phi \to L\left(⟨X,Y⟩\right)\in \mathrm{ran}L$$
21	8 20	eqeltrid	$$⊢\phi \to XLY\in \mathrm{ran}L$$