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