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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgelrnln.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	tgelrnln.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	tgelrnln.d	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion	tgelrnln	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )

Proof

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