This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcvnbtwn

Description: The covers relation implies no in-betweenness. ( cvnbtwn analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lcvnbtwn.s 
|- S = ( LSubSp ` W )
lcvnbtwn.c 
|- C = (
    lcvnbtwn.w 
    |- ( ph -> W e. X )
    lcvnbtwn.r 
    |- ( ph -> R e. S )
    lcvnbtwn.t 
    |- ( ph -> T e. S )
    lcvnbtwn.u 
    |- ( ph -> U e. S )
    lcvnbtwn.d 
    |- ( ph -> R C T )
    Assertion lcvnbtwn 
    |- ( ph -> -. ( R C. U /\ U C. T ) )

    Proof

    Step Hyp Ref Expression
    1 lcvnbtwn.s 
     |-  S = ( LSubSp ` W )
    2 lcvnbtwn.c 
     |-  C = (
      3 lcvnbtwn.w 
       |-  ( ph -> W e. X )
      4 lcvnbtwn.r 
       |-  ( ph -> R e. S )
      5 lcvnbtwn.t 
       |-  ( ph -> T e. S )
      6 lcvnbtwn.u 
       |-  ( ph -> U e. S )
      7 lcvnbtwn.d 
       |-  ( ph -> R C T )
      8 1 2 3 4 5 lcvbr 
       |-  ( ph -> ( R C T <-> ( R C. T /\ -. E. u e. S ( R C. u /\ u C. T ) ) ) )
      9 7 8 mpbid 
       |-  ( ph -> ( R C. T /\ -. E. u e. S ( R C. u /\ u C. T ) ) )
      10 9 simprd 
       |-  ( ph -> -. E. u e. S ( R C. u /\ u C. T ) )
      11 psseq2 
       |-  ( u = U -> ( R C. u <-> R C. U ) )
      12 psseq1 
       |-  ( u = U -> ( u C. T <-> U C. T ) )
      13 11 12 anbi12d 
       |-  ( u = U -> ( ( R C. u /\ u C. T ) <-> ( R C. U /\ U C. T ) ) )
      14 13 rspcev 
       |-  ( ( U e. S /\ ( R C. U /\ U C. T ) ) -> E. u e. S ( R C. u /\ u C. T ) )
      15 6 14 sylan 
       |-  ( ( ph /\ ( R C. U /\ U C. T ) ) -> E. u e. S ( R C. u /\ u C. T ) )
      16 10 15 mtand 
       |-  ( ph -> -. ( R C. U /\ U C. T ) )