MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-plig Unicode version

Definition df-plig 20843
Description: Planar incidence geometry. I use Hilbert's "axioms" adapted to planar geometry.  e. is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf (Contributed by FL, 2-Aug-2009.)
Assertion
Ref Expression
df-plig  |-  Plig  =  { x  |  ( A. a  e.  U. x A. b  e.  U. x
( a  =/=  b  ->  E! l  e.  x  ( a  e.  l  /\  b  e.  l ) )  /\  A. l  e.  x  E. a  e.  U. x E. b  e.  U. x
( a  =/=  b  /\  a  e.  l  /\  b  e.  l
)  /\  E. a  e.  U. x E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
) }
Distinct variable group:    x, a, b, l, c

Detailed syntax breakdown of Definition df-plig
StepHypRef Expression
1 cplig 20842 . 2  class  Plig
2 va . . . . . . . . 9  set  a
32cv 1622 . . . . . . . 8  class  a
4 vb . . . . . . . . 9  set  b
54cv 1622 . . . . . . . 8  class  b
63, 5wne 2446 . . . . . . 7  wff  a  =/=  b
7 vl . . . . . . . . . 10  set  l
82, 7wel 1685 . . . . . . . . 9  wff  a  e.  l
94, 7wel 1685 . . . . . . . . 9  wff  b  e.  l
108, 9wa 358 . . . . . . . 8  wff  ( a  e.  l  /\  b  e.  l )
11 vx . . . . . . . . 9  set  x
1211cv 1622 . . . . . . . 8  class  x
1310, 7, 12wreu 2545 . . . . . . 7  wff  E! l  e.  x  ( a  e.  l  /\  b  e.  l )
146, 13wi 4 . . . . . 6  wff  ( a  =/=  b  ->  E! l  e.  x  (
a  e.  l  /\  b  e.  l )
)
1512cuni 3827 . . . . . 6  class  U. x
1614, 4, 15wral 2543 . . . . 5  wff  A. b  e.  U. x ( a  =/=  b  ->  E! l  e.  x  (
a  e.  l  /\  b  e.  l )
)
1716, 2, 15wral 2543 . . . 4  wff  A. a  e.  U. x A. b  e.  U. x ( a  =/=  b  ->  E! l  e.  x  (
a  e.  l  /\  b  e.  l )
)
186, 8, 9w3a 934 . . . . . . 7  wff  ( a  =/=  b  /\  a  e.  l  /\  b  e.  l )
1918, 4, 15wrex 2544 . . . . . 6  wff  E. b  e.  U. x ( a  =/=  b  /\  a  e.  l  /\  b  e.  l )
2019, 2, 15wrex 2544 . . . . 5  wff  E. a  e.  U. x E. b  e.  U. x ( a  =/=  b  /\  a  e.  l  /\  b  e.  l )
2120, 7, 12wral 2543 . . . 4  wff  A. l  e.  x  E. a  e.  U. x E. b  e.  U. x ( a  =/=  b  /\  a  e.  l  /\  b  e.  l )
22 vc . . . . . . . . . . 11  set  c
2322, 7wel 1685 . . . . . . . . . 10  wff  c  e.  l
248, 9, 23w3a 934 . . . . . . . . 9  wff  ( a  e.  l  /\  b  e.  l  /\  c  e.  l )
2524wn 3 . . . . . . . 8  wff  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
2625, 7, 12wral 2543 . . . . . . 7  wff  A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
2726, 22, 15wrex 2544 . . . . . 6  wff  E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
2827, 4, 15wrex 2544 . . . . 5  wff  E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
2928, 2, 15wrex 2544 . . . 4  wff  E. a  e.  U. x E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
3017, 21, 29w3a 934 . . 3  wff  ( A. a  e.  U. x A. b  e.  U. x
( a  =/=  b  ->  E! l  e.  x  ( a  e.  l  /\  b  e.  l ) )  /\  A. l  e.  x  E. a  e.  U. x E. b  e.  U. x
( a  =/=  b  /\  a  e.  l  /\  b  e.  l
)  /\  E. a  e.  U. x E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
)
3130, 11cab 2269 . 2  class  { x  |  ( A. a  e.  U. x A. b  e.  U. x ( a  =/=  b  ->  E! l  e.  x  (
a  e.  l  /\  b  e.  l )
)  /\  A. l  e.  x  E. a  e.  U. x E. b  e.  U. x ( a  =/=  b  /\  a  e.  l  /\  b  e.  l )  /\  E. a  e.  U. x E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  ( a  e.  l  /\  b  e.  l  /\  c  e.  l ) ) }
321, 31wceq 1623 1  wff  Plig  =  { x  |  ( A. a  e.  U. x A. b  e.  U. x
( a  =/=  b  ->  E! l  e.  x  ( a  e.  l  /\  b  e.  l ) )  /\  A. l  e.  x  E. a  e.  U. x E. b  e.  U. x
( a  =/=  b  /\  a  e.  l  /\  b  e.  l
)  /\  E. a  e.  U. x E. b  e.  U. x E. c  e.  U. x A. l  e.  x  -.  (
a  e.  l  /\  b  e.  l  /\  c  e.  l )
) }
Colors of variables: wff set class
This definition is referenced by:  isplig  20844
  Copyright terms: Public domain W3C validator