Theorem atcvr0

Description: An atom covers zero. ( atcv0 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	atomcvr0.z	|- .0. = ( 0. ` K )
	atomcvr0.c	|- C = (
	atomcvr0.a	|- A = ( Atoms ` K )
Assertion	atcvr0	|- ( ( K e. D /\ P e. A ) -> .0. C P )

Proof

Step	Hyp	Ref	Expression
1		atomcvr0.z	|- .0. = ( 0. ` K )
2		atomcvr0.c	|- C = (
3		atomcvr0.a	|- A = ( Atoms ` K )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1 2 3	isat	|- ( K e. D -> ( P e. A <-> ( P e. ( Base ` K ) /\ .0. C P ) ) )
6	5	simplbda	|- ( ( K e. D /\ P e. A ) -> .0. C P )