Metamath Proof Explorer

Theorem lcvpss

Description: The covers relation implies proper subset. ( cvpss analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lcvfbr.s 
|- S = ( LSubSp ` W )
lcvfbr.c 
|- C = (
    lcvfbr.w 
    |- ( ph -> W e. X )
    lcvfbr.t 
    |- ( ph -> T e. S )
    lcvfbr.u 
    |- ( ph -> U e. S )
    lcvpss.d 
    |- ( ph -> T C U )
    Assertion lcvpss 
    |- ( ph -> T C. U )

    Proof

    Step Hyp Ref Expression
    1 lcvfbr.s 
     |-  S = ( LSubSp ` W )
    2 lcvfbr.c 
     |-  C = (
      3 lcvfbr.w 
       |-  ( ph -> W e. X )
      4 lcvfbr.t 
       |-  ( ph -> T e. S )
      5 lcvfbr.u 
       |-  ( ph -> U e. S )
      6 lcvpss.d 
       |-  ( ph -> T C U )
      7 1 2 3 4 5 lcvbr 
       |-  ( ph -> ( T C U <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )
      8 6 7 mpbid 
       |-  ( ph -> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) )
      9 8 simpld 
       |-  ( ph -> T C. U )