Theorem tglngne

Description: It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglngval.p	|- P = ( Base ` G )
	tglngval.l	|- L = ( LineG ` G )
	tglngval.i	|- I = ( Itv ` G )
	tglngval.g	|- ( ph -> G e. TarskiG )
	tglngval.x	|- ( ph -> X e. P )
	tglngval.y	|- ( ph -> Y e. P )
	tglngne.1	|- ( ph -> Z e. ( X L Y ) )
Assertion	tglngne	|- ( ph -> X =/= Y )

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	|- P = ( Base ` G )
2		tglngval.l	|- L = ( LineG ` G )
3		tglngval.i	|- I = ( Itv ` G )
4		tglngval.g	|- ( ph -> G e. TarskiG )
5		tglngval.x	|- ( ph -> X e. P )
6		tglngval.y	|- ( ph -> Y e. P )
7		tglngne.1	|- ( ph -> Z e. ( X L Y ) )
8		df-ov	|- ( X L Y ) = ( L ` <. X , Y >. )
9	7 8	eleqtrdi	|- ( ph -> Z e. ( L ` <. X , Y >. ) )
10		elfvdm	|- ( Z e. ( L ` <. X , Y >. ) -> <. X , Y >. e. dom L )
11	9 10	syl	|- ( ph -> <. X , Y >. e. dom L )
12	1 2 3	tglnfn	|- ( G e. TarskiG -> L Fn ( ( P X. P ) \ _I ) )
13		fndm	|- ( L Fn ( ( P X. P ) \ _I ) -> dom L = ( ( P X. P ) \ _I ) )
14	4 12 13	3syl	|- ( ph -> dom L = ( ( P X. P ) \ _I ) )
15	11 14	eleqtrd	|- ( ph -> <. X , Y >. e. ( ( P X. P ) \ _I ) )
16	15	eldifbd	|- ( ph -> -. <. X , Y >. e. _I )
17		df-br	|- ( X _I Y <-> <. X , Y >. e. _I )
18		ideqg	|- ( Y e. P -> ( X _I Y <-> X = Y ) )
19	6 18	syl	|- ( ph -> ( X _I Y <-> X = Y ) )
20	17 19	bitr3id	|- ( ph -> ( <. X , Y >. e. _I <-> X = Y ) )
21	20	necon3bbid	|- ( ph -> ( -. <. X , Y >. e. _I <-> X =/= Y ) )
22	16 21	mpbid	|- ( ph -> X =/= Y )