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

Metamath Proof Explorer

Theorem hsupss

Description: Subset relation for supremum of Hilbert space subsets. (Contributed by NM, 24-Nov-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hsupss 
|- ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( A C_ B -> ( \/H ` A ) C_ ( \/H ` B ) ) )

Proof

Step Hyp Ref Expression
1 uniss 
 |-  ( A C_ B -> U. A C_ U. B )
2 sspwuni 
 |-  ( A C_ ~P ~H <-> U. A C_ ~H )
3 sspwuni 
 |-  ( B C_ ~P ~H <-> U. B C_ ~H )
4 occon2 
 |-  ( ( U. A C_ ~H /\ U. B C_ ~H ) -> ( U. A C_ U. B -> ( _|_ ` ( _|_ ` U. A ) ) C_ ( _|_ ` ( _|_ ` U. B ) ) ) )
5 2 3 4 syl2anb 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( U. A C_ U. B -> ( _|_ ` ( _|_ ` U. A ) ) C_ ( _|_ ` ( _|_ ` U. B ) ) ) )
6 1 5 syl5 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( A C_ B -> ( _|_ ` ( _|_ ` U. A ) ) C_ ( _|_ ` ( _|_ ` U. B ) ) ) )
7 hsupval 
 |-  ( A C_ ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )
8 7 adantr 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )
9 hsupval 
 |-  ( B C_ ~P ~H -> ( \/H ` B ) = ( _|_ ` ( _|_ ` U. B ) ) )
10 9 adantl 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( \/H ` B ) = ( _|_ ` ( _|_ ` U. B ) ) )
11 8 10 sseq12d 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( ( \/H ` A ) C_ ( \/H ` B ) <-> ( _|_ ` ( _|_ ` U. A ) ) C_ ( _|_ ` ( _|_ ` U. B ) ) ) )
12 6 11 sylibrd 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( A C_ B -> ( \/H ` A ) C_ ( \/H ` B ) ) )