Metamath Proof Explorer


Theorem lemeet2

Description: A meet's second argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-Sep-2018)

Ref Expression
Hypotheses meetval2.b B = Base K
meetval2.l ˙ = K
meetval2.m ˙ = meet K
meetval2.k φ K V
meetval2.x φ X B
meetval2.y φ Y B
meetlem.e φ X Y dom ˙
Assertion lemeet2 φ X ˙ Y ˙ Y

Proof

Step Hyp Ref Expression
1 meetval2.b B = Base K
2 meetval2.l ˙ = K
3 meetval2.m ˙ = meet K
4 meetval2.k φ K V
5 meetval2.x φ X B
6 meetval2.y φ Y B
7 meetlem.e φ X Y dom ˙
8 1 2 3 4 5 6 7 meetlem φ X ˙ Y ˙ X X ˙ Y ˙ Y z B z ˙ X z ˙ Y z ˙ X ˙ Y
9 8 simplrd φ X ˙ Y ˙ Y