Metamath Proof Explorer

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 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) C_ ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 fvline 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x | x Colinear <. A , B >. } )
2 vex 
 |-  x e. _V
3 2 a1i 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> x e. _V )
4 simp1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> A e. ( EE ` N ) )
5 simp2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> B e. ( EE ` N ) )
6 3 4 5 3jca 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( x e. _V /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
7 colineardim1 
 |-  ( ( N e. NN /\ ( x e. _V /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( x Colinear <. A , B >. -> x e. ( EE ` N ) ) )
8 6 7 sylan2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( x Colinear <. A , B >. -> x e. ( EE ` N ) ) )
9 8 abssdv 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> { x | x Colinear <. A , B >. } C_ ( EE ` N ) )
10 1 9 eqsstrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) C_ ( EE ` N ) )