This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem meetcom

Description: The meet of a poset is commutative. (The antecedent <. X , Y >. e. dom ./\ /\ <. Y , X >. e. dom ./\ i.e., "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetcom.b	$⊢ B = {Base}_{K}$
	meetcom.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	meetcom	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\land} \land ⟨Y, X⟩ \in dom \underset{˙}{\land})) \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	1 2	meetcomALT	$⊢ (K \in Poset \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
4	3	adantr	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\land} \land ⟨Y, X⟩ \in dom \underset{˙}{\land})) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$