Theorem tglnpt 29045

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ∪ cuni 4870  ran crn 5657  ‘cfv 6561  Basecbs 17419  TarskiGcstrkg 28922  Itvcitv 28928  LineGclng 28929

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-cnv 5664  df-dm 5666  df-rn 5667  df-iota 6515  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451  df-trkg 28948

This theorem is used by:  tglnpt3  29155  mirln  29181  mirln2  29182  symquadprlnglem  29198  perpcom  29221  perpneq  29222  ragperp  29225  foot  29230  footne  29231  footeq  29232  hlperpnel  29234  perprag  29235  perpdragALT  29236  perpdrag  29237  colperpexlem3  29241  oppne3  29252  oppcom  29253  oppnid  29255  opphllem1  29256  opphllem2  29257  opphllem3  29258  opphllem4  29259  opphllem5  29260  opphllem6  29261  oppperpex  29262  opphl  29263  oppmir  29265  outpasch  29266  lnopp2hpgb  29274  hpgerlem  29276  colopp  29280  colhp  29281  hlopp  29283  elplnglnid  29294  lnincplng  29295  plngrotlem1  29298  lnssplnglem  29302  plngmiropp  29305  nhpmirhp  29309  lmieu  29322  lmimid  29332  symquadmid  29337  lnperpex  29342  trgcopy  29344  trgcopyeulem  29345  perpeqlem  29380  perpeq  29381  tgaaddcpbllem1  29382  tgaaddcpbllem2  29383  tgaaddcpbllem3  29384  angmgmaddcpbl  29423  prlnghpg  29457  prlngpln3  29460  perpprlng  29461  prlngex  29462  prlngmolem1  29463  prlngmolem2  29464  prlngeq  29468  prlngplngtr  29470  prlngmid2  29472  symquadprlng  29473  quadcgrprlng  29477