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	$⊢ P = {Base}_{G}$
	tglineintmo.i	$⊢ I = Itv (G)$
	tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineintmo.a	$⊢ φ \to A \in ran L$
	tglineintmo.b	$⊢ φ \to B \in ran L$
	tglineintmo.c	$⊢ φ \to A \neq B$
Assertion	tglineintmo	$⊢ φ \to \exists^{*} x (x \in A \land x \in B)$

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	$⊢ P = {Base}_{G}$
2		tglineintmo.i	$⊢ I = Itv (G)$
3		tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineintmo.a	$⊢ φ \to A \in ran L$
6		tglineintmo.b	$⊢ φ \to B \in ran L$
7		tglineintmo.c	$⊢ φ \to A \neq B$
8	4	ad2antrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to G \in 𝒢_{Tarski}$
9		elssuni	$⊢ A \in ran L \to A \subseteq ⋃ ran L$
10	5 9	syl	$⊢ φ \to A \subseteq ⋃ ran L$
11	1 3 2	tglnunirn	$⊢ G \in 𝒢_{Tarski} \to ⋃ ran L \subseteq P$
12	4 11	syl	$⊢ φ \to ⋃ ran L \subseteq P$
13	10 12	sstrd	$⊢ φ \to A \subseteq P$
14	13	ad2antrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to A \subseteq P$
15		simplrl	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to (x \in A \land x \in B)$
16	15	simpld	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to x \in A$
17	14 16	sseldd	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to x \in P$
18		simplrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to (y \in A \land y \in B)$
19	18	simpld	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to y \in A$
20	14 19	sseldd	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to y \in P$
21		simpr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to x \neq y$
22	5	ad2antrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to A \in ran L$
23	1 2 3 8 17 20 21 21 22 16 19	tglinethru	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to A = x L y$
24	6	ad2antrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to B \in ran L$
25	15	simprd	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to x \in B$
26	18	simprd	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to y \in B$
27	1 2 3 8 17 20 21 21 24 25 26	tglinethru	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to B = x L y$
28	23 27	eqtr4d	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to A = B$
29	7	ad2antrr	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to A \neq B$
30	29	neneqd	$⊢ ((φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \land x \neq y) \to \neg A = B$
31	28 30	pm2.65da	$⊢ (φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to \neg x \neq y$
32		nne	$⊢ \neg x \neq y \leftrightarrow x = y$
33	31 32	sylib	$⊢ (φ \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to x = y$
34	33	ex	$⊢ φ \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y)$
35	34	alrimivv	$⊢ φ \to \forall x \forall y (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y)$
36		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
37		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
38	36 37	anbi12d	$⊢ x = y \to ((x \in A \land x \in B) \leftrightarrow (y \in A \land y \in B))$
39	38	mo4	$⊢ \exists^{*} x (x \in A \land x \in B) \leftrightarrow \forall x \forall y (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y)$
40	35 39	sylibr	$⊢ φ \to \exists^{*} x (x \in A \land x \in B)$

Metamath Proof Explorer

Theorem tglineintmo

Proof