Metamath Proof Explorer

Theorem latjcom

Description: The join of a lattice commutes. ( chjcom analog.) (Contributed by NM, 16-Sep-2011)

Ref Expression
Hypotheses latjcom.b ⊢ B = Base K
latjcom.j ⊢ ∨ ˙ = join ⁡ K
Assertion latjcom ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y = Y ∨ ˙ X

Proof

Step Hyp Ref Expression
1 latjcom.b ⊢ B = Base K
2 latjcom.j ⊢ ∨ ˙ = join ⁡ K
3 opelxpi ⊢ X ∈ B ∧ Y ∈ B → X Y ∈ B × B
4 3 3adant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ B × B
5 eqid ⊢ meet ⁡ K = meet ⁡ K
6 1 2 5 islat ⊢ K ∈ Lat ↔ K ∈ Poset ∧ dom ⁡ ∨ ˙ = B × B ∧ dom ⁡ meet ⁡ K = B × B
7 simprl ⊢ K ∈ Poset ∧ dom ⁡ ∨ ˙ = B × B ∧ dom ⁡ meet ⁡ K = B × B → dom ⁡ ∨ ˙ = B × B
8 6 7 sylbi ⊢ K ∈ Lat → dom ⁡ ∨ ˙ = B × B
9 8 3ad2ant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → dom ⁡ ∨ ˙ = B × B
10 4 9 eleqtrrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ dom ⁡ ∨ ˙
11 opelxpi ⊢ Y ∈ B ∧ X ∈ B → Y X ∈ B × B
12 11 ancoms ⊢ X ∈ B ∧ Y ∈ B → Y X ∈ B × B
13 12 3adant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → Y X ∈ B × B
14 13 9 eleqtrrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → Y X ∈ dom ⁡ ∨ ˙
15 10 14 jca ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ dom ⁡ ∨ ˙ ∧ Y X ∈ dom ⁡ ∨ ˙
16 latpos ⊢ K ∈ Lat → K ∈ Poset
17 1 2 joincom ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B ∧ X Y ∈ dom ⁡ ∨ ˙ ∧ Y X ∈ dom ⁡ ∨ ˙ → X ∨ ˙ Y = Y ∨ ˙ X
18 16 17 syl3anl1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ X Y ∈ dom ⁡ ∨ ˙ ∧ Y X ∈ dom ⁡ ∨ ˙ → X ∨ ˙ Y = Y ∨ ˙ X
19 15 18 mpdan ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y = Y ∨ ˙ X