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

Definition df-ifs 24023
Description: The inner five segment configuration is an abbreviation for another congruence condition. See brifs 24027 and ifscgr 24028 for how it is used. Definition 4.1 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 26-Sep-2013.)
Assertion
Ref Expression
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. 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) ) }
Distinct variable group:    a, b, c, d, x, y, z, w, p, q, n

Detailed syntax breakdown of Definition df-ifs
StepHypRef Expression
1 cifs 24019 . 2  class  InnerFiveSeg
2 vp . . . . . . . . . . . . . . 15  set  p
32cv 1618 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  set  a
54cv 1618 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  set  b
76cv 1618 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 3603 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  set  c
109cv 1618 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  set  d
1211cv 1618 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 3603 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 3603 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1619 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  set  q
1716cv 1618 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  set  x
1918cv 1618 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  set  y
2120cv 1618 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 3603 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  set  z
2423cv 1618 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  set  w
2625cv 1618 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 3603 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 3603 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1619 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
305, 10cop 3603 . . . . . . . . . . . . . . . 16  class  <. a ,  c >.
31 cbtwn 23878 . . . . . . . . . . . . . . . 16  class  Btwn
327, 30, 31wbr 3983 . . . . . . . . . . . . . . 15  wff  b  Btwn  <.
a ,  c >.
3319, 24cop 3603 . . . . . . . . . . . . . . . 16  class  <. x ,  z >.
3421, 33, 31wbr 3983 . . . . . . . . . . . . . . 15  wff  y  Btwn  <.
x ,  z >.
3532, 34wa 360 . . . . . . . . . . . . . 14  wff  ( b 
Btwn  <. a ,  c
>.  /\  y  Btwn  <. x ,  z >. )
36 ccgr 23879 . . . . . . . . . . . . . . . 16  class Cgr
3730, 33, 36wbr 3983 . . . . . . . . . . . . . . 15  wff  <. a ,  c >.Cgr <. x ,  z >.
387, 10cop 3603 . . . . . . . . . . . . . . . 16  class  <. b ,  c >.
3921, 24cop 3603 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
4038, 39, 36wbr 3983 . . . . . . . . . . . . . . 15  wff  <. b ,  c >.Cgr <. y ,  z >.
4137, 40wa 360 . . . . . . . . . . . . . 14  wff  ( <.
a ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )
425, 12cop 3603 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
4319, 26cop 3603 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
4442, 43, 36wbr 3983 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
4513, 27, 36wbr 3983 . . . . . . . . . . . . . . 15  wff  <. c ,  d >.Cgr <. z ,  w >.
4644, 45wa 360 . . . . . . . . . . . . . 14  wff  ( <.
a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. )
4735, 41, 46w3a 939 . . . . . . . . . . . . 13  wff  ( ( b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) )
4815, 29, 47w3a 939 . . . . . . . . . . . 12  wff  ( p  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  Btwn  <. a ,  c >.  /\  y  Btwn  <. x ,  z
>. )  /\  ( <. a ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
49 vn . . . . . . . . . . . . . 14  set  n
5049cv 1618 . . . . . . . . . . . . 13  class  n
51 cee 23877 . . . . . . . . . . . . 13  class  EE
5250, 51cfv 4659 . . . . . . . . . . . 12  class  ( EE
`  n )
5348, 25, 52wrex 2517 . . . . . . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5453, 23, 52wrex 2517 . . . . . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5554, 20, 52wrex 2517 . . . . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5655, 18, 52wrex 2517 . . . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5756, 11, 52wrex 2517 . . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5857, 9, 52wrex 2517 . . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
5958, 6, 52wrex 2517 . . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
6059, 4, 52wrex 2517 . . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
61 cn 9700 . . . 4  class  NN
6260, 49, 61wrex 2517 . . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) )
6362, 2, 16copab 4036 . 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) ) }
641, 63wceq 1619 1  wff  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. 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 ,  c >.Cgr <. x ,  z >.  /\  <. b ,  c
>.Cgr <. y ,  z
>. )  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\ 
<. c ,  d >.Cgr <. z ,  w >. ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  brifs  24027
  Copyright terms: Public domain W3C validator