Theorem joincom

Description: The join of a poset is commutative. (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 = ( Base ` K )
	joincom.j	|- .\/ = ( join ` K )
Assertion	joincom	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ ( <. X , Y >. e. dom .\/ /\ <. Y , X >. e. dom .\/ ) ) -> ( X .\/ Y ) = ( Y .\/ X ) )

Proof

Step	Hyp	Ref	Expression
1		joincom.b	|- B = ( Base ` K )
2		joincom.j	|- .\/ = ( join ` K )
3	1 2	joincomALT	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) = ( Y .\/ X ) )
4	3	adantr	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ ( <. X , Y >. e. dom .\/ /\ <. Y , X >. e. dom .\/ ) ) -> ( X .\/ Y ) = ( Y .\/ X ) )