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

Theorem lppotoslem 26246
Description: To show that a point doesn't belong to a line  M 2. (For my private use only. Don't use.) (Contributed by FL, 14-Jul-2016.)
Hypotheses
Ref Expression
lppotoslem.6  |-  ( ph  ->  ( M1  i^i  M 2 )  =  { X } )
lppotoslem.8  |-  ( ph  ->  Y  e.  M1 )
lppotoslem.9  |-  ( ph  ->  X  =/=  Y )
Assertion
Ref Expression
lppotoslem  |-  ( ph  ->  -.  Y  e.  M 2 )

Proof of Theorem lppotoslem
StepHypRef Expression
1 lppotoslem.8 . . 3  |-  ( ph  ->  Y  e.  M1 )
2 elin 3371 . . . . . 6  |-  ( Y  e.  ( M1  i^i  M 2 )  <->  ( Y  e.  M1  /\  Y  e.  M 2 ) )
3 lppotoslem.6 . . . . . . . . 9  |-  ( ph  ->  ( M1  i^i  M 2 )  =  { X } )
43eleq2d 2363 . . . . . . . 8  |-  ( ph  ->  ( Y  e.  (
M1  i^i  M 2
)  <->  Y  e.  { X } ) )
5 elsni 3677 . . . . . . . . 9  |-  ( Y  e.  { X }  ->  Y  =  X )
6 lppotoslem.9 . . . . . . . . . . . 12  |-  ( ph  ->  X  =/=  Y )
7 df-ne 2461 . . . . . . . . . . . . 13  |-  ( X  =/=  Y  <->  -.  X  =  Y )
8 pm2.21 100 . . . . . . . . . . . . 13  |-  ( -.  X  =  Y  -> 
( X  =  Y  ->  -.  Y  e.  M 2 ) )
97, 8sylbi 187 . . . . . . . . . . . 12  |-  ( X  =/=  Y  ->  ( X  =  Y  ->  -.  Y  e.  M 2
) )
106, 9syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( X  =  Y  ->  -.  Y  e.  M 2 ) )
1110com12 27 . . . . . . . . . 10  |-  ( X  =  Y  ->  ( ph  ->  -.  Y  e.  M 2 ) )
1211eqcoms 2299 . . . . . . . . 9  |-  ( Y  =  X  ->  ( ph  ->  -.  Y  e.  M 2 ) )
135, 12syl 15 . . . . . . . 8  |-  ( Y  e.  { X }  ->  ( ph  ->  -.  Y  e.  M 2
) )
144, 13syl6bi 219 . . . . . . 7  |-  ( ph  ->  ( Y  e.  (
M1  i^i  M 2
)  ->  ( ph  ->  -.  Y  e.  M 2 ) ) )
1514pm2.43b 46 . . . . . 6  |-  ( Y  e.  ( M1  i^i  M 2 )  ->  ( ph  ->  -.  Y  e.  M 2 ) )
162, 15sylbir 204 . . . . 5  |-  ( ( Y  e.  M1  /\  Y  e.  M 2 )  -> 
( ph  ->  -.  Y  e.  M 2 ) )
1716ex 423 . . . 4  |-  ( Y  e.  M1  ->  ( Y  e.  M 2  ->  (
ph  ->  -.  Y  e.  M 2 ) ) )
1817com23 72 . . 3  |-  ( Y  e.  M1  ->  ( ph  ->  ( Y  e.  M 2  ->  -.  Y  e.  M 2 ) ) )
191, 18mpcom 32 . 2  |-  ( ph  ->  ( Y  e.  M 2  ->  -.  Y  e.  M 2 ) )
2019pm2.01d 161 1  |-  ( ph  ->  -.  Y  e.  M 2 )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459    i^i cin 3164   {csn 3653
This theorem is referenced by:  lppotos  26247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-in 3172  df-sn 3659
  Copyright terms: Public domain W3C validator