Metamath Proof Explorer

Definition df-ofs

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom ( ax5seg ). See brofs and 5segofs for how it is used. Definition 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Assertion 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 >. ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cofs 
 |-  OuterFiveSeg
1 vp 
 |-  p
2 vq 
 |-  q
3 vn 
 |-  n
4 cn 
 |-  NN
5 va 
 |-  a
6 cee 
 |-  EE
7 3 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 vb 
 |-  b
10 vc 
 |-  c
11 vd 
 |-  d
12 vx 
 |-  x
13 vy 
 |-  y
14 vz 
 |-  z
15 vw 
 |-  w
16 1 cv 
 |-  p
17 5 cv 
 |-  a
18 9 cv 
 |-  b
19 17 18 cop 
 |-  <. a , b >.
20 10 cv 
 |-  c
21 11 cv 
 |-  d
22 20 21 cop 
 |-  <. c , d >.
23 19 22 cop 
 |-  <. <. a , b >. , <. c , d >. >.
24 16 23 wceq 
 |-  p = <. <. a , b >. , <. c , d >. >.
25 2 cv 
 |-  q
26 12 cv 
 |-  x
27 13 cv 
 |-  y
28 26 27 cop 
 |-  <. x , y >.
29 14 cv 
 |-  z
30 15 cv 
 |-  w
31 29 30 cop 
 |-  <. z , w >.
32 28 31 cop 
 |-  <. <. x , y >. , <. z , w >. >.
33 25 32 wceq 
 |-  q = <. <. x , y >. , <. z , w >. >.
34 cbtwn 
 |-  Btwn
35 17 20 cop 
 |-  <. a , c >.
36 18 35 34 wbr 
 |-  b Btwn <. a , c >.
37 26 29 cop 
 |-  <. x , z >.
38 27 37 34 wbr 
 |-  y Btwn <. x , z >.
39 36 38 wa 
 |-  ( b Btwn <. a , c >. /\ y Btwn <. x , z >. )
40 ccgr 
 |-  Cgr
41 19 28 40 wbr 
 |-  <. a , b >. Cgr <. x , y >.
42 18 20 cop 
 |-  <. b , c >.
43 27 29 cop 
 |-  <. y , z >.
44 42 43 40 wbr 
 |-  <. b , c >. Cgr <. y , z >.
45 41 44 wa 
 |-  ( <. a , b >. Cgr <. x , y >. /\ <. b , c >. Cgr <. y , z >. )
46 17 21 cop 
 |-  <. a , d >.
47 26 30 cop 
 |-  <. x , w >.
48 46 47 40 wbr 
 |-  <. a , d >. Cgr <. x , w >.
49 18 21 cop 
 |-  <. b , d >.
50 27 30 cop 
 |-  <. y , w >.
51 49 50 40 wbr 
 |-  <. b , d >. Cgr <. y , w >.
52 48 51 wa 
 |-  ( <. a , d >. Cgr <. x , w >. /\ <. b , d >. Cgr <. y , w >. )
53 39 45 52 w3a 
 |-  ( ( 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 >. ) )
54 24 33 53 w3a 
 |-  ( 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 >. ) ) )
55 54 15 8 wrex 
 |-  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 >. ) ) )
56 55 14 8 wrex 
 |-  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 >. ) ) )
57 56 13 8 wrex 
 |-  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 >. ) ) )
58 57 12 8 wrex 
 |-  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 >. ) ) )
59 58 11 8 wrex 
 |-  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 >. ) ) )
60 59 10 8 wrex 
 |-  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 >. ) ) )
61 60 9 8 wrex 
 |-  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 >. ) ) )
62 61 5 8 wrex 
 |-  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 62 3 4 wrex 
 |-  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 >. ) ) )
64 63 1 2 copab 
 |-  { <. 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 >. ) ) ) }
65 0 64 wceq 
 |-  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 >. ) ) ) }