Metamath Proof Explorer

Theorem linedegen

Description: When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion linedegen 
|- ( A Line A ) = (/)

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A Line A ) = ( Line ` <. A , A >. )
2 neirr 
 |-  -. A =/= A
3 simp3 
 |-  ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) -> A =/= A )
4 2 3 mto 
 |-  -. ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A )
5 4 intnanr 
 |-  -. ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear )
6 5 a1i 
 |-  ( n e. NN -> -. ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) )
7 6 nrex 
 |-  -. E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear )
8 7 nex 
 |-  -. E. l E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear )
9 eleq1 
 |-  ( x = A -> ( x e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
10 neeq1 
 |-  ( x = A -> ( x =/= y <-> A =/= y ) )
11 9 10 3anbi13d 
 |-  ( x = A -> ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) <-> ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) ) )
12 opeq1 
 |-  ( x = A -> <. x , y >. = <. A , y >. )
13 12 eceq1d 
 |-  ( x = A -> [ <. x , y >. ] `' Colinear = [ <. A , y >. ] `' Colinear )
14 13 eqeq2d 
 |-  ( x = A -> ( l = [ <. x , y >. ] `' Colinear <-> l = [ <. A , y >. ] `' Colinear ) )
15 11 14 anbi12d 
 |-  ( x = A -> ( ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) <-> ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) ) )
16 15 rexbidv 
 |-  ( x = A -> ( E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) ) )
17 16 exbidv 
 |-  ( x = A -> ( E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) <-> E. l E. n e. NN ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) ) )
18 eleq1 
 |-  ( y = A -> ( y e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
19 neeq2 
 |-  ( y = A -> ( A =/= y <-> A =/= A ) )
20 18 19 3anbi23d 
 |-  ( y = A -> ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) <-> ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) ) )
21 opeq2 
 |-  ( y = A -> <. A , y >. = <. A , A >. )
22 21 eceq1d 
 |-  ( y = A -> [ <. A , y >. ] `' Colinear = [ <. A , A >. ] `' Colinear )
23 22 eqeq2d 
 |-  ( y = A -> ( l = [ <. A , y >. ] `' Colinear <-> l = [ <. A , A >. ] `' Colinear ) )
24 20 23 anbi12d 
 |-  ( y = A -> ( ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) <-> ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) ) )
25 24 rexbidv 
 |-  ( y = A -> ( E. n e. NN ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) ) )
26 25 exbidv 
 |-  ( y = A -> ( E. l E. n e. NN ( ( A e. ( EE ` n ) /\ y e. ( EE ` n ) /\ A =/= y ) /\ l = [ <. A , y >. ] `' Colinear ) <-> E. l E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) ) )
27 17 26 opelopabg 
 |-  ( ( A e. _V /\ A e. _V ) -> ( <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } <-> E. l E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) ) )
28 27 anidms 
 |-  ( A e. _V -> ( <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } <-> E. l E. n e. NN ( ( A e. ( EE ` n ) /\ A e. ( EE ` n ) /\ A =/= A ) /\ l = [ <. A , A >. ] `' Colinear ) ) )
29 8 28 mtbiri 
 |-  ( A e. _V -> -. <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } )
30 elopaelxp 
 |-  ( <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } -> <. A , A >. e. ( _V X. _V ) )
31 opelxp1 
 |-  ( <. A , A >. e. ( _V X. _V ) -> A e. _V )
32 30 31 syl 
 |-  ( <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } -> A e. _V )
33 32 con3i 
 |-  ( -. A e. _V -> -. <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } )
34 29 33 pm2.61i 
 |-  -. <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) }
35 df-line2 
 |-  Line = { <. <. x , y >. , l >. | E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) }
36 35 dmeqi 
 |-  dom Line = dom { <. <. x , y >. , l >. | E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) }
37 dmoprab 
 |-  dom { <. <. x , y >. , l >. | E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } = { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) }
38 36 37 eqtri 
 |-  dom Line = { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) }
39 38 eleq2i 
 |-  ( <. A , A >. e. dom Line <-> <. A , A >. e. { <. x , y >. | E. l E. n e. NN ( ( x e. ( EE ` n ) /\ y e. ( EE ` n ) /\ x =/= y ) /\ l = [ <. x , y >. ] `' Colinear ) } )
40 34 39 mtbir 
 |-  -. <. A , A >. e. dom Line
41 ndmfv 
 |-  ( -. <. A , A >. e. dom Line -> ( Line ` <. A , A >. ) = (/) )
42 40 41 ax-mp 
 |-  ( Line ` <. A , A >. ) = (/)
43 1 42 eqtri 
 |-  ( A Line A ) = (/)