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 ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 elat2 ( 𝐵 ∈ HAtoms ↔ ( 𝐵C ∧ ( 𝐵 ≠ 0 ∧ ∀ 𝑥C ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) ) ) )
2 sseq1 ( 𝑥 = 𝐴 → ( 𝑥𝐵𝐴𝐵 ) )
3 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵𝐴 = 𝐵 ) )
4 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = 0𝐴 = 0 ) )
5 3 4 orbi12d ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐵𝑥 = 0 ) ↔ ( 𝐴 = 𝐵𝐴 = 0 ) ) )
6 2 5 imbi12d ( 𝑥 = 𝐴 → ( ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) ↔ ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) ) )
7 6 rspcv ( 𝐴C → ( ∀ 𝑥C ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) ) )
8 7 adantld ( 𝐴C → ( ( 𝐵 ≠ 0 ∧ ∀ 𝑥C ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) ) )
9 8 adantld ( 𝐴C → ( ( 𝐵C ∧ ( 𝐵 ≠ 0 ∧ ∀ 𝑥C ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) ) ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) ) )
10 9 imp ( ( 𝐴C ∧ ( 𝐵C ∧ ( 𝐵 ≠ 0 ∧ ∀ 𝑥C ( 𝑥𝐵 → ( 𝑥 = 𝐵𝑥 = 0 ) ) ) ) ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) )
11 1 10 sylan2b ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐴 = 0 ) ) )