# Metamath Proof Explorer

## Theorem tglnunirn

Description: Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-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)$
Assertion tglnunirn ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to \bigcup \mathrm{ran}{L}\subseteq {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 1 2 3 tglng ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to {L}=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)$
5 4 rneqd ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to \mathrm{ran}{L}=\mathrm{ran}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)$
6 5 eleq2d ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to \left({p}\in \mathrm{ran}{L}↔{p}\in \mathrm{ran}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)\right)$
7 6 biimpa ${⊢}\left({G}\in {𝒢}_{\mathrm{Tarski}}\wedge {p}\in \mathrm{ran}{L}\right)\to {p}\in \mathrm{ran}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)$
8 eqid ${⊢}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)$
9 1 fvexi ${⊢}{P}\in \mathrm{V}$
10 9 rabex ${⊢}\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\in \mathrm{V}$
11 8 10 elrnmpo ${⊢}{p}\in \mathrm{ran}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)↔\exists {x}\in {P}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({P}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{p}=\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}$
12 ssrab2 ${⊢}\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\subseteq {P}$
13 sseq1 ${⊢}{p}=\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\to \left({p}\subseteq {P}↔\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\subseteq {P}\right)$
14 12 13 mpbiri ${⊢}{p}=\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\to {p}\subseteq {P}$
15 14 rexlimivw ${⊢}\exists {y}\in \left({P}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{p}=\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\to {p}\subseteq {P}$
16 15 rexlimivw ${⊢}\exists {x}\in {P}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({P}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{p}=\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\to {p}\subseteq {P}$
17 11 16 sylbi ${⊢}{p}\in \mathrm{ran}\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {P}|\left({z}\in \left({x}{I}{y}\right)\vee {x}\in \left({z}{I}{y}\right)\vee {y}\in \left({x}{I}{z}\right)\right)\right\}\right)\to {p}\subseteq {P}$
18 7 17 syl ${⊢}\left({G}\in {𝒢}_{\mathrm{Tarski}}\wedge {p}\in \mathrm{ran}{L}\right)\to {p}\subseteq {P}$
19 18 ralrimiva ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to \forall {p}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}{p}\subseteq {P}$
20 unissb ${⊢}\bigcup \mathrm{ran}{L}\subseteq {P}↔\forall {p}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}{p}\subseteq {P}$
21 19 20 sylibr ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}\to \bigcup \mathrm{ran}{L}\subseteq {P}$