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

Metamath Proof Explorer

Theorem meetat2

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012)

Ref Expression
Hypotheses m.b 
|- B = ( Base ` K )
m.m 
|- ./\ = ( meet ` K )
m.z 
|- .0. = ( 0. ` K )
m.a 
|- A = ( Atoms ` K )
Assertion meetat2 
|- ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = .0. ) )

Proof

Step Hyp Ref Expression
1 m.b 
 |-  B = ( Base ` K )
2 m.m 
 |-  ./\ = ( meet ` K )
3 m.z 
 |-  .0. = ( 0. ` K )
4 m.a 
 |-  A = ( Atoms ` K )
5 1 2 3 4 meetat 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) )
6 eleq1a 
 |-  ( P e. A -> ( ( X ./\ P ) = P -> ( X ./\ P ) e. A ) )
7 6 3ad2ant3 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = P -> ( X ./\ P ) e. A ) )
8 7 orim1d 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = .0. ) ) )
9 5 8 mpd 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = .0. ) )