Metamath Proof Explorer

Theorem 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 ( 𝑃 ≠ 𝑄 → ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( 𝑥 ∈ LinesEE ∧ 𝑦 ∈ LinesEE ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) )
2 simprl ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ) → 𝑥 ∈ LinesEE )
3 simprr ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ) → ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
4 simpl ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ) → 𝑃 ≠ 𝑄 )
5 linethru ⊢ ( ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑥 = ( 𝑃 Line 𝑄 ) )
6 2 3 4 5 syl3anc ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ) → 𝑥 = ( 𝑃 Line 𝑄 ) )
7 6 ex ⊢ ( 𝑃 ≠ 𝑄 → ( ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) → 𝑥 = ( 𝑃 Line 𝑄 ) ) )
8 simprl ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑦 ∈ LinesEE )
9 simprr ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) )
10 simpl ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑃 ≠ 𝑄 )
11 linethru ⊢ ( ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑦 = ( 𝑃 Line 𝑄 ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑦 = ( 𝑃 Line 𝑄 ) )
13 12 ex ⊢ ( 𝑃 ≠ 𝑄 → ( ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑦 = ( 𝑃 Line 𝑄 ) ) )
14 7 13 anim12d ⊢ ( 𝑃 ≠ 𝑄 → ( ( ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → ( 𝑥 = ( 𝑃 Line 𝑄 ) ∧ 𝑦 = ( 𝑃 Line 𝑄 ) ) ) )
15 eqtr3 ⊢ ( ( 𝑥 = ( 𝑃 Line 𝑄 ) ∧ 𝑦 = ( 𝑃 Line 𝑄 ) ) → 𝑥 = 𝑦 )
16 14 15 syl6 ⊢ ( 𝑃 ≠ 𝑄 → ( ( ( 𝑥 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) ∧ ( 𝑦 ∈ LinesEE ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
17 1 16 syl5bi ⊢ ( 𝑃 ≠ 𝑄 → ( ( ( 𝑥 ∈ LinesEE ∧ 𝑦 ∈ LinesEE ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
18 17 expd ⊢ ( 𝑃 ≠ 𝑄 → ( ( 𝑥 ∈ LinesEE ∧ 𝑦 ∈ LinesEE ) → ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
19 18 ralrimivv ⊢ ( 𝑃 ≠ 𝑄 → ∀ 𝑥 ∈ LinesEE ∀ 𝑦 ∈ LinesEE ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) )
20 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦 ) )
21 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝑄 ∈ 𝑥 ↔ 𝑄 ∈ 𝑦 ) )
22 20 21 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) )
23 22 rmo4 ⊢ ( ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ LinesEE ∀ 𝑦 ∈ LinesEE ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) )
24 19 23 sylibr ⊢ ( 𝑃 ≠ 𝑄 → ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )