Metamath Proof Explorer

Theorem meetcomALT

Description: The meet of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	meetcom.b	$⊢ B = {Base}_{K}$
		meetcom.m	$⊢ \underset{˙}{\land} = meet (K)$
	Assertion	meetcomALT	$⊢ (K \in V \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$

Proof

Step	Hyp	Ref	Expression
1		meetcom.b	$⊢ B = {Base}_{K}$
2		meetcom.m	$⊢ \underset{˙}{\land} = meet (K)$
3		prcom	$⊢ \{Y, X\} = \{X, Y\}$
4	3	fveq2i	$⊢ glb (K) (\{Y, X\}) = glb (K) (\{X, Y\})$
5	4	a1i	$⊢ (K \in V \land X \in B \land Y \in B) \to glb (K) (\{Y, X\}) = glb (K) (\{X, Y\})$
6		eqid	$⊢ glb (K) = glb (K)$
7		simp1	$⊢ (K \in V \land X \in B \land Y \in B) \to K \in V$
8		simp3	$⊢ (K \in V \land X \in B \land Y \in B) \to Y \in B$
9		simp2	$⊢ (K \in V \land X \in B \land Y \in B) \to X \in B$
10	6 2 7 8 9	meetval	$⊢ (K \in V \land X \in B \land Y \in B) \to Y \underset{˙}{\land} X = glb (K) (\{Y, X\})$
11	6 2 7 9 8	meetval	$⊢ (K \in V \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
12	5 10 11	3eqtr4rd	$⊢ (K \in V \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$