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