Theorem atl0dm

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

	Ref	Expression
Hypotheses	atl01dm.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atl01dm.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	atl01dm.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion	atl0dm	⊢ ( 𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		atl01dm.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		atl01dm.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		atl01dm.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	1 3 4 5 6	isatl	⊢ ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ ( 0. ‘ 𝐾 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝐾 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ) ) )
8	7	simp2bi	⊢ ( 𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺 )