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 e. AtLat -> B e. 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	|- ( le ` K ) = ( le ` K )
5		eqid	|- ( 0. ` K ) = ( 0. ` K )
6		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
7	1 3 4 5 6	isatl	|- ( K e. AtLat <-> ( K e. Lat /\ B e. dom G /\ A. x e. B ( x =/= ( 0. ` K ) -> E. y e. ( Atoms ` K ) y ( le ` K ) x ) ) )
8	7	simp2bi	|- ( K e. AtLat -> B e. dom G )