Metamath Proof Explorer


Theorem atss

Description: A lattice element smaller than an atom is either the atom or zero. (Contributed by NM, 25-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atss A C B HAtoms A B A = B A = 0

Proof

Step Hyp Ref Expression
1 elat2 B HAtoms B C B 0 x C x B x = B x = 0
2 sseq1 x = A x B A B
3 eqeq1 x = A x = B A = B
4 eqeq1 x = A x = 0 A = 0
5 3 4 orbi12d x = A x = B x = 0 A = B A = 0
6 2 5 imbi12d x = A x B x = B x = 0 A B A = B A = 0
7 6 rspcv A C x C x B x = B x = 0 A B A = B A = 0
8 7 adantld A C B 0 x C x B x = B x = 0 A B A = B A = 0
9 8 adantld A C B C B 0 x C x B x = B x = 0 A B A = B A = 0
10 9 imp A C B C B 0 x C x B x = B x = 0 A B A = B A = 0
11 1 10 sylan2b A C B HAtoms A B A = B A = 0