Theorem meetcl

Description: Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetcl.b	$$⊢B={\mathrm{Base}}_K$$
	meetcl.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	meetcl.k	$$⊢\phi \to K\in V$$
	meetcl.x	$$⊢\phi \to X\in B$$
	meetcl.y	$$⊢\phi \to Y\in B$$
	meetcl.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
Assertion	meetcl	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		meetcl.b	$$⊢B={\mathrm{Base}}_K$$
2		meetcl.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		meetcl.k	$$⊢\phi \to K\in V$$
4		meetcl.x	$$⊢\phi \to X\in B$$
5		meetcl.y	$$⊢\phi \to Y\in B$$
6		meetcl.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
7		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
8	7 2 3 4 5	meetval	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y=\mathrm{glb}\left(K\right)\left(\left\{X,Y\right\}\right)$$
9	7 2 3 4 5	meetdef	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\leftrightarrow \left\{X,Y\right\}\in \mathrm{dom}\mathrm{glb}\left(K\right)\right)$$
10	6 9	mpbid	$$⊢\phi \to \left\{X,Y\right\}\in \mathrm{dom}\mathrm{glb}\left(K\right)$$
11	1 7 3 10	glbcl	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(\left\{X,Y\right\}\right)\in B$$
12	8 11	eqeltrd	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y\in B$$