Metamath Proof Explorer


Theorem lejoin2

Description: A join's second argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011)

Ref Expression
Hypotheses joinval2.b
|- B = ( Base ` K )
joinval2.l
|- .<_ = ( le ` K )
joinval2.j
|- .\/ = ( join ` K )
joinval2.k
|- ( ph -> K e. V )
joinval2.x
|- ( ph -> X e. B )
joinval2.y
|- ( ph -> Y e. B )
joinlem.e
|- ( ph -> <. X , Y >. e. dom .\/ )
Assertion lejoin2
|- ( ph -> Y .<_ ( X .\/ Y ) )

Proof

Step Hyp Ref Expression
1 joinval2.b
 |-  B = ( Base ` K )
2 joinval2.l
 |-  .<_ = ( le ` K )
3 joinval2.j
 |-  .\/ = ( join ` K )
4 joinval2.k
 |-  ( ph -> K e. V )
5 joinval2.x
 |-  ( ph -> X e. B )
6 joinval2.y
 |-  ( ph -> Y e. B )
7 joinlem.e
 |-  ( ph -> <. X , Y >. e. dom .\/ )
8 1 2 3 4 5 6 7 joinlem
 |-  ( ph -> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )
9 8 simplrd
 |-  ( ph -> Y .<_ ( X .\/ Y ) )