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 = {Base}_{K}$
	meetle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	meetle.m	$⊢ \underset{˙}{\land} = meet (K)$
	meetle.k	$⊢ φ \to K \in Poset$
	meetle.x	$⊢ φ \to X \in B$
	meetle.y	$⊢ φ \to Y \in B$
	meetle.z	$⊢ φ \to Z \in B$
	meetle.e	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
Assertion	meetle	$⊢ φ \to ((Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y) \leftrightarrow Z \underset{˙}{\leq} (X \underset{˙}{\land} Y))$

Proof

Step	Hyp	Ref	Expression
1		meetle.b	$⊢ B = {Base}_{K}$
2		meetle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		meetle.m	$⊢ \underset{˙}{\land} = meet (K)$
4		meetle.k	$⊢ φ \to K \in Poset$
5		meetle.x	$⊢ φ \to X \in B$
6		meetle.y	$⊢ φ \to Y \in B$
7		meetle.z	$⊢ φ \to Z \in B$
8		meetle.e	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
9		breq1	$⊢ z = Z \to (z \underset{˙}{\leq} X \leftrightarrow Z \underset{˙}{\leq} X)$
10		breq1	$⊢ z = Z \to (z \underset{˙}{\leq} Y \leftrightarrow Z \underset{˙}{\leq} Y)$
11	9 10	anbi12d	$⊢ z = Z \to ((z \underset{˙}{\leq} X \land z \underset{˙}{\leq} Y) \leftrightarrow (Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y))$
12		breq1	$⊢ z = Z \to (z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow Z \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
13	11 12	imbi12d	$⊢ z = Z \to (((z \underset{˙}{\leq} X \land z \underset{˙}{\leq} Y) \to z \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \leftrightarrow ((Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y) \to Z \underset{˙}{\leq} (X \underset{˙}{\land} Y)))$
14	1 2 3 4 5 6 8	meetlem	$⊢ φ \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y) \land \forall z \in B ((z \underset{˙}{\leq} X \land z \underset{˙}{\leq} Y) \to z \underset{˙}{\leq} (X \underset{˙}{\land} Y)))$
15	14	simprd	$⊢ φ \to \forall z \in B ((z \underset{˙}{\leq} X \land z \underset{˙}{\leq} Y) \to z \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
16	13 15 7	rspcdva	$⊢ φ \to ((Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y) \to Z \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
17	1 2 3 4 5 6 8	lemeet1	$⊢ φ \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
18	1 3 4 5 6 8	meetcl	$⊢ φ \to X \underset{˙}{\land} Y \in B$
19	1 2	postr	$⊢ (K \in Poset \land (Z \in B \land X \underset{˙}{\land} Y \in B \land X \in B)) \to ((Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} X) \to Z \underset{˙}{\leq} X)$
20	4 7 18 5 19	syl13anc	$⊢ φ \to ((Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} X) \to Z \underset{˙}{\leq} X)$
21	17 20	mpan2d	$⊢ φ \to (Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \to Z \underset{˙}{\leq} X)$
22	1 2 3 4 5 6 8	lemeet2	$⊢ φ \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
23	1 2	postr	$⊢ (K \in Poset \land (Z \in B \land X \underset{˙}{\land} Y \in B \land Y \in B)) \to ((Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y) \to Z \underset{˙}{\leq} Y)$
24	4 7 18 6 23	syl13anc	$⊢ φ \to ((Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y) \to Z \underset{˙}{\leq} Y)$
25	22 24	mpan2d	$⊢ φ \to (Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \to Z \underset{˙}{\leq} Y)$
26	21 25	jcad	$⊢ φ \to (Z \underset{˙}{\leq} (X \underset{˙}{\land} Y) \to (Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y))$
27	16 26	impbid	$⊢ φ \to ((Z \underset{˙}{\leq} X \land Z \underset{˙}{\leq} Y) \leftrightarrow Z \underset{˙}{\leq} (X \underset{˙}{\land} Y))$

Metamath Proof Explorer

Theorem meetle

Proof