This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℋ