Metamath Proof Explorer


Theorem shsub2

Description: Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsub2 ( ( 𝐴S𝐵S ) → 𝐴 ⊆ ( 𝐵 + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 shsub1 ( ( 𝐴S𝐵S ) → 𝐴 ⊆ ( 𝐴 + 𝐵 ) )
2 shscom ( ( 𝐴S𝐵S ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
3 1 2 sseqtrd ( ( 𝐴S𝐵S ) → 𝐴 ⊆ ( 𝐵 + 𝐴 ) )