Theorem tglineinsn

Description: If two distinct lines intersect, it is at a single point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	tglineintmo.p	|- P = ( Base ` G )
	tglineintmo.i	|- I = ( Itv ` G )
	tglineintmo.l	|- L = ( LineG ` G )
	tglineintmo.g	|- ( ph -> G e. TarskiG )
	tglineinsn.a	|- ( ph -> A e. ran L )
	tglineinsn.b	|- ( ph -> B e. ran L )
	tglineinsn.c	|- ( ph -> A =/= B )
	tglineinsn.x	|- ( ph -> X e. ( A i^i B ) )
Assertion	tglineinsn	|- ( ph -> ( A i^i B ) = { X } )

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	|- P = ( Base ` G )
2		tglineintmo.i	|- I = ( Itv ` G )
3		tglineintmo.l	|- L = ( LineG ` G )
4		tglineintmo.g	|- ( ph -> G e. TarskiG )
5		tglineinsn.a	|- ( ph -> A e. ran L )
6		tglineinsn.b	|- ( ph -> B e. ran L )
7		tglineinsn.c	|- ( ph -> A =/= B )
8		tglineinsn.x	|- ( ph -> X e. ( A i^i B ) )
9	4	adantr	|- ( ( ph /\ x e. ( A i^i B ) ) -> G e. TarskiG )
10	5	adantr	|- ( ( ph /\ x e. ( A i^i B ) ) -> A e. ran L )
11	6	adantr	|- ( ( ph /\ x e. ( A i^i B ) ) -> B e. ran L )
12	7	adantr	|- ( ( ph /\ x e. ( A i^i B ) ) -> A =/= B )
13		simpr	|- ( ( ph /\ x e. ( A i^i B ) ) -> x e. ( A i^i B ) )
14	8	adantr	|- ( ( ph /\ x e. ( A i^i B ) ) -> X e. ( A i^i B ) )
15	1 2 3 9 10 11 12 13 14	tglineineq	|- ( ( ph /\ x e. ( A i^i B ) ) -> x = X )
16	15 8	eqsnd	|- ( ph -> ( A i^i B ) = { X } )