Metamath Proof Explorer

Theorem brofs

Description: Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Assertion brofs 
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )

Proof

Step Hyp Ref Expression
1 opeq1 
 |-  ( a = A -> <. a , c >. = <. A , c >. )
2 1 breq2d 
 |-  ( a = A -> ( b Btwn <. a , c >. <-> b Btwn <. A , c >. ) )
3 2 anbi1d 
 |-  ( a = A -> ( ( b Btwn <. a , c >. /\ f Btwn <. e , g >. ) <-> ( b Btwn <. A , c >. /\ f Btwn <. e , g >. ) ) )
4 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
5 4 breq1d 
 |-  ( a = A -> ( <. a , b >. Cgr <. e , f >. <-> <. A , b >. Cgr <. e , f >. ) )
6 5 anbi1d 
 |-  ( a = A -> ( ( <. a , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) <-> ( <. A , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) ) )
7 opeq1 
 |-  ( a = A -> <. a , d >. = <. A , d >. )
8 7 breq1d 
 |-  ( a = A -> ( <. a , d >. Cgr <. e , h >. <-> <. A , d >. Cgr <. e , h >. ) )
9 8 anbi1d 
 |-  ( a = A -> ( ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) <-> ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) )
10 3 6 9 3anbi123d 
 |-  ( a = A -> ( ( ( b Btwn <. a , c >. /\ f Btwn <. e , g >. ) /\ ( <. a , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) /\ ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) <-> ( ( b Btwn <. A , c >. /\ f Btwn <. e , g >. ) /\ ( <. A , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) ) )
11 breq1 
 |-  ( b = B -> ( b Btwn <. A , c >. <-> B Btwn <. A , c >. ) )
12 11 anbi1d 
 |-  ( b = B -> ( ( b Btwn <. A , c >. /\ f Btwn <. e , g >. ) <-> ( B Btwn <. A , c >. /\ f Btwn <. e , g >. ) ) )
13 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
14 13 breq1d 
 |-  ( b = B -> ( <. A , b >. Cgr <. e , f >. <-> <. A , B >. Cgr <. e , f >. ) )
15 opeq1 
 |-  ( b = B -> <. b , c >. = <. B , c >. )
16 15 breq1d 
 |-  ( b = B -> ( <. b , c >. Cgr <. f , g >. <-> <. B , c >. Cgr <. f , g >. ) )
17 14 16 anbi12d 
 |-  ( b = B -> ( ( <. A , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) <-> ( <. A , B >. Cgr <. e , f >. /\ <. B , c >. Cgr <. f , g >. ) ) )
18 opeq1 
 |-  ( b = B -> <. b , d >. = <. B , d >. )
19 18 breq1d 
 |-  ( b = B -> ( <. b , d >. Cgr <. f , h >. <-> <. B , d >. Cgr <. f , h >. ) )
20 19 anbi2d 
 |-  ( b = B -> ( ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) <-> ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) )
21 12 17 20 3anbi123d 
 |-  ( b = B -> ( ( ( b Btwn <. A , c >. /\ f Btwn <. e , g >. ) /\ ( <. A , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) <-> ( ( B Btwn <. A , c >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , c >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) ) )
22 opeq2 
 |-  ( c = C -> <. A , c >. = <. A , C >. )
23 22 breq2d 
 |-  ( c = C -> ( B Btwn <. A , c >. <-> B Btwn <. A , C >. ) )
24 23 anbi1d 
 |-  ( c = C -> ( ( B Btwn <. A , c >. /\ f Btwn <. e , g >. ) <-> ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) ) )
25 opeq2 
 |-  ( c = C -> <. B , c >. = <. B , C >. )
26 25 breq1d 
 |-  ( c = C -> ( <. B , c >. Cgr <. f , g >. <-> <. B , C >. Cgr <. f , g >. ) )
27 26 anbi2d 
 |-  ( c = C -> ( ( <. A , B >. Cgr <. e , f >. /\ <. B , c >. Cgr <. f , g >. ) <-> ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) ) )
28 24 27 3anbi12d 
 |-  ( c = C -> ( ( ( B Btwn <. A , c >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , c >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) ) )
29 opeq2 
 |-  ( d = D -> <. A , d >. = <. A , D >. )
30 29 breq1d 
 |-  ( d = D -> ( <. A , d >. Cgr <. e , h >. <-> <. A , D >. Cgr <. e , h >. ) )
31 opeq2 
 |-  ( d = D -> <. B , d >. = <. B , D >. )
32 31 breq1d 
 |-  ( d = D -> ( <. B , d >. Cgr <. f , h >. <-> <. B , D >. Cgr <. f , h >. ) )
33 30 32 anbi12d 
 |-  ( d = D -> ( ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) )
34 33 3anbi3d 
 |-  ( d = D -> ( ( ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) ) )
35 opeq1 
 |-  ( e = E -> <. e , g >. = <. E , g >. )
36 35 breq2d 
 |-  ( e = E -> ( f Btwn <. e , g >. <-> f Btwn <. E , g >. ) )
37 36 anbi2d 
 |-  ( e = E -> ( ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) <-> ( B Btwn <. A , C >. /\ f Btwn <. E , g >. ) ) )
