Theorem tgelrnln 27281

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

Hypotheses

Ref	Expression
tglineelsb2.p	⊢ 𝐵 = (Base‘𝐺)
tglineelsb2.i	⊢ 𝐼 = (Itv‘𝐺)
tglineelsb2.l	⊢ 𝐿 = (LineG‘𝐺)
tglineelsb2.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgelrnln.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
tgelrnln.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
tgelrnln.d	⊢ (𝜑 → 𝑋 ≠ 𝑌)

Assertion

Ref	Expression
tgelrnln	⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)

Proof of Theorem tgelrnln

Step	Hyp	Ref	Expression
1		df-ov 7341	. 2 ⊢ (𝑋𝐿𝑌) = (𝐿‘⟨𝑋, 𝑌⟩)
2		tglineelsb2.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
3		tglineelsb2.p	. . . . 5 ⊢ 𝐵 = (Base‘𝐺)
4		tglineelsb2.l	. . . . 5 ⊢ 𝐿 = (LineG‘𝐺)
5		tglineelsb2.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
6	3, 4, 5	tglnfn 27198	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
7	2, 6	syl 17	. . 3 ⊢ (𝜑 → 𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
8		tgelrnln.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
9		tgelrnln.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
10	8, 9	opelxpd 5659	. . . 4 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
11		tgelrnln.d	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
12		df-br 5094	. . . . . . . 8 ⊢ (𝑋 I 𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ I )
13		ideqg 5794	. . . . . . . 8 ⊢ (𝑌 ∈ 𝐵 → (𝑋 I 𝑌 ↔ 𝑋 = 𝑌))
14	12, 13	bitr3id 284	. . . . . . 7 ⊢ (𝑌 ∈ 𝐵 → (⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋 = 𝑌))
15	14	necon3bbid 2978	. . . . . 6 ⊢ (𝑌 ∈ 𝐵 → (¬ ⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋 ≠ 𝑌))
16	15	biimpar 478	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
17	9, 11, 16	syl2anc 584	. . . 4 ⊢ (𝜑 → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
18	10, 17	eldifd 3909	. . 3 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I ))
19		fnfvelrn 7015	. . 3 ⊢ ((𝐿 Fn ((𝐵 × 𝐵) ∖ I ) ∧ ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I )) → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
20	7, 18, 19	syl2anc 584	. 2 ⊢ (𝜑 → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
21	1, 20	eqeltrid 2841	1 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2105   ≠ wne 2940   ∖ cdif 3895  ⟨cop 4580   class class class wbr 5093   I cid 5518   × cxp 5619  ran crn 5622   Fn wfn 6475  ‘cfv 6480  (class class class)co 7338  Basecbs 17010  TarskiGcstrkg 27078  Itvcitv 27084  LineGclng 27085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pr 5373  ax-un 7651

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-fv 6488  df-ov 7341  df-oprab 7342  df-mpo 7343  df-1st 7900  df-2nd 7901  df-trkg 27104

This theorem is referenced by:  tghilberti1  27288  tglineinteq  27296  colline  27300  tglowdim2ln  27302  footexALT  27369  footexlem2  27371  foot  27373  perprag  27377  colperpexlem3  27383  mideulem2  27385  midex  27388  outpasch  27406  lnopp2hpgb  27414  colopp  27420  lmieu  27435  lmimid  27445  hypcgrlem1  27450  hypcgrlem2  27451  lnperpex  27454  trgcopy  27455  trgcopyeulem  27456  acopy  27484  acopyeu  27485  tgasa1  27509