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

Definition df-ibg2 25462
Description: Definition of a geometry that can build on the axioms of incidence and betweenness. Axioms B-1, B-2, B-3, B-4 of [AitkenIBG] p. 3-4. (For my private use only. Don't use.) (Contributed by FL, 1-Apr-2016.)
Assertion
Ref Expression
df-ibg2  |- Ibg  =  {
f  e. Ig  |  [. (PPoints `  f )  /  g ]. [. (PLines `  f
)  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) }
Distinct variable group:    a, b, c, d, e, f, g, h, l, p, q, r

Detailed syntax breakdown of Definition df-ibg2
StepHypRef Expression
1 cibg 25460 . 2  class Ibg
2 vp . . . . . . . . . . . . 13  set  p
32cv 1618 . . . . . . . . . . . 12  class  p
4 vq . . . . . . . . . . . . 13  set  q
54cv 1618 . . . . . . . . . . . 12  class  q
63, 5wne 2419 . . . . . . . . . . 11  wff  p  =/=  q
7 va . . . . . . . . . . . . . . . . . 18  set  a
87cv 1618 . . . . . . . . . . . . . . . . 17  class  a
9 ve . . . . . . . . . . . . . . . . . 18  set  e
109cv 1618 . . . . . . . . . . . . . . . . 17  class  e
118, 5, 10co 5778 . . . . . . . . . . . . . . . 16  class  ( a e q )
123, 11wcel 1621 . . . . . . . . . . . . . . 15  wff  p  e.  ( a e q )
13 vb . . . . . . . . . . . . . . . . 17  set  b
1413cv 1618 . . . . . . . . . . . . . . . 16  class  b
153, 5, 10co 5778 . . . . . . . . . . . . . . . 16  class  ( p e q )
1614, 15wcel 1621 . . . . . . . . . . . . . . 15  wff  b  e.  ( p e q )
17 vc . . . . . . . . . . . . . . . . . 18  set  c
1817cv 1618 . . . . . . . . . . . . . . . . 17  class  c
193, 18, 10co 5778 . . . . . . . . . . . . . . . 16  class  ( p e c )
205, 19wcel 1621 . . . . . . . . . . . . . . 15  wff  q  e.  ( p e c )
2112, 16, 20w3a 939 . . . . . . . . . . . . . 14  wff  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) )
22 vg . . . . . . . . . . . . . . 15  set  g
2322cv 1618 . . . . . . . . . . . . . 14  class  g
2421, 17, 23wrex 2517 . . . . . . . . . . . . 13  wff  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) )
2524, 13, 23wrex 2517 . . . . . . . . . . . 12  wff  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) )
2625, 7, 23wrex 2517 . . . . . . . . . . 11  wff  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) )
276, 26wi 6 . . . . . . . . . 10  wff  ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )
28 vr . . . . . . . . . . . . . . . . 17  set  r
2928cv 1618 . . . . . . . . . . . . . . . 16  class  r
303, 5, 29ctp 3602 . . . . . . . . . . . . . . 15  class  { p ,  q ,  r }
31 vd . . . . . . . . . . . . . . . 16  set  d
3231cv 1618 . . . . . . . . . . . . . . 15  class  d
3330, 32wcel 1621 . . . . . . . . . . . . . 14  wff  { p ,  q ,  r }  e.  d
343, 29wne 2419 . . . . . . . . . . . . . . 15  wff  p  =/=  r
355, 29wne 2419 . . . . . . . . . . . . . . 15  wff  q  =/=  r
366, 34, 35w3a 939 . . . . . . . . . . . . . 14  wff  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r )
3733, 36wa 360 . . . . . . . . . . . . 13  wff  ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) )
385, 29, 10co 5778 . . . . . . . . . . . . . . . 16  class  ( q e r )
393, 38wcel 1621 . . . . . . . . . . . . . . 15  wff  p  e.  ( q e r )
403, 29, 10co 5778 . . . . . . . . . . . . . . . 16  class  ( p e r )
415, 40wnel 2420 . . . . . . . . . . . . . . 15  wff  q  e/  ( p e r )
4229, 15wnel 2420 . . . . . . . . . . . . . . 15  wff  r  e/  ( p e q )
4339, 41, 42w3a 939 . . . . . . . . . . . . . 14  wff  ( p  e.  ( q e r )  /\  q  e/  ( p e r )  /\  r  e/  ( p e q ) )
443, 38wnel 2420 . . . . . . . . . . . . . . 15  wff  p  e/  ( q e r )
455, 40wcel 1621 . . . . . . . . . . . . . . 15  wff  q  e.  ( p e r )
4644, 45, 42w3a 939 . . . . . . . . . . . . . 14  wff  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )
4729, 15wcel 1621 . . . . . . . . . . . . . . 15  wff  r  e.  ( p e q )
4844, 41, 47w3a 939 . . . . . . . . . . . . . 14  wff  ( p  e/  ( q e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) )
4943, 46, 48w3o 938 . . . . . . . . . . . . 13  wff  ( ( p  e.  ( q e r )  /\  q  e/  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e.  ( p
e r )  /\  r  e/  ( p e q ) )  \/  ( p  e/  (
q e r )  /\  q  e/  (
p e r )  /\  r  e.  ( p e q ) ) )
5037, 49wi 6 . . . . . . . . . . . 12  wff  ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) )  -> 
( ( p  e.  ( q e r )  /\  q  e/  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e.  ( p
e r )  /\  r  e/  ( p e q ) )  \/  ( p  e/  (
q e r )  /\  q  e/  (
p e r )  /\  r  e.  ( p e q ) ) ) )
5129, 3, 10co 5778 . . . . . . . . . . . . . . 15  class  ( r e p )
525, 51wcel 1621 . . . . . . . . . . . . . 14  wff  q  e.  ( r e p )
5352, 33, 36w3a 939 . . . . . . . . . . . . 13  wff  ( q  e.  ( r e p )  /\  {
p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) )
5445, 53wi 6 . . . . . . . . . . . 12  wff  ( q  e.  ( p e r )  ->  (
q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) ) )
55 vl . . . . . . . . . . . . . . . . 17  set  l
5655cv 1618 . . . . . . . . . . . . . . . 16  class  l
573, 56wnel 2420 . . . . . . . . . . . . . . 15  wff  p  e/  l
585, 56wnel 2420 . . . . . . . . . . . . . . 15  wff  q  e/  l
5929, 56wnel 2420 . . . . . . . . . . . . . . 15  wff  r  e/  l
6057, 58, 59w3a 939 . . . . . . . . . . . . . 14  wff  ( p  e/  l  /\  q  e/  l  /\  r  e/  l )
6115, 56cin 3112 . . . . . . . . . . . . . . . . . 18  class  ( ( p e q )  i^i  l )
62 c0 3416 . . . . . . . . . . . . . . . . . 18  class  (/)
6361, 62wceq 1619 . . . . . . . . . . . . . . . . 17  wff  ( ( p e q )  i^i  l )  =  (/)
6438, 56cin 3112 . . . . . . . . . . . . . . . . . 18  class  ( ( q e r )  i^i  l )
6564, 62wceq 1619 . . . . . . . . . . . . . . . . 17  wff  ( ( q e r )  i^i  l )  =  (/)
6663, 65wa 360 . . . . . . . . . . . . . . . 16  wff  ( ( ( p e q )  i^i  l )  =  (/)  /\  (
( q e r )  i^i  l )  =  (/) )
6740, 56cin 3112 . . . . . . . . . . . . . . . . 17  class  ( ( p e r )  i^i  l )
6867, 62wceq 1619 . . . . . . . . . . . . . . . 16  wff  ( ( p e r )  i^i  l )  =  (/)
6966, 68wi 6 . . . . . . . . . . . . . . 15  wff  ( ( ( ( p e q )  i^i  l
)  =  (/)  /\  (
( q e r )  i^i  l )  =  (/) )  ->  (
( p e r )  i^i  l )  =  (/) )
7061, 62wne 2419 . . . . . . . . . . . . . . . . 17  wff  ( ( p e q )  i^i  l )  =/=  (/)
7164, 62wne 2419 . . . . . . . . . . . . . . . . 17  wff  ( ( q e r )  i^i  l )  =/=  (/)
7270, 71wa 360 . . . . . . . . . . . . . . . 16  wff  ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )
7372, 68wi 6 . . . . . . . . . . . . . . 15  wff  ( ( ( ( p e q )  i^i  l
)  =/=  (/)  /\  (
( q e r )  i^i  l )  =/=  (/) )  ->  (
( p e r )  i^i  l )  =  (/) )
7469, 73wa 360 . . . . . . . . . . . . . 14  wff  ( ( ( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) )
7560, 74wi 6 . . . . . . . . . . . . 13  wff  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l )  ->  (
( ( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l )  =  (/) )  ->  ( ( p e r )  i^i  l )  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  ->  ( ( p e r )  i^i  l )  =  (/) ) ) )
76 vh . . . . . . . . . . . . . 14  set  h
7776cv 1618 . . . . . . . . . . . . 13  class  h
7875, 55, 77wral 2516 . . . . . . . . . . . 12  wff  A. l  e.  h  ( (
p  e/  l  /\  q  e/  l  /\  r  e/  l )  ->  (
( ( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l )  =  (/) )  ->  ( ( p e r )  i^i  l )  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  ->  ( ( p e r )  i^i  l )  =  (/) ) ) )
7950, 54, 78w3a 939 . . . . . . . . . . 11  wff  ( ( ( { p ,  q ,  r }  e.  d  /\  (
p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) )  -> 
( ( p  e.  ( q e r )  /\  q  e/  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e.  ( p
e r )  /\  r  e/  ( p e q ) )  \/  ( p  e/  (
q e r )  /\  q  e/  (
p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) )
8079, 28, 23wral 2516 . . . . . . . . . 10  wff  A. r  e.  g  ( (
( { p ,  q ,  r }  e.  d  /\  (
p  =/=  q  /\  p  =/=  r  /\  q  =/=  r ) )  -> 
( ( p  e.  ( q e r )  /\  q  e/  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e.  ( p
e r )  /\  r  e/  ( p e q ) )  \/  ( p  e/  (
q e r )  /\  q  e/  (
p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) )
8127, 80wa 360 . . . . . . . . 9  wff  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g 
( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
8281, 4, 23wral 2516 . . . . . . . 8  wff  A. q  e.  g  ( (
p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g 
( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
8382, 2, 23wral 2516 . . . . . . 7  wff  A. p  e.  g  A. q  e.  g  ( (
p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g 
( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
84 vf . . . . . . . . 9  set  f
8584cv 1618 . . . . . . . 8  class  f
86 cbtw 25459 . . . . . . . 8  class btw
8785, 86cfv 4659 . . . . . . 7  class  (btw `  f )
8883, 9, 87wsbc 2952 . . . . . 6  wff  [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
89 ccol 25443 . . . . . . 7  class coln
9085, 89cfv 4659 . . . . . 6  class  (coln `  f )
9188, 31, 90wsbc 2952 . . . . 5  wff  [. (coln `  f )  /  d ]. [. (btw `  f
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
92 cplines 25411 . . . . . 6  class PLines
9385, 92cfv 4659 . . . . 5  class  (PLines `  f )
9491, 76, 93wsbc 2952 . . . 4  wff  [. (PLines `  f )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
95 cpoints 25409 . . . . 5  class PPoints
9685, 95cfv 4659 . . . 4  class  (PPoints `  f
)
9794, 22, 96wsbc 2952 . . 3  wff  [. (PPoints `  f )  /  g ]. [. (PLines `  f
)  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )
98 cig 25413 . . 3  class Ig
9997, 84, 98crab 2520 . 2  class  { f  e. Ig  |  [. (PPoints `  f )  /  g ]. [. (PLines `  f
)  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) }
1001, 99wceq 1619 1  wff Ibg  =  {
f  e. Ig  |  [. (PPoints `  f )  /  g ]. [. (PLines `  f
)  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isibg2  25463
  Copyright terms: Public domain W3C validator