Metamath Proof Explorer


Theorem leat

Description: A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013)

Ref Expression
Hypotheses leatom.b B = Base K
leatom.l ˙ = K
leatom.z 0 ˙ = 0. K
leatom.a A = Atoms K
Assertion leat K OP X B P A X ˙ P X = P X = 0 ˙

Proof

Step Hyp Ref Expression
1 leatom.b B = Base K
2 leatom.l ˙ = K
3 leatom.z 0 ˙ = 0. K
4 leatom.a A = Atoms K
5 1 2 3 4 leatb K OP X B P A X ˙ P X = P X = 0 ˙
6 5 biimpa K OP X B P A X ˙ P X = P X = 0 ˙