Metamath Proof Explorer


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=BaseG
tglineelsb2.i I=ItvG
tglineelsb2.l L=Line𝒢G
tglineelsb2.g φG𝒢Tarski
tgelrnln.x φXB
tgelrnln.y φYB
tgelrnln.d φXY
Assertion tgelrnln φXLYranL

Proof

Step Hyp Ref Expression
1 tglineelsb2.p B=BaseG
2 tglineelsb2.i I=ItvG
3 tglineelsb2.l L=Line𝒢G
4 tglineelsb2.g φG𝒢Tarski
5 tgelrnln.x φXB
6 tgelrnln.y φYB
7 tgelrnln.d φXY
8 df-ov XLY=LXY
9 1 3 2 tglnfn G𝒢TarskiLFnB×BI
10 4 9 syl φLFnB×BI
11 5 6 opelxpd φXYB×B
12 df-br XIYXYI
13 ideqg YBXIYX=Y
14 12 13 bitr3id YBXYIX=Y
15 14 necon3bbid YB¬XYIXY
16 15 biimpar YBXY¬XYI
17 6 7 16 syl2anc φ¬XYI
18 11 17 eldifd φXYB×BI
19 fnfvelrn LFnB×BIXYB×BILXYranL
20 10 18 19 syl2anc φLXYranL
21 8 20 eqeltrid φXLYranL