Theorem tglnpt

Description: Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019)

	Ref	Expression
Hypotheses	tglng.p	$$⊢P={\mathrm{Base}}_G$$
	tglng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglng.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglnpt.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglnpt.a	$$⊢\phi \to A\in \mathrm{ran}L$$
	tglnpt.x	$$⊢\phi \to X\in A$$
Assertion	tglnpt	$$⊢\phi \to X\in P$$

Proof

Step	Hyp	Ref	Expression
1		tglng.p	$$⊢P={\mathrm{Base}}_G$$
2		tglng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglng.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglnpt.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglnpt.a	$$⊢\phi \to A\in \mathrm{ran}L$$
6		tglnpt.x	$$⊢\phi \to X\in A$$
7	1 2 3	tglnunirn	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to \bigcup \mathrm{ran}L\subseteq P$$
8	4 7	syl	$$⊢\phi \to \bigcup \mathrm{ran}L\subseteq P$$
9		elssuni	$$⊢A\in \mathrm{ran}L\to A\subseteq \bigcup \mathrm{ran}L$$
10	5 9	syl	$$⊢\phi \to A\subseteq \bigcup \mathrm{ran}L$$
11	10 6	sseldd	$$⊢\phi \to X\in \bigcup \mathrm{ran}L$$
12	8 11	sseldd	$$⊢\phi \to X\in P$$