Metamath Proof Explorer


Theorem leatb

Description: A poset element less than or equal to an atom equals either zero or the atom. ( atss analog.) (Contributed by NM, 17-Nov-2011)

Ref Expression
Hypotheses leatom.b B = Base K
leatom.l ˙ = K
leatom.z 0 ˙ = 0. K
leatom.a A = Atoms K
Assertion leatb 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 op0le K OP X B 0 ˙ ˙ X
6 5 3adant3 K OP X B P A 0 ˙ ˙ X
7 6 biantrurd K OP X B P A X ˙ P 0 ˙ ˙ X X ˙ P
8 opposet K OP K Poset
9 8 3ad2ant1 K OP X B P A K Poset
10 1 3 op0cl K OP 0 ˙ B
11 1 4 atbase P A P B
12 id X B X B
13 10 11 12 3anim123i K OP P A X B 0 ˙ B P B X B
14 13 3com23 K OP X B P A 0 ˙ B P B X B
15 eqid K = K
16 3 15 4 atcvr0 K OP P A 0 ˙ K P
17 16 3adant2 K OP X B P A 0 ˙ K P
18 1 2 15 cvrnbtwn4 K Poset 0 ˙ B P B X B 0 ˙ K P 0 ˙ ˙ X X ˙ P 0 ˙ = X X = P
19 9 14 17 18 syl3anc K OP X B P A 0 ˙ ˙ X X ˙ P 0 ˙ = X X = P
20 eqcom 0 ˙ = X X = 0 ˙
21 20 orbi1i 0 ˙ = X X = P X = 0 ˙ X = P
22 19 21 bitrdi K OP X B P A 0 ˙ ˙ X X ˙ P X = 0 ˙ X = P
23 7 22 bitrd K OP X B P A X ˙ P X = 0 ˙ X = P
24 orcom X = 0 ˙ X = P X = P X = 0 ˙
25 23 24 bitrdi K OP X B P A X ˙ P X = P X = 0 ˙