Metamath Proof Explorer

Theorem ellines

Description: Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion ellines 
|- ( A e. LinesEE <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. LinesEE -> A e. _V )
2 ovex 
 |-  ( p Line q ) e. _V
3 eleq1 
 |-  ( A = ( p Line q ) -> ( A e. _V <-> ( p Line q ) e. _V ) )
4 2 3 mpbiri 
 |-  ( A = ( p Line q ) -> A e. _V )
5 4 adantl 
 |-  ( ( p =/= q /\ A = ( p Line q ) ) -> A e. _V )
6 5 rexlimivw 
 |-  ( E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) -> A e. _V )
7 6 a1i 
 |-  ( ( n e. NN /\ p e. ( EE ` n ) ) -> ( E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) -> A e. _V ) )
8 7 rexlimivv 
 |-  ( E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) -> A e. _V )
9 eleq1 
 |-  ( x = A -> ( x e. LinesEE <-> A e. LinesEE ) )
10 eqeq1 
 |-  ( x = A -> ( x = ( p Line q ) <-> A = ( p Line q ) ) )
11 10 anbi2d 
 |-  ( x = A -> ( ( p =/= q /\ x = ( p Line q ) ) <-> ( p =/= q /\ A = ( p Line q ) ) ) )
12 11 rexbidv 
 |-  ( x = A -> ( E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) <-> E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) ) )
13 12 2rexbidv 
 |-  ( x = A -> ( E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) ) )
14 df-lines2 
 |-  LinesEE = ran Line
15 df-line2 
 |-  Line = { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) }
16 15 rneqi 
 |-  ran Line = ran { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) }
17 rnoprab 
 |-  ran { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) } = { x | E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) }
18 14 16 17 3eqtri 
 |-  LinesEE = { x | E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) }
19 18 eleq2i 
 |-  ( x e. LinesEE <-> x e. { x | E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) } )
20 abid 
 |-  ( x e. { x | E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) } <-> E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) )
21 df-rex 
 |-  ( E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) <-> E. n ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) )
22 21 2exbii 
 |-  ( E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) <-> E. p E. q E. n ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) )
23 exrot3 
 |-  ( E. n E. p E. q ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) <-> E. p E. q E. n ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
24 r2ex 
 |-  ( E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) <-> E. n E. p ( ( n e. NN /\ p e. ( EE ` n ) ) /\ E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) ) )
25 r19.42v 
 |-  ( E. q e. ( EE ` n ) ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) <-> ( ( n e. NN /\ p e. ( EE ` n ) ) /\ E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) ) )
26 df-rex 
 |-  ( E. q e. ( EE ` n ) ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) <-> E. q ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
27 25 26 bitr3i 
 |-  ( ( ( n e. NN /\ p e. ( EE ` n ) ) /\ E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) ) <-> E. q ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
28 27 2exbii 
 |-  ( E. n E. p ( ( n e. NN /\ p e. ( EE ` n ) ) /\ E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) ) <-> E. n E. p E. q ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
29 24 28 bitri 
 |-  ( E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) <-> E. n E. p E. q ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
30 anass 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) <-> ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
31 anass 
 |-  ( ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) /\ x = ( p Line q ) ) <-> ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) )
32 simplrl 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> n e. NN )
33 simplrr 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> p e. ( EE ` n ) )
34 simpll 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> q e. ( EE ` n ) )
35 simpr 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> p =/= q )
36 33 34 35 3jca 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) )
37 32 36 jca 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) -> ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) )
38 simpr2 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> q e. ( EE ` n ) )
39 simpl 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> n e. NN )
40 simpr1 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> p e. ( EE ` n ) )
41 38 39 40 jca32 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) )
42 simpr3 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> p =/= q )
43 41 42 jca 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) )
44 37 43 impbii 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) <-> ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) )
45 44 anbi1i 
 |-  ( ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ p =/= q ) /\ x = ( p Line q ) ) <-> ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = ( p Line q ) ) )
46 31 45 bitr3i 
 |-  ( ( ( q e. ( EE ` n ) /\ ( n e. NN /\ p e. ( EE ` n ) ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) <-> ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = ( p Line q ) ) )
47 30 46 bitr3i 
 |-  ( ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) <-> ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = ( p Line q ) ) )
48 fvline 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> ( p Line q ) = { x | x Colinear <. p , q >. } )
49 opex 
 |-  <. p , q >. e. _V
50 dfec2 
 |-  ( <. p , q >. e. _V -> [ <. p , q >. ] `' Colinear = { x | <. p , q >. `' Colinear x } )
51 49 50 ax-mp 
 |-  [ <. p , q >. ] `' Colinear = { x | <. p , q >. `' Colinear x }
52 vex 
 |-  x e. _V
53 49 52 brcnv 
 |-  ( <. p , q >. `' Colinear x <-> x Colinear <. p , q >. )
54 53 abbii 
 |-  { x | <. p , q >. `' Colinear x } = { x | x Colinear <. p , q >. }
55 51 54 eqtri 
 |-  [ <. p , q >. ] `' Colinear = { x | x Colinear <. p , q >. }
56 48 55 eqtr4di 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> ( p Line q ) = [ <. p , q >. ] `' Colinear )
57 56 eqeq2d 
 |-  ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) -> ( x = ( p Line q ) <-> x = [ <. p , q >. ] `' Colinear ) )
58 57 pm5.32i 
 |-  ( ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = ( p Line q ) ) <-> ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = [ <. p , q >. ] `' Colinear ) )
59 anass 
 |-  ( ( ( n e. NN /\ ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) ) /\ x = [ <. p , q >. ] `' Colinear ) <-> ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) )
60 47 58 59 3bitrri 
 |-  ( ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) <-> ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
61 60 3exbii 
 |-  ( E. p E. q E. n ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) <-> E. p E. q E. n ( q e. ( EE ` n ) /\ ( ( n e. NN /\ p e. ( EE ` n ) ) /\ ( p =/= q /\ x = ( p Line q ) ) ) ) )
62 23 29 61 3bitr4ri 
 |-  ( E. p E. q E. n ( n e. NN /\ ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) ) <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) )
63 22 62 bitri 
 |-  ( E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) )
64 20 63 bitri 
 |-  ( x e. { x | E. p E. q E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ p =/= q ) /\ x = [ <. p , q >. ] `' Colinear ) } <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) )
65 19 64 bitri 
 |-  ( x e. LinesEE <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ x = ( p Line q ) ) )
66 9 13 65 vtoclbg 
 |-  ( A e. _V -> ( A e. LinesEE <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) ) )
67 1 8 66 pm5.21nii 
 |-  ( A e. LinesEE <-> E. n e. NN E. p e. ( EE ` n ) E. q e. ( EE ` n ) ( p =/= q /\ A = ( p Line q ) ) )