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ℋ ) ) )