Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
2 simp2 ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3 ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
4 eqidd ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑄 ) )
5 neeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≠ 𝑞 ↔ 𝑃 ≠ 𝑞 ) )
6 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 Line 𝑞 ) = ( 𝑃 Line 𝑞 ) )
7 6 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ↔ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑞 ) ) )
8 5 7 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ↔ ( 𝑃 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑞 ) ) ) )
9 neeq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑃 ≠ 𝑞 ↔ 𝑃 ≠ 𝑄 ) )
10 oveq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑃 Line 𝑞 ) = ( 𝑃 Line 𝑄 ) )
11 10 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑞 ) ↔ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑄 ) ) )
12 9 11 anbi12d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑃 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑞 ) ) ↔ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑄 ) ) ) )
13 8 12 rspc2ev ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑃 Line 𝑄 ) ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) )
14 1 2 3 4 13 syl112anc ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) )
15 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
16 15 rexeqdv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ) )
17 15 16 rexeqbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ) )
18 17 rspcev ⊢ ( ( 𝑁 ∈ ℕ ∧ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) )
19 14 18 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) )
20 ellines ⊢ ( ( 𝑃 Line 𝑄 ) ∈ LinesEE ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ ( 𝑃 Line 𝑄 ) = ( 𝑝 Line 𝑞 ) ) )
21 19 20 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) ∈ LinesEE )
22 linerflx1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ ( 𝑃 Line 𝑄 ) )
23 linerflx2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑄 ∈ ( 𝑃 Line 𝑄 ) )
24 eleq2 ⊢ ( 𝑥 = ( 𝑃 Line 𝑄 ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑃 Line 𝑄 ) ) )
25 eleq2 ⊢ ( 𝑥 = ( 𝑃 Line 𝑄 ) → ( 𝑄 ∈ 𝑥 ↔ 𝑄 ∈ ( 𝑃 Line 𝑄 ) ) )
26 24 25 anbi12d ⊢ ( 𝑥 = ( 𝑃 Line 𝑄 ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( 𝑃 ∈ ( 𝑃 Line 𝑄 ) ∧ 𝑄 ∈ ( 𝑃 Line 𝑄 ) ) ) )
27 26 rspcev ⊢ ( ( ( 𝑃 Line 𝑄 ) ∈ LinesEE ∧ ( 𝑃 ∈ ( 𝑃 Line 𝑄 ) ∧ 𝑄 ∈ ( 𝑃 Line 𝑄 ) ) ) → ∃ 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
28 21 22 23 27 syl12anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃ 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )