Metamath Proof Explorer


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 𝐵 = ( Base ‘ 𝐾 )
joincom.j = ( join ‘ 𝐾 )
Assertion joincom ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ) ) → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )

Proof

Step Hyp Ref Expression
1 joincom.b 𝐵 = ( Base ‘ 𝐾 )
2 joincom.j = ( join ‘ 𝐾 )
3 1 2 joincomALT ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )
4 3 adantr ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ) ) → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )