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={\mathrm{Base}}_K$$
	meetcom.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	meetcom	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\wedge ⟨Y,X⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\right)\right)\to X\underset{\dot{}}{\wedge }Y=Y\underset{\dot{}}{\wedge }X$$

Proof

Step	Hyp	Ref	Expression
1		meetcom.b	$$⊢B={\mathrm{Base}}_K$$
2		meetcom.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3	1 2	meetcomALT	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\wedge }Y=Y\underset{\dot{}}{\wedge }X$$
4	3	adantr	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\wedge ⟨Y,X⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\right)\right)\to X\underset{\dot{}}{\wedge }Y=Y\underset{\dot{}}{\wedge }X$$