Theorem lejoin1

Description: A join's first 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	lejoin1	|- ( ph -> X .<_ ( 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	simplld	|- ( ph -> X .<_ ( X .\/ Y ) )