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 29567
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 24073). See brofs 29589 and 5segofs 29590 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 29566 . 2  class  OuterFiveSeg
2 vp . . . . . . . . . . . . . . 15  setvar  p
32cv 1378 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  setvar  a
54cv 1378 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  setvar  b
76cv 1378 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 4039 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  setvar  c
109cv 1378 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  setvar  d
1211cv 1378 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 4039 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 4039 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1379 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  setvar  q
1716cv 1378 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  setvar  x
1918cv 1378 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  setvar  y
2120cv 1378 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 4039 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  setvar  z
2423cv 1378 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  setvar  w
2625cv 1378 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 4039 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 4039 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1379 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
305, 10cop 4039 . . . . . . . . . . . . . . . 16  class  <. a ,  c >.
31 cbtwn 24024 . . . . . . . . . . . . . . . 16  class  Btwn
327, 30, 31wbr 4453 . . . . . . . . . . . . . . 15  wff  b  Btwn  <.
a ,  c >.
3319, 24cop 4039 . . . . . . . . . . . . . . . 16  class  <. x ,  z >.
3421, 33, 31wbr 4453 . . . . . . . . . . . . . . 15  wff  y  Btwn  <.
x ,  z >.
3532, 34wa 369 . . . . . . . . . . . . . 14  wff  ( b 
Btwn  <. a ,  c
>.  /\  y  Btwn  <. x ,  z >. )
36 ccgr 24025 . . . . . . . . . . . . . . . 16  class Cgr
378, 22, 36wbr 4453 . . . . . . . . . . . . . . 15  wff  <. a ,  b >.Cgr <. x ,  y >.
387, 10cop 4039 . . . . . . . . . . . . . . . 16  class  <. b ,  c >.
3921, 24cop 4039 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
4038, 39, 36wbr 4453 . . . . . . . . . . . . . . 15  wff  <. b ,  c >.Cgr <. y ,  z >.
4137, 40wa 369 . . . . . . . . . . . . . 14  wff  ( <.
a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )
425, 12cop 4039 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
4319, 26cop 4039 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
4442, 43, 36wbr 4453 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
457, 12cop 4039 . . . . . . . . . . . . . . . 16  class  <. b ,  d >.
4621, 26cop 4039 . . . . . . . . . . . . . . . 16  class  <. y ,  w >.
4745, 46, 36wbr 4453 . . . . . . . . . . . . . . 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 973 . . . . . . . . . . . . 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 973 . . . . . . . . . . . 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 1378 . . . . . . . . . . . . 13  class  n
53 cee 24023 . . . . . . . . . . . . 13  class  EE
5452, 53cfv 5594 . . . . . . . . . . . 12  class  ( EE
`  n )
5550, 25, 54wrex 2818 . . . . . . . . . . 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 2818 . . . . . . . . . 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 2818 . . . . . . . . 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 2818 . . . . . . . 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 2818 . . . . . . 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 2818 . . . . . 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 2818 . . . . 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 2818 . . . 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 10548 . . . 4  class  NN
6462, 51, 63wrex 2818 . . 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 4510 . 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 1379 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  29589
  Copyright terms: Public domain W3C validator