Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ofs Unicode version

Definition df-ofs 25865
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 25825). See brofs 25887 and 5segofs 25888 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
Assertion
Ref Expression
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. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) ) }
Distinct variable group:    a, b, c, d, x, y, z, w, p, q, n

Detailed syntax breakdown of Definition df-ofs
StepHypRef Expression
1 cofs 25864 . 2  class  OuterFiveSeg
2 vp . . . . . . . . . . . . . . 15  set  p
32cv 1651 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  set  a
54cv 1651 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  set  b
76cv 1651 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 3809 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  set  c
109cv 1651 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  set  d
1211cv 1651 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 3809 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 3809 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1652 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  set  q
1716cv 1651 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  set  x
1918cv 1651 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  set  y
2120cv 1651 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 3809 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  set  z
2423cv 1651 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  set  w
2625cv 1651 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 3809 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 3809 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1652 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
305, 10cop 3809 . . . . . . . . . . . . . . . 16  class  <. a ,  c >.
31 cbtwn 25776 . . . . . . . . . . . . . . . 16  class  Btwn
327, 30, 31wbr 4204 . . . . . . . . . . . . . . 15  wff  b  Btwn  <.
a ,  c >.
3319, 24cop 3809 . . . . . . . . . . . . . . . 16  class  <. x ,  z >.
3421, 33, 31wbr 4204 . . . . . . . . . . . . . . 15  wff  y  Btwn  <.
x ,  z >.
3532, 34wa 359 . . . . . . . . . . . . . 14  wff  ( b 
Btwn  <. a ,  c
>.  /\  y  Btwn  <. x ,  z >. )
36 ccgr 25777 . . . . . . . . . . . . . . . 16  class Cgr
378, 22, 36wbr 4204 . . . . . . . . . . . . . . 15  wff  <. a ,  b >.Cgr <. x ,  y >.
387, 10cop 3809 . . . . . . . . . . . . . . . 16  class  <. b ,  c >.
3921, 24cop 3809 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
4038, 39, 36wbr 4204 . . . . . . . . . . . . . . 15  wff  <. b ,  c >.Cgr <. y ,  z >.
4137, 40wa 359 . . . . . . . . . . . . . 14  wff  ( <.
a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )
425, 12cop 3809 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
4319, 26cop 3809 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
4442, 43, 36wbr 4204 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
457, 12cop 3809 . . . . . . . . . . . . . . . 16  class  <. b ,  d >.
4621, 26cop 3809 . . . . . . . . . . . . . . . 16  class  <. y ,  w >.
4745, 46, 36wbr 4204 . . . . . . . . . . . . . . 15  wff  <. b ,  d >.Cgr <. y ,  w >.
4844, 47wa 359 . . . . . . . . . . . . . 14  wff  ( <.
a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. )
4935, 41, 48w3a 936 . . . . . . . . . . . . 13  wff  ( ( b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) )
5015, 29, 49w3a 936 . . . . . . . . . . . 12  wff  ( p  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
51 vn . . . . . . . . . . . . . 14  set  n
5251cv 1651 . . . . . . . . . . . . 13  class  n
53 cee 25775 . . . . . . . . . . . . 13  class  EE
5452, 53cfv 5445 . . . . . . . . . . . 12  class  ( EE
`  n )
5550, 25, 54wrex 2698 . . . . . . . . . . 11  wff  E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
5655, 23, 54wrex 2698 . . . . . . . . . 10  wff  E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
5756, 20, 54wrex 2698 . . . . . . . . 9  wff  E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
5857, 18, 54wrex 2698 . . . . . . . 8  wff  E. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
5958, 11, 54wrex 2698 . . . . . . 7  wff  E. d  e.  ( EE `  n
) E. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
6059, 9, 54wrex 2698 . . . . . 6  wff  E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) E. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
6160, 6, 54wrex 2698 . . . . 5  wff  E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) E. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
6261, 4, 54wrex 2698 . . . 4  wff  E. a  e.  ( EE `  n
) E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) E. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
63 cn 9989 . . . 4  class  NN
6462, 51, 63wrex 2698 . . 3  wff  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. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) )
6564, 2, 16copab 4257 . 2  class  { <. 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. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) ) }
661, 65wceq 1652 1  wff  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. x  e.  ( EE `  n
) E. y  e.  ( EE `  n
) E. z  e.  ( EE `  n
) E. w  e.  ( EE `  n
) ( p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  brofs  25887
  Copyright terms: Public domain W3C validator