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

Definition df-ofs 24678
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 24638). See brofs 24700 and 5segofs 24701 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 24677 . 2  class  OuterFiveSeg
2 vp . . . . . . . . . . . . . . 15  set  p
32cv 1631 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  set  a
54cv 1631 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  set  b
76cv 1631 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 3656 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  set  c
109cv 1631 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  set  d
1211cv 1631 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 3656 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 3656 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1632 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  set  q
1716cv 1631 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  set  x
1918cv 1631 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  set  y
2120cv 1631 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 3656 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  set  z
2423cv 1631 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  set  w
2625cv 1631 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 3656 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 3656 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1632 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
305, 10cop 3656 . . . . . . . . . . . . . . . 16  class  <. a ,  c >.
31 cbtwn 24589 . . . . . . . . . . . . . . . 16  class  Btwn
327, 30, 31wbr 4039 . . . . . . . . . . . . . . 15  wff  b  Btwn  <.
a ,  c >.
3319, 24cop 3656 . . . . . . . . . . . . . . . 16  class  <. x ,  z >.
3421, 33, 31wbr 4039 . . . . . . . . . . . . . . 15  wff  y  Btwn  <.
x ,  z >.
3532, 34wa 358 . . . . . . . . . . . . . 14  wff  ( b 
Btwn  <. a ,  c
>.  /\  y  Btwn  <. x ,  z >. )
36 ccgr 24590 . . . . . . . . . . . . . . . 16  class Cgr
378, 22, 36wbr 4039 . . . . . . . . . . . . . . 15  wff  <. a ,  b >.Cgr <. x ,  y >.
387, 10cop 3656 . . . . . . . . . . . . . . . 16  class  <. b ,  c >.
3921, 24cop 3656 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
4038, 39, 36wbr 4039 . . . . . . . . . . . . . . 15  wff  <. b ,  c >.Cgr <. y ,  z >.
4137, 40wa 358 . . . . . . . . . . . . . 14  wff  ( <.
a ,  b >.Cgr <. x ,  y >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )
425, 12cop 3656 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
4319, 26cop 3656 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
4442, 43, 36wbr 4039 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
457, 12cop 3656 . . . . . . . . . . . . . . . 16  class  <. b ,  d >.
4621, 26cop 3656 . . . . . . . . . . . . . . . 16  class  <. y ,  w >.
4745, 46, 36wbr 4039 . . . . . . . . . . . . . . 15  wff  <. b ,  d >.Cgr <. y ,  w >.
4844, 47wa 358 . . . . . . . . . . . . . 14  wff  ( <.
a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. )
4935, 41, 48w3a 934 . . . . . . . . . . . . 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 934 . . . . . . . . . . . 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 1631 . . . . . . . . . . . . 13  class  n
53 cee 24588 . . . . . . . . . . . . 13  class  EE
5452, 53cfv 5271 . . . . . . . . . . . 12  class  ( EE
`  n )
5550, 25, 54wrex 2557 . . . . . . . . . . 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 2557 . . . . . . . . . 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 2557 . . . . . . . . 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 2557 . . . . . . . 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 2557 . . . . . . 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 2557 . . . . . 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 2557 . . . . 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 2557 . . . 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 9762 . . . 4  class  NN
6462, 51, 63wrex 2557 . . 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 4092 . 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 1632 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  24700
  Copyright terms: Public domain W3C validator