38 opeq1 
 |-  ( e = E -> <. e , f >. = <. E , f >. )
39 38 breq2d 
 |-  ( e = E -> ( <. A , B >. Cgr <. e , f >. <-> <. A , B >. Cgr <. E , f >. ) )
40 39 anbi1d 
 |-  ( e = E -> ( ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) <-> ( <. A , B >. Cgr <. E , f >. /\ <. B , C >. Cgr <. f , g >. ) ) )
41 opeq1 
 |-  ( e = E -> <. e , h >. = <. E , h >. )
42 41 breq2d 
 |-  ( e = E -> ( <. A , D >. Cgr <. e , h >. <-> <. A , D >. Cgr <. E , h >. ) )
43 42 anbi1d 
 |-  ( e = E -> ( ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) )
44 37 40 43 3anbi123d 
 |-  ( e = E -> ( ( ( B Btwn <. A , C >. /\ f Btwn <. e , g >. ) /\ ( <. A , B >. Cgr <. e , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ f Btwn <. E , g >. ) /\ ( <. A , B >. Cgr <. E , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) ) )
45 breq1 
 |-  ( f = F -> ( f Btwn <. E , g >. <-> F Btwn <. E , g >. ) )
46 45 anbi2d 
 |-  ( f = F -> ( ( B Btwn <. A , C >. /\ f Btwn <. E , g >. ) <-> ( B Btwn <. A , C >. /\ F Btwn <. E , g >. ) ) )
47 opeq2 
 |-  ( f = F -> <. E , f >. = <. E , F >. )
48 47 breq2d 
 |-  ( f = F -> ( <. A , B >. Cgr <. E , f >. <-> <. A , B >. Cgr <. E , F >. ) )
49 opeq1 
 |-  ( f = F -> <. f , g >. = <. F , g >. )
50 49 breq2d 
 |-  ( f = F -> ( <. B , C >. Cgr <. f , g >. <-> <. B , C >. Cgr <. F , g >. ) )
51 48 50 anbi12d 
 |-  ( f = F -> ( ( <. A , B >. Cgr <. E , f >. /\ <. B , C >. Cgr <. f , g >. ) <-> ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , g >. ) ) )
52 opeq1 
 |-  ( f = F -> <. f , h >. = <. F , h >. )
53 52 breq2d 
 |-  ( f = F -> ( <. B , D >. Cgr <. f , h >. <-> <. B , D >. Cgr <. F , h >. ) )
54 53 anbi2d 
 |-  ( f = F -> ( ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) )
55 46 51 54 3anbi123d 
 |-  ( f = F -> ( ( ( B Btwn <. A , C >. /\ f Btwn <. E , g >. ) /\ ( <. A , B >. Cgr <. E , f >. /\ <. B , C >. Cgr <. f , g >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , g >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , g >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) ) )
56 opeq2 
 |-  ( g = G -> <. E , g >. = <. E , G >. )
57 56 breq2d 
 |-  ( g = G -> ( F Btwn <. E , g >. <-> F Btwn <. E , G >. ) )
58 57 anbi2d 
 |-  ( g = G -> ( ( B Btwn <. A , C >. /\ F Btwn <. E , g >. ) <-> ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) ) )
59 opeq2 
 |-  ( g = G -> <. F , g >. = <. F , G >. )
60 59 breq2d 
 |-  ( g = G -> ( <. B , C >. Cgr <. F , g >. <-> <. B , C >. Cgr <. F , G >. ) )
61 60 anbi2d 
 |-  ( g = G -> ( ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , g >. ) <-> ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) ) )
62 58 61 3anbi12d 
 |-  ( g = G -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , g >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , g >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) ) )
63 opeq2 
 |-  ( h = H -> <. E , h >. = <. E , H >. )
64 63 breq2d 
 |-  ( h = H -> ( <. A , D >. Cgr <. E , h >. <-> <. A , D >. Cgr <. E , H >. ) )
65 opeq2 
 |-  ( h = H -> <. F , h >. = <. F , H >. )
66 65 breq2d 
 |-  ( h = H -> ( <. B , D >. Cgr <. F , h >. <-> <. B , D >. Cgr <. F , H >. ) )
67 64 66 anbi12d 
 |-  ( h = H -> ( ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) <-> ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) )
68 67 3anbi3d 
 |-  ( h = H -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
69 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
70 df-ofs 
 |-  OuterFiveSeg = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) E. g e. ( EE ` n ) E. h e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ( ( b Btwn <. a , c >. /\ f Btwn <. e , g >. ) /\ ( <. a , b >. Cgr <. e , f >. /\ <. b , c >. Cgr <. f , g >. ) /\ ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) ) }
71 10 21 28 34 44 55 62 68 69 70 br8 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )