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

Metamath Proof Explorer

Theorem spansnss2

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnss2 
|- ( ( A e. SH /\ B e. ~H ) -> ( B e. A <-> ( span ` { B } ) C_ A ) )

Proof

Step Hyp Ref Expression
1 spansnss 
 |-  ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )
2 1 ex 
 |-  ( A e. SH -> ( B e. A -> ( span ` { B } ) C_ A ) )
3 2 adantr 
 |-  ( ( A e. SH /\ B e. ~H ) -> ( B e. A -> ( span ` { B } ) C_ A ) )
4 spansnid 
 |-  ( B e. ~H -> B e. ( span ` { B } ) )
5 ssel 
 |-  ( ( span ` { B } ) C_ A -> ( B e. ( span ` { B } ) -> B e. A ) )
6 4 5 syl5com 
 |-  ( B e. ~H -> ( ( span ` { B } ) C_ A -> B e. A ) )
7 6 adantl 
 |-  ( ( A e. SH /\ B e. ~H ) -> ( ( span ` { B } ) C_ A -> B e. A ) )
8 3 7 impbid 
 |-  ( ( A e. SH /\ B e. ~H ) -> ( B e. A <-> ( span ` { B } ) C_ A ) )