Theorem tglnpt

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

	Ref	Expression
Hypotheses	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	tglnpt	|- ( ph -> X e. P )

Proof

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