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 ( ( 𝐴 ∈ 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ℋ ) ) )