Theorem tgelrnln

Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	|- B = ( Base ` G )
	tglineelsb2.i	|- I = ( Itv ` G )
	tglineelsb2.l	|- L = ( LineG ` G )
	tglineelsb2.g	|- ( ph -> G e. TarskiG )
	tgelrnln.x	|- ( ph -> X e. B )
	tgelrnln.y	|- ( ph -> Y e. B )
	tgelrnln.d	|- ( ph -> X =/= Y )
Assertion	tgelrnln	|- ( ph -> ( X L Y ) e. ran L )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	|- B = ( Base ` G )
2		tglineelsb2.i	|- I = ( Itv ` G )
3		tglineelsb2.l	|- L = ( LineG ` G )
4		tglineelsb2.g	|- ( ph -> G e. TarskiG )
5		tgelrnln.x	|- ( ph -> X e. B )
6		tgelrnln.y	|- ( ph -> Y e. B )
7		tgelrnln.d	|- ( ph -> X =/= Y )
8		df-ov	|- ( X L Y ) = ( L ` <. X , Y >. )
9	1 3 2	tglnfn	|- ( G e. TarskiG -> L Fn ( ( B X. B ) \ _I ) )
10	4 9	syl	|- ( ph -> L Fn ( ( B X. B ) \ _I ) )
11	5 6	opelxpd	|- ( ph -> <. X , Y >. e. ( B X. B ) )
12		df-br	|- ( X _I Y <-> <. X , Y >. e. _I )
13		ideqg	|- ( Y e. B -> ( X _I Y <-> X = Y ) )
14	12 13	bitr3id	|- ( Y e. B -> ( <. X , Y >. e. _I <-> X = Y ) )
15	14	necon3bbid	|- ( Y e. B -> ( -. <. X , Y >. e. _I <-> X =/= Y ) )
16	15	biimpar	|- ( ( Y e. B /\ X =/= Y ) -> -. <. X , Y >. e. _I )
17	6 7 16	syl2anc	|- ( ph -> -. <. X , Y >. e. _I )
18	11 17	eldifd	|- ( ph -> <. X , Y >. e. ( ( B X. B ) \ _I ) )
19		fnfvelrn	|- ( ( L Fn ( ( B X. B ) \ _I ) /\ <. X , Y >. e. ( ( B X. B ) \ _I ) ) -> ( L ` <. X , Y >. ) e. ran L )
20	10 18 19	syl2anc	|- ( ph -> ( L ` <. X , Y >. ) e. ran L )
21	8 20	eqeltrid	|- ( ph -> ( X L Y ) e. ran L )