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

Metamath Proof Explorer

Theorem meetcomALT

Description: The meet of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses meetcom.b ⊢ B = Base K
meetcom.m ⊢ ∧ ˙ = meet ⁡ K
Assertion meetcomALT ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y = Y ∧ ˙ X

Proof

Step Hyp Ref Expression
1 meetcom.b ⊢ B = Base K
2 meetcom.m ⊢ ∧ ˙ = meet ⁡ K
3 prcom ⊢ Y X = X Y
4 3 fveq2i ⊢ glb ⁡ K ⁡ Y X = glb ⁡ K ⁡ X Y
5 4 a1i ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → glb ⁡ K ⁡ Y X = glb ⁡ K ⁡ X Y
6 eqid ⊢ glb ⁡ K = glb ⁡ K
7 simp1 ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → K ∈ V
8 simp3 ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
9 simp2 ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → X ∈ B
10 6 2 7 8 9 meetval ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → Y ∧ ˙ X = glb ⁡ K ⁡ Y X
11 6 2 7 9 8 meetval ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y = glb ⁡ K ⁡ X Y
12 5 10 11 3eqtr4rd ⊢ K ∈ V ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y = Y ∧ ˙ X