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

Definition df-ofs 28026
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 23196). See brofs 28048 and 5segofs 28049 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 28025 . 2  class  OuterFiveSeg
2 vp . . . . . . . . . . . . . . 15  setvar  p
32cv 1368 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  setvar  a
54cv 1368 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  setvar  b
76cv 1368 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 3895 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  setvar  c
109cv 1368 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  setvar  d
1211cv 1368 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 3895 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 3895 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1369 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  setvar  q
1716cv 1368 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  setvar  x
1918cv 1368 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  setvar  y
2120cv 1368 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 3895 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  setvar  z
2423cv 1368 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  setvar  w
2625cv 1368 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 3895 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 3895 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1369 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
305, 10cop 3895 . . . . . . . . . . . . . . . 16  class  <. a ,  c >.
31 cbtwn 23147 . . . . . . . . . . . . . . . 16  class  Btwn
327, 30, 31wbr 4304 . . . . . . . . . . . . . . 15  wff  b  Btwn  <.
a ,  c >.
3319, 24cop 3895 . . . . . . . . . . . . . . . 16  class  <. x ,  z >.
3421, 33, 31wbr 4304 . . . . . . . . . . . . . . 15  wff  y  Btwn  <.
x ,  z >.
3532, 34wa 369 . . . . . . . . . . . . . 14  wff  ( b 
Btwn  <. a ,  c
>.  /\  y  Btwn  <. x ,  z >. )
36 ccgr 23148 . . . . . . . . . . . . . . . 16  class Cgr
378, 22, 36wbr 4304 . . . . . . . . . . . . . . 15  wff  <. a ,  b >.Cgr <. x ,  y >.
387, 10cop 3895 . . . . . . . . . . . . . . . 16  class  <. b ,  c >.
3921, 24cop 3895 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
4038, 39, 36wbr 4304 . . . . . . . . . . . . . . 15  wff  <. b ,  c >.Cgr <. y ,  z >.
4137, 40wa 369 . . . . . . . . . . . . . 14  wff  ( <.
a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )
425, 12cop 3895 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
4319, 26cop 3895 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
4442, 43, 36wbr 4304 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
457, 12cop 3895 . . . . . . . . . . . . . . . 16  class  <. b ,  d >.
4621, 26cop 3895 . . . . . . . . . . . . . . . 16  class  <. y ,  w >.
4745, 46, 36wbr 4304 . . . . . . . . . . . . . . 15  wff  <. b ,  d >.Cgr <. y ,  w >.
4844, 47wa 369 . . . . . . . . . . . . . 14  wff  ( <.
a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. )
4935, 41, 48w3a 965 . . . . . . . . . . . . 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 965 . . . . . . . . . . . 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  setvar  n
5251cv 1368 . . . . . . . . . . . . 13  class  n
53 cee 23146 . . . . . . . . . . . . 13  class  EE
5452, 53cfv 5430 . . . . . . . . . . . 12  class  ( EE
`  n )
5550, 25, 54wrex 2728 . . . . . . . . . . 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 2728 . . . . . . . . . 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 2728 . . . . . . . . 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 2728 . . . . . . . 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 2728 . . . . . . 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 2728 . . . . . 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 2728 . . . . 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 2728 . . . 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 10334 . . . 4  class  NN
6462, 51, 63wrex 2728 . . 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 4361 . 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 1369 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 setvar class
This definition is referenced by:  brofs  28048
  Copyright terms: Public domain W3C validator