Metamath Proof Explorer

Theorem funline

Description: Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funline 
|- Fun Line

Proof

Step Hyp Ref Expression
1 reeanv 
 |-  ( E. n e. NN E. m e. NN ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) <-> ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) )
2 eqtr3 
 |-  ( ( l = [ <. a , b >. ] `' Colinear /\ k = [ <. a , b >. ] `' Colinear ) -> l = k )
3 2 ad2ant2l 
 |-  ( ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k )
4 3 a1i 
 |-  ( ( n e. NN /\ m e. NN ) -> ( ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k ) )
5 4 rexlimivv 
 |-  ( E. n e. NN E. m e. NN ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k )
6 1 5 sylbir 
 |-  ( ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k )
7 6 gen2 
 |-  A. l A. k ( ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k )
8 eqeq1 
 |-  ( l = k -> ( l = [ <. a , b >. ] `' Colinear <-> k = [ <. a , b >. ] `' Colinear ) )
9 8 anbi2d 
 |-  ( l = k -> ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) )
10 9 rexbidv 
 |-  ( l = k -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) )
11 fveq2 
 |-  ( n = m -> ( EE ` n ) = ( EE ` m ) )
12 11 eleq2d 
 |-  ( n = m -> ( a e. ( EE ` n ) <-> a e. ( EE ` m ) ) )
13 11 eleq2d 
 |-  ( n = m -> ( b e. ( EE ` n ) <-> b e. ( EE ` m ) ) )
14 12 13 3anbi12d 
 |-  ( n = m -> ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) <-> ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) ) )
15 14 anbi1d 
 |-  ( n = m -> ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) <-> ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) )
16 15 cbvrexvw 
 |-  ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) <-> E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) )
17 10 16 bitrdi 
 |-  ( l = k -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) )
18 17 mo4 
 |-  ( E* l E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> A. l A. k ( ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) /\ E. m e. NN ( ( a e. ( EE ` m ) /\ b e. ( EE ` m ) /\ a =/= b ) /\ k = [ <. a , b >. ] `' Colinear ) ) -> l = k ) )
19 7 18 mpbir 
 |-  E* l E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
20 19 funoprab 
 |-  Fun { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }
21 df-line2 
 |-  Line = { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }
22 21 funeqi 
 |-  ( Fun Line <-> Fun { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } )
23 20 22 mpbir 
 |-  Fun Line