Theorem tglnpt 28899

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 28898	. . 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 3935	. 2 ⊢ (𝜑 → 𝑋 ∈ ∪ ran 𝐿)
12	6, 11	sseldd 3935	1 ⊢ (𝜑 → 𝑋 ∈ 𝑃)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902  ∪ cuni 4870  ran crn 5660  ‘cfv 6537  Basecbs 17307  TarskiGcstrkg 28776  Itvcitv 28782  LineGclng 28783

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670  df-iota 6493  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-trkg 28802

This theorem is used by:  tglnpt3  29009  mirln  29035  mirln2  29036  symquadprlnglem  29052  perpcom  29075  perpneq  29076  ragperp  29079  foot  29084  footne  29085  footeq  29086  hlperpnel  29088  perprag  29089  perpdragALT  29090  perpdrag  29091  colperpexlem3  29095  oppne3  29106  oppcom  29107  oppnid  29109  opphllem1  29110  opphllem2  29111  opphllem3  29112  opphllem4  29113  opphllem5  29114  opphllem6  29115  oppperpex  29116  opphl  29117  oppmir  29119  outpasch  29120  lnopp2hpgb  29128  hpgerlem  29130  colopp  29134  colhp  29135  hlopp  29137  elplnglnid  29148  lnincplng  29149  plngrotlem1  29152  lnssplnglem  29156  plngmiropp  29159  nhpmirhp  29163  lmieu  29176  lmimid  29186  symquadmid  29191  lnperpex  29196  trgcopy  29198  trgcopyeulem  29199  perpeqlem  29234  perpeq  29235  tgaaddcpbllem1  29236  tgaaddcpbllem2  29237  tgaaddcpbllem3  29238  angmgmaddcpbl  29277  prlnghpg  29311  prlngpln3  29314  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlngeq  29322  prlngplngtr  29324  prlngmid2  29326  symquadprlng  29327  quadcgrprlng  29331