Theorem atbase

Description: An atom is a member of the lattice base set (i.e. a lattice element). ( atelch analog.) (Contributed by NM, 10-Oct-2011)

	Ref	Expression
Hypotheses	atombase.b	|- B = ( Base ` K )
	atombase.a	|- A = ( Atoms ` K )
Assertion	atbase	|- ( P e. A -> P e. B )

Proof

Step	Hyp	Ref	Expression
1		atombase.b	|- B = ( Base ` K )
2		atombase.a	|- A = ( Atoms ` K )
3		n0i	|- ( P e. A -> -. A = (/) )
4	2	eqeq1i	|- ( A = (/) <-> ( Atoms ` K ) = (/) )
5	3 4	sylnib	|- ( P e. A -> -. ( Atoms ` K ) = (/) )
6		fvprc	|- ( -. K e. _V -> ( Atoms ` K ) = (/) )
7	5 6	nsyl2	|- ( P e. A -> K e. _V )
8		eqid	|- ( 0. ` K ) = ( 0. ` K )
9		eqid	|- (
10	1 8 9 2	isat	|- ( K e. _V -> ( P e. A <-> ( P e. B /\ ( 0. ` K ) (
11	10	simprbda	|- ( ( K e. _V /\ P e. A ) -> P e. B )
12	7 11	mpancom	|- ( P e. A -> P e. B )