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

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 ⊢ B = Base K
joincom.j ⊢ ∨ ˙ = join ⁡ K
Assertion joincom ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B ∧ X Y ∈ dom ⁡ ∨ ˙ ∧ Y X ∈ 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 ∈ Poset ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y = Y ∨ ˙ X
4 3 adantr ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B ∧ X Y ∈ dom ⁡ ∨ ˙ ∧ Y X ∈ dom ⁡ ∨ ˙ → X ∨ ˙ Y = Y ∨ ˙ X