Theorem joincom

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

	Ref	Expression
Hypotheses	joincom.b	$$⊢B={\mathrm{Base}}_K$$
	joincom.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
Assertion	joincom	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\wedge ⟨Y,X⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\right)\right)\to X\underset{\dot{}}{\vee }Y=Y\underset{\dot{}}{\vee }X$$

Proof

Step	Hyp	Ref	Expression
1		joincom.b	$$⊢B={\mathrm{Base}}_K$$
2		joincom.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3	1 2	joincomALT	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\vee }Y=Y\underset{\dot{}}{\vee }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{}}{\vee }\wedge ⟨Y,X⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\right)\right)\to X\underset{\dot{}}{\vee }Y=Y\underset{\dot{}}{\vee }X$$