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	|- P = ( Base ` G )
	tglineintmo.i	|- I = ( Itv ` G )
	tglineintmo.l	|- L = ( LineG ` G )
	tglineintmo.g	|- ( ph -> G e. TarskiG )
	tglineintmo.a	|- ( ph -> A e. ran L )
	tglineintmo.b	|- ( ph -> B e. ran L )
	tglineintmo.c	|- ( ph -> A =/= B )
	tglineineq.x	|- ( ph -> X e. ( A i^i B ) )
	tglineineq.y	|- ( ph -> Y e. ( A i^i B ) )
Assertion	tglineineq	|- ( ph -> X = Y )

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		tglineintmo.a	|- ( ph -> A e. ran L )
6		tglineintmo.b	|- ( ph -> B e. ran L )
7		tglineintmo.c	|- ( ph -> A =/= B )
8		tglineineq.x	|- ( ph -> X e. ( A i^i B ) )
9		tglineineq.y	|- ( ph -> Y e. ( A i^i B ) )
10	1 2 3 4 5 6 7	tglineintmo	|- ( ph -> E* x ( x e. A /\ x e. B ) )
11		elin	|- ( X e. ( A i^i B ) <-> ( X e. A /\ X e. B ) )
12	8 11	sylib	|- ( ph -> ( X e. A /\ X e. B ) )
13		elin	|- ( Y e. ( A i^i B ) <-> ( Y e. A /\ Y e. B ) )
14	9 13	sylib	|- ( ph -> ( Y e. A /\ Y e. B ) )
15		eleq1	|- ( x = X -> ( x e. A <-> X e. A ) )
16		eleq1	|- ( x = X -> ( x e. B <-> X e. B ) )
17	15 16	anbi12d	|- ( x = X -> ( ( x e. A /\ x e. B ) <-> ( X e. A /\ X e. B ) ) )
18		eleq1	|- ( x = Y -> ( x e. A <-> Y e. A ) )
19		eleq1	|- ( x = Y -> ( x e. B <-> Y e. B ) )
20	18 19	anbi12d	|- ( x = Y -> ( ( x e. A /\ x e. B ) <-> ( Y e. A /\ Y e. B ) ) )
21	17 20	moi	|- ( ( ( X e. ( A i^i B ) /\ Y e. ( A i^i B ) ) /\ E* x ( x e. A /\ x e. B ) /\ ( ( X e. A /\ X e. B ) /\ ( Y e. A /\ Y e. B ) ) ) -> X = Y )
22	8 9 10 12 14 21	syl212anc	|- ( ph -> X = Y )