Metamath Proof Explorer

Definition df-afs

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom ( axtg5seg ). See df-ofs . Definition 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013) (Revised by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion df-afs 
|- AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cafs 
 |-  AFS
1 vg 
 |-  g
2 cstrkg 
 |-  TarskiG
3 ve 
 |-  e
4 vf 
 |-  f
5 cbs 
 |-  Base
6 1 cv 
 |-  g
7 6 5 cfv 
 |-  ( Base ` g )
8 vp 
 |-  p
9 cds 
 |-  dist
10 6 9 cfv 
 |-  ( dist ` g )
11 vh 
 |-  h
12 citv 
 |-  Itv
13 6 12 cfv 
 |-  ( Itv ` g )
14 vi 
 |-  i
15 va 
 |-  a
16 8 cv 
 |-  p
17 vb 
 |-  b
18 vc 
 |-  c
19 vd 
 |-  d
20 vx 
 |-  x
21 vy 
 |-  y
22 vz 
 |-  z
23 vw 
 |-  w
24 3 cv 
 |-  e
25 15 cv 
 |-  a
26 17 cv 
 |-  b
27 25 26 cop 
 |-  <. a , b >.
28 18 cv 
 |-  c
29 19 cv 
 |-  d
30 28 29 cop 
 |-  <. c , d >.
31 27 30 cop 
 |-  <. <. a , b >. , <. c , d >. >.
32 24 31 wceq 
 |-  e = <. <. a , b >. , <. c , d >. >.
33 4 cv 
 |-  f
34 20 cv 
 |-  x
35 21 cv 
 |-  y
36 34 35 cop 
 |-  <. x , y >.
37 22 cv 
 |-  z
38 23 cv 
 |-  w
39 37 38 cop 
 |-  <. z , w >.
40 36 39 cop 
 |-  <. <. x , y >. , <. z , w >. >.
41 33 40 wceq 
 |-  f = <. <. x , y >. , <. z , w >. >.
42 14 cv 
 |-  i
43 25 28 42 co 
 |-  ( a i c )
44 26 43 wcel 
 |-  b e. ( a i c )
45 34 37 42 co 
 |-  ( x i z )
46 35 45 wcel 
 |-  y e. ( x i z )
47 44 46 wa 
 |-  ( b e. ( a i c ) /\ y e. ( x i z ) )
48 11 cv 
 |-  h
49 25 26 48 co 
 |-  ( a h b )
50 34 35 48 co 
 |-  ( x h y )
51 49 50 wceq 
 |-  ( a h b ) = ( x h y )
52 26 28 48 co 
 |-  ( b h c )
53 35 37 48 co 
 |-  ( y h z )
54 52 53 wceq 
 |-  ( b h c ) = ( y h z )
55 51 54 wa 
 |-  ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) )
56 25 29 48 co 
 |-  ( a h d )
57 34 38 48 co 
 |-  ( x h w )
58 56 57 wceq 
 |-  ( a h d ) = ( x h w )
59 26 29 48 co 
 |-  ( b h d )
60 35 38 48 co 
 |-  ( y h w )
61 59 60 wceq 
 |-  ( b h d ) = ( y h w )
62 58 61 wa 
 |-  ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) )
63 47 55 62 w3a 
 |-  ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) )
64 32 41 63 w3a 
 |-  ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
65 64 23 16 wrex 
 |-  E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
66 65 22 16 wrex 
 |-  E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
67 66 21 16 wrex 
 |-  E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
68 67 20 16 wrex 
 |-  E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
69 68 19 16 wrex 
 |-  E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
70 69 18 16 wrex 
 |-  E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
71 70 17 16 wrex 
 |-  E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
72 71 15 16 wrex 
 |-  E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
73 72 14 13 wsbc 
 |-  [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
74 73 11 10 wsbc 
 |-  [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
75 74 8 7 wsbc 
 |-  [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
76 75 3 4 copab 
 |-  { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) }
77 1 2 76 cmpt 
 |-  ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )
78 0 77 wceq 
 |-  AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )