hilbert1.1

Description: There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	hilbert1.1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists x \in LinesEE (P \in x \land Q \in x)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \to P \in 𝔼 (N)$
2		simp2	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \to Q \in 𝔼 (N)$
3		simp3	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \to P \neq Q$
4		eqidd	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \to P Line Q = P Line Q$
5		neeq1	$⊢ p = P \to (p \neq q \leftrightarrow P \neq q)$
6		oveq1	$⊢ p = P \to p Line q = P Line q$
7	6	eqeq2d	$⊢ p = P \to (P Line Q = p Line q \leftrightarrow P Line Q = P Line q)$
8	5 7	anbi12d	$⊢ p = P \to ((p \neq q \land P Line Q = p Line q) \leftrightarrow (P \neq q \land P Line Q = P Line q))$
9		neeq2	$⊢ q = Q \to (P \neq q \leftrightarrow P \neq Q)$
10		oveq2	$⊢ q = Q \to P Line q = P Line Q$
11	10	eqeq2d	$⊢ q = Q \to (P Line Q = P Line q \leftrightarrow P Line Q = P Line Q)$
12	9 11	anbi12d	$⊢ q = Q \to ((P \neq q \land P Line Q = P Line q) \leftrightarrow (P \neq Q \land P Line Q = P Line Q))$
13	8 12	rspc2ev	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land (P \neq Q \land P Line Q = P Line Q)) \to \exists p \in 𝔼 (N) \exists q \in 𝔼 (N) (p \neq q \land P Line Q = p Line q)$
14	1 2 3 4 13	syl112anc	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \to \exists p \in 𝔼 (N) \exists q \in 𝔼 (N) (p \neq q \land P Line Q = p Line q)$
15		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
16	15	rexeqdv	$⊢ n = N \to (\exists q \in 𝔼 (n) (p \neq q \land P Line Q = p Line q) \leftrightarrow \exists q \in 𝔼 (N) (p \neq q \land P Line Q = p Line q))$
17	15 16	rexeqbidv	$⊢ n = N \to (\exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land P Line Q = p Line q) \leftrightarrow \exists p \in 𝔼 (N) \exists q \in 𝔼 (N) (p \neq q \land P Line Q = p Line q))$
18	17	rspcev	$⊢ (N \in ℕ \land \exists p \in 𝔼 (N) \exists q \in 𝔼 (N) (p \neq q \land P Line Q = p Line q)) \to \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land P Line Q = p Line q)$
19	14 18	sylan2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land P Line Q = p Line q)$
20		ellines	$⊢ P Line Q \in LinesEE \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land P Line Q = p Line q)$
21	19 20	sylibr	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q \in LinesEE$
22		linerflx1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \in (P Line Q)$
23		linerflx2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to Q \in (P Line Q)$
24		eleq2	$⊢ x = P Line Q \to (P \in x \leftrightarrow P \in (P Line Q))$
25		eleq2	$⊢ x = P Line Q \to (Q \in x \leftrightarrow Q \in (P Line Q))$
26	24 25	anbi12d	$⊢ x = P Line Q \to ((P \in x \land Q \in x) \leftrightarrow (P \in (P Line Q) \land Q \in (P Line Q)))$
27	26	rspcev	$⊢ (P Line Q \in LinesEE \land (P \in (P Line Q) \land Q \in (P Line Q))) \to \exists x \in LinesEE (P \in x \land Q \in x)$
28	21 22 23 27	syl12anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists x \in LinesEE (P \in x \land Q \in x)$

Metamath Proof Explorer

Theorem hilbert1.1

Proof