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={\mathrm{Base}}_K$$
	meetval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	meetval2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	meetval2.k	$$⊢\phi \to K\in V$$
	meetval2.x	$$⊢\phi \to X\in B$$
	meetval2.y	$$⊢\phi \to Y\in B$$
	meetlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
Assertion	lemeet1	$$⊢\phi \to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X$$

Proof

Step	Hyp	Ref	Expression
1		meetval2.b	$$⊢B={\mathrm{Base}}_K$$
2		meetval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		meetval2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		meetval2.k	$$⊢\phi \to K\in V$$
5		meetval2.x	$$⊢\phi \to X\in B$$
6		meetval2.y	$$⊢\phi \to Y\in B$$
7		meetlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
8	1 2 3 4 5 6 7	meetlem	$$⊢\phi \to \left(\left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\right)\right)$$
9	8	simplld	$$⊢\phi \to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X$$