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

Metamath Proof Explorer

Theorem atl0dm

Description: Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018)

Ref Expression
Hypotheses atl01dm.b ⊢ B = Base K
atl01dm.u ⊢ U = lub ⁡ K
atl01dm.g ⊢ G = glb ⁡ K
Assertion atl0dm ⊢ K ∈ AtLat → B ∈ dom ⁡ G

Proof

Step Hyp Ref Expression
1 atl01dm.b ⊢ B = Base K
2 atl01dm.u ⊢ U = lub ⁡ K
3 atl01dm.g ⊢ G = glb ⁡ K
4 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ 0. ⁡ K = 0. ⁡ K
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 1 3 4 5 6 isatl ⊢ K ∈ AtLat ↔ K ∈ Lat ∧ B ∈ dom ⁡ G ∧ ∀ x ∈ B x ≠ 0. ⁡ K → ∃ y ∈ Atoms ⁡ K y ≤ K x
8 7 simp2bi ⊢ K ∈ AtLat → B ∈ dom ⁡ G