Theorem liness

Description: A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	liness	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) ⊆ ( 𝔼 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fvline	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )
2		vex	⊢ 𝑥 ∈ V
3	2	a1i	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑥 ∈ V )
4		simp1	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simp2	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
6	3 4 5	3jca	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑥 ∈ V ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7		colineardim1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ V ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) )
8	6 7	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) )
9	8	abssdv	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ⊆ ( 𝔼 ‘ 𝑁 ) )
10	1 9	eqsstrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) ⊆ ( 𝔼 ‘ 𝑁 ) )