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. ) )