Theorem tglnpt 29018

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 29017	. . 3 ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃)
6	1, 5	syl 18	. 2 ⊢ (𝜑 → ∪ ran 𝐿 ⊆ 𝑃)
7		tglnpt.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
8		elssuni 4898	. . . 4 ⊢ (𝐴 ∈ ran 𝐿 → 𝐴 ⊆ ∪ ran 𝐿)
9	7, 8	syl 18	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ∪ ran 𝐿)
10		tglnpt.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
11	9, 10	sseldd 3909	. 2 ⊢ (𝜑 → 𝑋 ∈ ∪ ran 𝐿)
12	6, 11	sseldd 3909	1 ⊢ (𝜑 → 𝑋 ∈ 𝑃)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  ∪ cuni 4866  ran crn 5651  ‘cfv 6539  Basecbs 17393  TarskiGcstrkg 28895  Itvcitv 28901  LineGclng 28902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661  df-iota 6494  df-fv 6547  df-ov 7424  df-oprab 7425  df-mpo 7426  df-trkg 28921

This theorem is used by:  tglnpt3  29128  mirln  29154  mirln2  29155  symquadprlnglem  29171  perpcom  29194  perpneq  29195  ragperp  29198  foot  29203  footne  29204  footeq  29205  hlperpnel  29207  perprag  29208  perpdragALT  29209  perpdrag  29210  colperpexlem3  29214  oppne3  29225  oppcom  29226  oppnid  29228  opphllem1  29229  opphllem2  29230  opphllem3  29231  opphllem4  29232  opphllem5  29233  opphllem6  29234  oppperpex  29235  opphl  29236  oppmir  29238  outpasch  29239  lnopp2hpgb  29247  hpgerlem  29249  colopp  29253  colhp  29254  hlopp  29256  elplnglnid  29267  lnincplng  29268  plngrotlem1  29271  lnssplnglem  29275  plngmiropp  29278  nhpmirhp  29282  lmieu  29295  lmimid  29305  symquadmid  29310  lnperpex  29315  trgcopy  29317  trgcopyeulem  29318  perpeqlem  29353  perpeq  29354  tgaaddcpbllem1  29355  tgaaddcpbllem2  29356  tgaaddcpbllem3  29357  angmgmaddcpbl  29396  prlnghpg  29430  prlngpln3  29433  perpprlng  29434  prlngex  29435  prlngmolem1  29436  prlngmolem2  29437  prlngeq  29441  prlngplngtr  29443  prlngmid2  29445  symquadprlng  29446  quadcgrprlng  29450