Theorem meetle

Description: A meet is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		meetle.b	$$⊢B={\mathrm{Base}}_K$$
2		meetle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		meetle.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		meetle.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		meetle.x	$$⊢\phi \to X\in B$$
6		meetle.y	$$⊢\phi \to Y\in B$$
7		meetle.z	$$⊢\phi \to Z\in B$$
8		meetle.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
9		breq1	$$⊢z=Z\to \left(z\underset{\dot{}}{\le }X\leftrightarrow Z\underset{\dot{}}{\le }X\right)$$
10		breq1	$$⊢z=Z\to \left(z\underset{\dot{}}{\le }Y\leftrightarrow Z\underset{\dot{}}{\le }Y\right)$$
11	9 10	anbi12d	$$⊢z=Z\to \left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(Z\underset{\dot{}}{\le }X\wedge Z\underset{\dot{}}{\le }Y\right)\right)$$
12		breq1	$$⊢z=Z\to \left(z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\leftrightarrow Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\right)$$
13	11 12	imbi12d	$$⊢z=Z\to \left(\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)\leftrightarrow \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)$$
14	1 2 3 4 5 6 8	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)$$
15	14	simprd	$$⊢\phi \to \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)$$
16	13 15 7	rspcdva	$$⊢\phi \to \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)$$
17	1 2 3 4 5 6 8	lemeet1	$$⊢\phi \to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X$$
18	1 3 4 5 6 8	meetcl	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y\in B$$
19	1 2	postr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(Z\in B\wedge X\underset{\dot{}}{\wedge }Y\in B\wedge X\in B\right)\right)\to \left(\left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\right)\to Z\underset{\dot{}}{\le }X\right)$$
20	4 7 18 5 19	syl13anc	$$⊢\phi \to \left(\left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\right)\to Z\underset{\dot{}}{\le }X\right)$$
21	17 20	mpan2d	$$⊢\phi \to \left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\to Z\underset{\dot{}}{\le }X\right)$$
22	1 2 3 4 5 6 8	lemeet2	$$⊢\phi \to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y$$
23	1 2	postr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(Z\in B\wedge X\underset{\dot{}}{\wedge }Y\in B\wedge Y\in B\right)\right)\to \left(\left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y\right)\to Z\underset{\dot{}}{\le }Y\right)$$
24	4 7 18 6 23	syl13anc	$$⊢\phi \to \left(\left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y\right)\to Z\underset{\dot{}}{\le }Y\right)$$
25	22 24	mpan2d	$$⊢\phi \to \left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\to Z\underset{\dot{}}{\le }Y\right)$$
26	21 25	jcad	$$⊢\phi \to \left(Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\to \left(Z\underset{\dot{}}{\le }X\wedge Z\underset{\dot{}}{\le }Y\right)\right)$$
27	16 26	impbid	$$⊢\phi \to \left(\left(Z\underset{\dot{}}{\le }X\wedge Z\underset{\dot{}}{\le }Y\right)\leftrightarrow Z\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }Y\right)\right)$$