hilbert1.2

Description: There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by NM, 17-Jun-2017)

		Ref	Expression
	Assertion	hilbert1.2	$⊢ P \neq Q \to \exists^{*} x \in LinesEE (P \in x \land Q \in x)$

Proof

Step	Hyp	Ref	Expression
1		an4	$⊢ ((x \in LinesEE \land y \in LinesEE) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \leftrightarrow ((x \in LinesEE \land (P \in x \land Q \in x)) \land (y \in LinesEE \land (P \in y \land Q \in y)))$
2		simprl	$⊢ (P \neq Q \land (x \in LinesEE \land (P \in x \land Q \in x))) \to x \in LinesEE$
3		simprr	$⊢ (P \neq Q \land (x \in LinesEE \land (P \in x \land Q \in x))) \to (P \in x \land Q \in x)$
4		simpl	$⊢ (P \neq Q \land (x \in LinesEE \land (P \in x \land Q \in x))) \to P \neq Q$
5		linethru	$⊢ (x \in LinesEE \land (P \in x \land Q \in x) \land P \neq Q) \to x = P Line Q$
6	2 3 4 5	syl3anc	$⊢ (P \neq Q \land (x \in LinesEE \land (P \in x \land Q \in x))) \to x = P Line Q$
7	6	ex	$⊢ P \neq Q \to ((x \in LinesEE \land (P \in x \land Q \in x)) \to x = P Line Q)$
8		simprl	$⊢ (P \neq Q \land (y \in LinesEE \land (P \in y \land Q \in y))) \to y \in LinesEE$
9		simprr	$⊢ (P \neq Q \land (y \in LinesEE \land (P \in y \land Q \in y))) \to (P \in y \land Q \in y)$
10		simpl	$⊢ (P \neq Q \land (y \in LinesEE \land (P \in y \land Q \in y))) \to P \neq Q$
11		linethru	$⊢ (y \in LinesEE \land (P \in y \land Q \in y) \land P \neq Q) \to y = P Line Q$
12	8 9 10 11	syl3anc	$⊢ (P \neq Q \land (y \in LinesEE \land (P \in y \land Q \in y))) \to y = P Line Q$
13	12	ex	$⊢ P \neq Q \to ((y \in LinesEE \land (P \in y \land Q \in y)) \to y = P Line Q)$
14	7 13	anim12d	$⊢ P \neq Q \to (((x \in LinesEE \land (P \in x \land Q \in x)) \land (y \in LinesEE \land (P \in y \land Q \in y))) \to (x = P Line Q \land y = P Line Q))$
15		eqtr3	$⊢ (x = P Line Q \land y = P Line Q) \to x = y$
16	14 15	syl6	$⊢ P \neq Q \to (((x \in LinesEE \land (P \in x \land Q \in x)) \land (y \in LinesEE \land (P \in y \land Q \in y))) \to x = y)$
17	1 16	syl5bi	$⊢ P \neq Q \to (((x \in LinesEE \land y \in LinesEE) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to x = y)$
18	17	expd	$⊢ P \neq Q \to ((x \in LinesEE \land y \in LinesEE) \to (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y))$
19	18	ralrimivv	$⊢ P \neq Q \to \forall x \in LinesEE \forall y \in LinesEE (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y)$
20		eleq2w	$⊢ x = y \to (P \in x \leftrightarrow P \in y)$
21		eleq2w	$⊢ x = y \to (Q \in x \leftrightarrow Q \in y)$
22	20 21	anbi12d	$⊢ x = y \to ((P \in x \land Q \in x) \leftrightarrow (P \in y \land Q \in y))$
23	22	rmo4	$⊢ \exists^{*} x \in LinesEE (P \in x \land Q \in x) \leftrightarrow \forall x \in LinesEE \forall y \in LinesEE (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y)$
24	19 23	sylibr	$⊢ P \neq Q \to \exists^{*} x \in LinesEE (P \in x \land Q \in x)$

Metamath Proof Explorer

Theorem hilbert1.2

Proof