Metamath Proof Explorer


Theorem leat2

Description: A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013)

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

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 orcom X = P X = 0 ˙ X = 0 ˙ X = P
7 neor X = 0 ˙ X = P X 0 ˙ X = P
8 6 7 bitri X = P X = 0 ˙ X 0 ˙ X = P
9 5 8 bitrdi K OP X B P A X ˙ P X 0 ˙ X = P
10 9 biimpd K OP X B P A X ˙ P X 0 ˙ X = P
11 10 com23 K OP X B P A X 0 ˙ X ˙ P X = P
12 11 imp32 K OP X B P A X 0 ˙ X ˙ P X = P