Theorem tglineintmo

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

	Ref	Expression
Hypotheses	tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineintmo.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	tglineintmo.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
	tglineintmo.c	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	tglineintmo	⊢ ( 𝜑 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )

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	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐺 ∈ TarskiG )
9		elssuni	⊢ ( 𝐴 ∈ ran 𝐿 → 𝐴 ⊆ ∪ ran 𝐿 )
10	5 9	syl	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran 𝐿 )
11	1 3 2	tglnunirn	⊢ ( 𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃 )
12	4 11	syl	⊢ ( 𝜑 → ∪ ran 𝐿 ⊆ 𝑃 )
13	10 12	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ 𝑃 )
14	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 ⊆ 𝑃 )
15		simplrl	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
16	15	simpld	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐴 )
17	14 16	sseldd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝑃 )
18		simplrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
19	18	simpld	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐴 )
20	14 19	sseldd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝑃 )
21		simpr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
22	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 ∈ ran 𝐿 )
23	1 2 3 8 17 20 21 21 22 16 19	tglinethru	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
24	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 ∈ ran 𝐿 )
25	15	simprd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐵 )
26	18	simprd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐵 )
27	1 2 3 8 17 20 21 21 24 25 26	tglinethru	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
28	23 27	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = 𝐵 )
29	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 ≠ 𝐵 )
30	29	neneqd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ 𝐴 = 𝐵 )
31	28 30	pm2.65da	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → ¬ 𝑥 ≠ 𝑦 )
32		nne	⊢ ( ¬ 𝑥 ≠ 𝑦 ↔ 𝑥 = 𝑦 )
33	31 32	sylib	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → 𝑥 = 𝑦 )
34	33	ex	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
35	34	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
36		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
37		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
38	36 37	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
39	38	mo4	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
40	35 39	sylibr	⊢ ( 𝜑 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )