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

Metamath Proof Explorer

Theorem lhpbase

Description: A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses lhpbase.b 
|- B = ( Base ` K )
lhpbase.h 
|- H = ( LHyp ` K )
Assertion lhpbase 
|- ( W e. H -> W e. B )

Proof

Step Hyp Ref Expression
1 lhpbase.b 
 |-  B = ( Base ` K )
2 lhpbase.h 
 |-  H = ( LHyp ` K )
3 n0i 
 |-  ( W e. H -> -. H = (/) )
4 2 eqeq1i 
 |-  ( H = (/) <-> ( LHyp ` K ) = (/) )
5 3 4 sylnib 
 |-  ( W e. H -> -. ( LHyp ` K ) = (/) )
6 fvprc 
 |-  ( -. K e. _V -> ( LHyp ` K ) = (/) )
7 5 6 nsyl2 
 |-  ( W e. H -> K e. _V )
8 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
9 eqid 
 |-  (
10 1 8 9 2 islhp 
 |-  ( K e. _V -> ( W e. H <-> ( W e. B /\ W (
11 10 simprbda 
 |-  ( ( K e. _V /\ W e. H ) -> W e. B )
12 7 11 mpancom 
 |-  ( W e. H -> W e. B )