Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ibcg Unicode version

Definition df-ibcg 25589
Description: Incidence-Betweenness Geometry plus congruence axioms. (Here is an excerpt of Aitken's handout.)

Axiom (C-1). Segment congruence is an equivalence relation for line segments.

Axiom (C-2). Suppose that 
A B is a line segment and  C D is a ray. Then there is a unique point  E on  C D, distinct from  C, such that  A B  .~  s C E. The next axiom concerns copying dividing or intermediate points on a segment.

Axiom (C-3). Suppose that 
A C and  A' C' are congruent line segments. If B is a point such that  A * B * C, then there is a point  B' such that  A' * B' * C',  A B  .~  s A' B', and  B C  .~  s B' C'.

Axiom (C-4). Angle congruence is an equivalence relation for angles.

Axiom (C-5). (Copying an angle) Suppose  B A C is an angle, and  D E is a ray. Then on any given side of  D E, there is a unique ray  D F such that  B A C  .~  a E D F.

Axiom (C-6). (Copying a triangle) Suppose  A B C is a triangle, and  A' B' is a segment such that  A B  .~  s A' B'. Then on any given side of  A' B', there is a point  C' such that  A B C  .~  a A' B' C'.

(For my private use only. Don't use.) Axiom C-1 C-2, C-3, C-4, C-5, C-6 of [AitkenIBCG] p. 2 . (Contributed by FL, 1-Apr-2016.)

Assertion
Ref Expression
df-ibcg  |- Ibcg  =  {
g  e. Ibg  |  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) }
Distinct variable group:    a, b, c, d, e, f, g, l, o, p, q, r, s, t, u, v, w, x, y, z

Detailed syntax breakdown of Definition df-ibcg
StepHypRef Expression
1 cibcg 25580 . 2  class Ibcg
2 vy . . . . . . . . . . . . . . . . . . 19  set  y
32cv 1627 . . . . . . . . . . . . . . . . . 18  class  y
4 vs . . . . . . . . . . . . . . . . . . 19  set  s
54cv 1627 . . . . . . . . . . . . . . . . . 18  class  s
63, 5wer 6652 . . . . . . . . . . . . . . . . 17  wff  s  Er  y
7 vu . . . . . . . . . . . . . . . . . . . 20  set  u
87cv 1627 . . . . . . . . . . . . . . . . . . 19  class  u
9 vw . . . . . . . . . . . . . . . . . . . 20  set  w
109cv 1627 . . . . . . . . . . . . . . . . . . 19  class  w
118, 10cima 4691 . . . . . . . . . . . . . . . . . 18  class  ( u
" w )
12 vo . . . . . . . . . . . . . . . . . . 19  set  o
1312cv 1627 . . . . . . . . . . . . . . . . . 18  class  o
1411, 13wer 6652 . . . . . . . . . . . . . . . . 17  wff  o  Er  ( u " w
)
15 vd . . . . . . . . . . . . . . . . . . . . . 22  set  d
1615cv 1627 . . . . . . . . . . . . . . . . . . . . 21  class  d
17 ve . . . . . . . . . . . . . . . . . . . . . 22  set  e
1817cv 1627 . . . . . . . . . . . . . . . . . . . . 21  class  e
1916, 18wne 2447 . . . . . . . . . . . . . . . . . . . 20  wff  d  =/=  e
20 va . . . . . . . . . . . . . . . . . . . . . . . . . . 27  set  a
2120cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  a
22 vb . . . . . . . . . . . . . . . . . . . . . . . . . . 27  set  b
2322cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  b
2421, 23wne 2447 . . . . . . . . . . . . . . . . . . . . . . . . 25  wff  a  =/=  b
25 vf . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  set  f
2625cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  f
2726, 16wne 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  wff  f  =/=  d
28 vt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  set  t
2928cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  t
3021, 23, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  ( a t b )
3116, 26, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  ( d t f )
3230, 31, 5wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  wff  ( a t b ) s ( d t f )
3327, 32wa 360 . . . . . . . . . . . . . . . . . . . . . . . . . 26  wff  ( f  =/=  d  /\  (
a t b ) s ( d t f ) )
34 vr . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  set  r
3534cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  r
3616, 18, 35co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  ( d r e )
3733, 25, 36wreu 2546 . . . . . . . . . . . . . . . . . . . . . . . . 25  wff  E! f  e.  ( d r e ) ( f  =/=  d  /\  (
a t b ) s ( d t f ) )
3824, 37wi 6 . . . . . . . . . . . . . . . . . . . . . . . 24  wff  ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )
39 vc . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  set  c
4039cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  c
41 vq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  set  q
4241cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  q
4321, 23, 42co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  ( a q b )
4440, 43wcel 1688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  wff  c  e.  ( a q b )
4516, 18, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  ( d t e )
4630, 45, 5wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  wff  ( a t b ) s ( d t e )
4744, 46wa 360 . . . . . . . . . . . . . . . . . . . . . . . . . 26  wff  ( c  e.  ( a q b )  /\  (
a t b ) s ( d t e ) )
4816, 18, 42co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  ( d q e )
4926, 48wcel 1688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  wff  f  e.  ( d q e )
5021, 40, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  ( a t c )
5150, 31, 5wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  wff  ( a t c ) s ( d t f )
5240, 23, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  ( c t b )
5326, 18, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  class  ( f t e )
5452, 53, 5wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  wff  ( c t b ) s ( f t e )
5549, 51, 54w3a 939 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  wff  ( f  e.  ( d q e )  /\  (
a t c ) s ( d t f )  /\  (
c t b ) s ( f t e ) )
56 vp . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  set  p
5756cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  p
5855, 25, 57wrex 2545 . . . . . . . . . . . . . . . . . . . . . . . . . 26  wff  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) )
5947, 58wi 6 . . . . . . . . . . . . . . . . . . . . . . . . 25  wff  ( ( c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) )
6059, 39, 57wral 2544 . . . . . . . . . . . . . . . . . . . . . . . 24  wff  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) )
6138, 60wa 360 . . . . . . . . . . . . . . . . . . . . . . 23  wff  ( ( a  =/=  b  ->  E! f  e.  (
d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )
6261, 22, 57wral 2544 . . . . . . . . . . . . . . . . . . . . . 22  wff  A. b  e.  p  ( (
a  =/=  b  ->  E! f  e.  (
d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )
6362, 20, 57wral 2544 . . . . . . . . . . . . . . . . . . . . 21  wff  A. a  e.  p  A. b  e.  p  ( (
a  =/=  b  ->  E! f  e.  (
d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )
6421, 8cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  ( u `
 a )
6518, 16, 26cs3 11486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  <" e
d f ">
6665, 8cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  ( u `
 <" e d f "> )
6764, 66, 13wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . 25  wff  ( u `
 a ) o ( u `  <" e d f "> )
6867, 25, 23wreu 2546 . . . . . . . . . . . . . . . . . . . . . . . 24  wff  E! f  e.  b  ( u `
 a ) o ( u `  <" e d f "> )
69 vl . . . . . . . . . . . . . . . . . . . . . . . . . . 27  set  l
7069cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  l
7116, 18, 70co 5819 . . . . . . . . . . . . . . . . . . . . . . . . 25  class  ( d l e )
72 vx . . . . . . . . . . . . . . . . . . . . . . . . . 26  set  x
7372cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . 25  class  x
7471, 73cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . 24  class  ( x `
 ( d l e ) )
7568, 22, 74wral 2544 . . . . . . . . . . . . . . . . . . . . . . 23  wff  A. b  e.  ( x `  (
d l e ) ) E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> )
76 c1 8733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  1
7776, 21cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  ( a `
 1 )
78 c2 9790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  2
7978, 21cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  class  ( a `
 2 )
8077, 79, 29co 5819 . . . . . . . . . . . . . . . . . . . . . . . . 25  class  ( ( a `  1 ) t ( a ` 
2 ) )
8180, 45, 5wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . 24  wff  ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )
8216, 18, 26cs3 11486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  <" d
e f ">
83 vv . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  set  v
8483cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  class  v
8582, 84cfv 5221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  ( v `
 <" d e f "> )
86 vz . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  set  z
8786cv 1627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  class  z
8821, 85, 87wbr 4024 . . . . . . . . . . . . . . . . . . . . . . . . . 26  wff  a z ( v `  <" d e f "> )
8988, 25, 23wrex 2545 . . . . . . . . . . . . . . . . . . . . . . . . 25  wff  E. f  e.  b  a z
( v `  <" d e f "> )
9089, 22, 74wral 2544 . . . . . . . . . . . . . . . . . . . . . . . 24  wff  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> )
9181, 90wi 6 . . . . . . . . . . . . . . . . . . . . . . 23  wff  ( ( ( a `  1
) t ( a `
 2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) )
9275, 91wa 360 . . . . . . . . . . . . . . . . . . . . . 22  wff  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `
 a ) o ( u `  <" e d f "> )  /\  (
( ( a ` 
1 ) t ( a `  2 ) ) s ( d t e )  ->  A. b  e.  (
x `  ( d
l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) )
9392, 20, 10wral 2544 . . . . . . . . . . . . . . . . . . . . 21  wff  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `
 a ) o ( u `  <" e d f "> )  /\  (
( ( a ` 
1 ) t ( a `  2 ) ) s ( d t e )  ->  A. b  e.  (
x `  ( d
l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) )
9463, 93wa 360 . . . . . . . . . . . . . . . . . . . 20  wff  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) )
9519, 94wi 6 . . . . . . . . . . . . . . . . . . 19  wff  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( ( c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  (
d l e ) ) E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) )
9695, 17, 57wral 2544 . . . . . . . . . . . . . . . . . 18  wff  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )
9796, 15, 57wral 2544 . . . . . . . . . . . . . . . . 17  wff  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )
986, 14, 97w3a 939 . . . . . . . . . . . . . . . 16  wff  ( s  Er  y  /\  o  Er  ( u " w
)  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
99 vg . . . . . . . . . . . . . . . . . 18  set  g
10099cv 1627 . . . . . . . . . . . . . . . . 17  class  g
101 ctrcng 25560 . . . . . . . . . . . . . . . . 17  class trcng
102100, 101cfv 5221 . . . . . . . . . . . . . . . 16  class  (trcng `  g )
10398, 86, 102wsbc 2992 . . . . . . . . . . . . . . 15  wff  [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
104 cSeg 25547 . . . . . . . . . . . . . . . 16  class Segments
105100, 104cfv 5221 . . . . . . . . . . . . . . 15  class  (Segments `  g
)
106103, 2, 105wsbc 2992 . . . . . . . . . . . . . 14  wff  [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
107 chalfp 25569 . . . . . . . . . . . . . . 15  class Halfplane
108100, 107cfv 5221 . . . . . . . . . . . . . 14  class  (Halfplane `  g
)
109106, 72, 108wsbc 2992 . . . . . . . . . . . . 13  wff  [. (Halfplane `  g )  /  x ]. [. (Segments `  g
)  /  y ]. [. (trcng `  g )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
110 c3 9791 . . . . . . . . . . . . . 14  class  3
111 cdwords 25383 . . . . . . . . . . . . . 14  class dWords
11257, 110, 111co 5819 . . . . . . . . . . . . 13  class  ( pdWords 3 )
113109, 9, 112wsbc 2992 . . . . . . . . . . . 12  wff  [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
114 ctriangle 25558 . . . . . . . . . . . . 13  class triangle
115100, 114cfv 5221 . . . . . . . . . . . 12  class  (triangle `  g
)
116113, 83, 115wsbc 2992 . . . . . . . . . . 11  wff  [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
117 cangle 25556 . . . . . . . . . . . 12  class angle
118100, 117cfv 5221 . . . . . . . . . . 11  class  (angle `  g )
119116, 7, 118wsbc 2992 . . . . . . . . . 10  wff  [. (angle `  g )  /  u ]. [. (triangle `  g
)  /  v ]. [. ( pdWords 3 )  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g
)  /  y ]. [. (trcng `  g )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
120 cline 25475 . . . . . . . . . . 11  class  line
121100, 120cfv 5221 . . . . . . . . . 10  class  ( line `  g )
122119, 69, 121wsbc 2992 . . . . . . . . 9  wff  [. ( line `  g )  / 
l ]. [. (angle `  g )  /  u ]. [. (triangle `  g
)  /  v ]. [. ( pdWords 3 )  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g
)  /  y ]. [. (trcng `  g )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
123 cseg 25529 . . . . . . . . . 10  class  seg
124100, 123cfv 5221 . . . . . . . . 9  class  ( seg `  g )
125122, 28, 124wsbc 2992 . . . . . . . 8  wff  [. ( seg `  g )  / 
t ]. [. ( line `  g )  /  l ]. [. (angle `  g
)  /  u ]. [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
126 csegc 25579 . . . . . . . . 9  class segc
127100, 126cfv 5221 . . . . . . . 8  class  (segc `  g )
128125, 4, 127wsbc 2992 . . . . . . 7  wff  [. (segc `  g )  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
129 cray2 25550 . . . . . . . 8  class ray
130100, 129cfv 5221 . . . . . . 7  class  (ray `  g )
131128, 34, 130wsbc 2992 . . . . . 6  wff  [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
132 cbtw 25505 . . . . . . 7  class btw
133100, 132cfv 5221 . . . . . 6  class  (btw `  g )
134131, 41, 133wsbc 2992 . . . . 5  wff  [. (btw `  g )  /  q ]. [. (ray `  g
)  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g )  / 
t ]. [. ( line `  g )  /  l ]. [. (angle `  g
)  /  u ]. [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
135 cpoints 25455 . . . . . 6  class PPoints
136100, 135cfv 5221 . . . . 5  class  (PPoints `  g
)
137134, 56, 136wsbc 2992 . . . 4  wff  [. (PPoints `  g )  /  p ]. [. (btw `  g
)  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
138 cangc 25582 . . . . 5  class angc
139100, 138cfv 5221 . . . 4  class  (angc `  g )
140137, 12, 139wsbc 2992 . . 3  wff  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )
141 cibg 25506 . . 3  class Ibg
142140, 99, 141crab 2548 . 2  class  { g  e. Ibg  |  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) }
1431, 142wceq 1628 1  wff Ibcg  =  {
g  e. Ibg  |  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isibcg  25590
  Copyright terms: Public domain W3C validator