lineintmo

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	lineintmo	$⊢ (A \in LinesEE \land B \in LinesEE \land A \neq B) \to \exists^{*} x (x \in A \land x \in B)$

Proof

Step	Hyp	Ref	Expression
1		an4	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \leftrightarrow ((x \in A \land y \in A) \land (x \in B \land y \in B))$
2		linethru	$⊢ (A \in LinesEE \land (x \in A \land y \in A) \land x \neq y) \to A = x Line y$
3	2	3expa	$⊢ ((A \in LinesEE \land (x \in A \land y \in A)) \land x \neq y) \to A = x Line y$
4		linethru	$⊢ (B \in LinesEE \land (x \in B \land y \in B) \land x \neq y) \to B = x Line y$
5	4	3expa	$⊢ ((B \in LinesEE \land (x \in B \land y \in B)) \land x \neq y) \to B = x Line y$
6		eqtr3	$⊢ (A = x Line y \land B = x Line y) \to A = B$
7	3 5 6	syl2an	$⊢ (((A \in LinesEE \land (x \in A \land y \in A)) \land x \neq y) \land ((B \in LinesEE \land (x \in B \land y \in B)) \land x \neq y)) \to A = B$
8	7	anandirs	$⊢ (((A \in LinesEE \land (x \in A \land y \in A)) \land (B \in LinesEE \land (x \in B \land y \in B))) \land x \neq y) \to A = B$
9	8	ex	$⊢ ((A \in LinesEE \land (x \in A \land y \in A)) \land (B \in LinesEE \land (x \in B \land y \in B))) \to (x \neq y \to A = B)$
10	9	necon1d	$⊢ ((A \in LinesEE \land (x \in A \land y \in A)) \land (B \in LinesEE \land (x \in B \land y \in B))) \to (A \neq B \to x = y)$
11	10	an4s	$⊢ ((A \in LinesEE \land B \in LinesEE) \land ((x \in A \land y \in A) \land (x \in B \land y \in B))) \to (A \neq B \to x = y)$
12	1 11	sylan2b	$⊢ ((A \in LinesEE \land B \in LinesEE) \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to (A \neq B \to x = y)$
13	12	ex	$⊢ (A \in LinesEE \land B \in LinesEE) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to (A \neq B \to x = y))$
14	13	com23	$⊢ (A \in LinesEE \land B \in LinesEE) \to (A \neq B \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y))$
15	14	3impia	$⊢ (A \in LinesEE \land B \in LinesEE \land A \neq B) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y)$
16	15	alrimivv	$⊢ (A \in LinesEE \land B \in LinesEE \land A \neq B) \to \forall x \forall y (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x = y)$
17		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
18		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
19	17 18	anbi12d	$⊢ x = y \to ((x \in A \land x \in B) \leftrightarrow (y \in A \land y \in B))$
20	19	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)$
21	16 20	sylibr	$⊢ (A \in LinesEE \land B \in LinesEE \land A \neq B) \to \exists^{*} x (x \in A \land x \in B)$

Metamath Proof Explorer

Theorem lineintmo

Proof