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

Metamath Proof Explorer

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 )