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 e. CH /\ B e. HAtoms ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )

Proof

Step Hyp Ref Expression
1 elat2 
 |-  ( B e. HAtoms <-> ( B e. CH /\ ( B =/= 0H /\ A. x e. CH ( x C_ B -> ( x = B \/ x = 0H ) ) ) ) )
2 sseq1 
 |-  ( x = A -> ( x C_ B <-> A C_ B ) )
3 eqeq1 
 |-  ( x = A -> ( x = B <-> A = B ) )
4 eqeq1 
 |-  ( x = A -> ( x = 0H <-> A = 0H ) )
5 3 4 orbi12d 
 |-  ( x = A -> ( ( x = B \/ x = 0H ) <-> ( A = B \/ A = 0H ) ) )
6 2 5 imbi12d 
 |-  ( x = A -> ( ( x C_ B -> ( x = B \/ x = 0H ) ) <-> ( A C_ B -> ( A = B \/ A = 0H ) ) ) )
7 6 rspcv 
 |-  ( A e. CH -> ( A. x e. CH ( x C_ B -> ( x = B \/ x = 0H ) ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) ) )
8 7 adantld 
 |-  ( A e. CH -> ( ( B =/= 0H /\ A. x e. CH ( x C_ B -> ( x = B \/ x = 0H ) ) ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) ) )
9 8 adantld 
 |-  ( A e. CH -> ( ( B e. CH /\ ( B =/= 0H /\ A. x e. CH ( x C_ B -> ( x = B \/ x = 0H ) ) ) ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) ) )
10 9 imp 
 |-  ( ( A e. CH /\ ( B e. CH /\ ( B =/= 0H /\ A. x e. CH ( x C_ B -> ( x = B \/ x = 0H ) ) ) ) ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )
11 1 10 sylan2b 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )