Theorem tglineineq

Description: Two distinct lines intersect in at most one point, variation. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineintmo.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	tglineintmo.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
	tglineintmo.c	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	tglineineq.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
	tglineineq.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∩ 𝐵 ) )
Assertion	tglineineq	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglineintmo.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		tglineintmo.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
7		tglineintmo.c	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
8		tglineineq.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
9		tglineineq.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∩ 𝐵 ) )
10	1 2 3 4 5 6 7	tglineintmo	⊢ ( 𝜑 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
11		elin	⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) )
12	8 11	sylib	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) )
13		elin	⊢ ( 𝑌 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
14	9 13	sylib	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
15		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
16		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
17	15 16	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) )
18		eleq1	⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ 𝐴 ↔ 𝑌 ∈ 𝐴 ) )
19		eleq1	⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵 ) )
20	18 19	anbi12d	⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) )
21	17 20	moi	⊢ ( ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) ) → 𝑋 = 𝑌 )
22	8 9 10 12 14 21	syl212anc	⊢ ( 𝜑 → 𝑋 = 𝑌 )