Metamath Proof Explorer

Theorem chsupss

Description: Subset relation for supremum of subset of CH . (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsupss 
|- ( ( A C_ CH /\ B C_ CH ) -> ( A C_ B -> ( \/H ` A ) C_ ( \/H ` B ) ) )

Proof

Step Hyp Ref Expression
1 chsspwh 
 |-  CH C_ ~P ~H
2 sstr2 
 |-  ( A C_ CH -> ( CH C_ ~P ~H -> A C_ ~P ~H ) )
3 1 2 mpi 
 |-  ( A C_ CH -> A C_ ~P ~H )
4 sstr2 
 |-  ( B C_ CH -> ( CH C_ ~P ~H -> B C_ ~P ~H ) )
5 1 4 mpi 
 |-  ( B C_ CH -> B C_ ~P ~H )
6 hsupss 
 |-  ( ( A C_ ~P ~H /\ B C_ ~P ~H ) -> ( A C_ B -> ( \/H ` A ) C_ ( \/H ` B ) ) )
7 3 5 6 syl2an 
 |-  ( ( A C_ CH /\ B C_ CH ) -> ( A C_ B -> ( \/H ` A ) C_ ( \/H ` B ) ) )