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

Metamath Proof Explorer

Theorem lcvnbtwn3

Description: The covers relation implies no in-betweenness. ( cvnbtwn3 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 )
    lcvnbtwn3.p 
    |- ( ph -> R C_ U )
    lcvnbtwn3.q 
    |- ( ph -> U C. T )
    Assertion lcvnbtwn3 
    |- ( ph -> U = R )

    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 lcvnbtwn3.p 
       |-  ( ph -> R C_ U )
      9 lcvnbtwn3.q 
       |-  ( ph -> U C. T )
      10 1 2 3 4 5 6 7 lcvnbtwn 
       |-  ( ph -> -. ( R C. U /\ U C. T ) )
      11 iman 
       |-  ( ( ( R C_ U /\ U C. T ) -> R = U ) <-> -. ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
      12 eqcom 
       |-  ( U = R <-> R = U )
      13 12 imbi2i 
       |-  ( ( ( R C_ U /\ U C. T ) -> U = R ) <-> ( ( R C_ U /\ U C. T ) -> R = U ) )
      14 dfpss2 
       |-  ( R C. U <-> ( R C_ U /\ -. R = U ) )
      15 14 anbi1i 
       |-  ( ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ -. R = U ) /\ U C. T ) )
      16 an32 
       |-  ( ( ( R C_ U /\ -. R = U ) /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
      17 15 16 bitri 
       |-  ( ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
      18 17 notbii 
       |-  ( -. ( R C. U /\ U C. T ) <-> -. ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
      19 11 13 18 3bitr4ri 
       |-  ( -. ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) -> U = R ) )
      20 10 19 sylib 
       |-  ( ph -> ( ( R C_ U /\ U C. T ) -> U = R ) )
      21 8 9 20 mp2and 
       |-  ( ph -> U = R )