Theorem tglnpt 28994

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

Hypotheses

Ref	Expression
tglng.p	⊢ 𝑃 = (Base‘𝐺)
tglng.l	⊢ 𝐿 = (LineG‘𝐺)
tglng.i	⊢ 𝐼 = (Itv‘𝐺)
tglnpt.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tglnpt.a	⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
tglnpt.x	⊢ (𝜑 → 𝑋 ∈ 𝐴)

Assertion

Ref	Expression
tglnpt	⊢ (𝜑 → 𝑋 ∈ 𝑃)

Proof of Theorem tglnpt

Step	Hyp	Ref	Expression
1		tglnpt.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
2		tglng.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
3		tglng.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
4		tglng.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
5	2, 3, 4	tglnunirn 28993	. . 3 ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃)
6	1, 5	syl 18	. 2 ⊢ (𝜑 → ∪ ran 𝐿 ⊆ 𝑃)
7		tglnpt.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
8		elssuni 4899	. . . 4 ⊢ (𝐴 ∈ ran 𝐿 → 𝐴 ⊆ ∪ ran 𝐿)
9	7, 8	syl 18	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ∪ ran 𝐿)
10		tglnpt.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
11	9, 10	sseldd 3932	. 2 ⊢ (𝜑 → 𝑋 ∈ ∪ ran 𝐿)
12	6, 11	sseldd 3932	1 ⊢ (𝜑 → 𝑋 ∈ 𝑃)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867  ran crn 5652  ‘cfv 6531  Basecbs 17367  TarskiGcstrkg 28871  Itvcitv 28877  LineGclng 28878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662  df-iota 6487  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-trkg 28897

This theorem is used by:  tglnpt3  29104  mirln  29130  mirln2  29131  symquadprlnglem  29147  perpcom  29170  perpneq  29171  ragperp  29174  foot  29179  footne  29180  footeq  29181  hlperpnel  29183  perprag  29184  perpdragALT  29185  perpdrag  29186  colperpexlem3  29190  oppne3  29201  oppcom  29202  oppnid  29204  opphllem1  29205  opphllem2  29206  opphllem3  29207  opphllem4  29208  opphllem5  29209  opphllem6  29210  oppperpex  29211  opphl  29212  oppmir  29214  outpasch  29215  lnopp2hpgb  29223  hpgerlem  29225  colopp  29229  colhp  29230  hlopp  29232  elplnglnid  29243  lnincplng  29244  plngrotlem1  29247  lnssplnglem  29251  plngmiropp  29254  nhpmirhp  29258  lmieu  29271  lmimid  29281  symquadmid  29286  lnperpex  29291  trgcopy  29293  trgcopyeulem  29294  perpeqlem  29329  perpeq  29330  tgaaddcpbllem1  29331  tgaaddcpbllem2  29332  tgaaddcpbllem3  29333  angmgmaddcpbl  29372  prlnghpg  29406  prlngpln3  29409  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  prlngeq  29417  prlngplngtr  29419  prlngmid2  29421  symquadprlng  29422  quadcgrprlng  29426