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 ) ) )