# Metamath Proof Explorer

## 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}$