Theorem lemeet1

Description: A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetval2.b	|- B = ( Base ` K )
	meetval2.l	|- .<_ = ( le ` K )
	meetval2.m	|- ./\ = ( meet ` K )
	meetval2.k	|- ( ph -> K e. V )
	meetval2.x	|- ( ph -> X e. B )
	meetval2.y	|- ( ph -> Y e. B )
	meetlem.e	|- ( ph -> <. X , Y >. e. dom ./\ )
Assertion	lemeet1	|- ( ph -> ( X ./\ Y ) .<_ X )

Proof

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