Theorem tglnpt 25444

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

Hypotheses

Ref	Expression
tglng.p	|- P = ( Base ` G )
tglng.l	|- L = (LineG ` G )
tglng.i	|- I = (Itv ` G )
tglnpt.g	|- ( ph -> G e. TarskiG )
tglnpt.a	|- ( ph -> A e. ran L )
tglnpt.x	|- ( ph -> X e. A )

Assertion

Ref	Expression
tglnpt	|- ( ph -> X e. P )

Proof of Theorem tglnpt

Step	Hyp	Ref	Expression
1		tglnpt.g	. . 3 |- ( ph -> G e. TarskiG )
2		tglng.p	. . . 4 |- P = ( Base ` G )
3		tglng.l	. . . 4 |- L = (LineG ` G )
4		tglng.i	. . . 4 |- I = (Itv ` G )
5	2, 3, 4	tglnunirn 25443	. . 3 |- ( G e. TarskiG -> U. ran L C_ P )
6	1, 5	syl 17	. 2 |- ( ph -> U. ran L C_ P )
7		tglnpt.a	. . . 4 |- ( ph -> A e. ran L )
8		elssuni 4467	. . . 4 |- ( A e. ran L -> A C_ U. ran L )
9	7, 8	syl 17	. . 3 |- ( ph -> A C_ U. ran L )
10		tglnpt.x	. . 3 |- ( ph -> X e. A )
11	9, 10	sseldd 3604	. 2 |- ( ph -> X e. U. ran L )
12	6, 11	sseldd 3604	1 |- ( ph -> X e. P )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   C_ wss 3574   U.cuni 4436   ran crn 5115   ` cfv 5888   Basecbs 15857  TarskiGcstrkg 25329  Itvcitv 25335  LineGclng 25336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125  df-iota 5851  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-trkg 25352

This theorem is referenced by:  mirln  25571  mirln2  25572  perpcom  25608  perpneq  25609  ragperp  25612  foot  25614  footne  25615  footeq  25616  hlperpnel  25617  perprag  25618  perpdragALT  25619  perpdrag  25620  colperpexlem3  25624  oppne3  25635  oppcom  25636  oppnid  25638  opphllem1  25639  opphllem2  25640  opphllem3  25641  opphllem4  25642  opphllem5  25643  opphllem6  25644  oppperpex  25645  opphl  25646  outpasch  25647  lnopp2hpgb  25655  hpgerlem  25657  colopp  25661  colhp  25662  lmieu  25676  lmimid  25686  lnperpex  25695  trgcopy  25696  trgcopyeulem  25697