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	$⊢ \underset{˙}{\land} = meet (K)$
	m.z	$⊢ \underset{˙}{0} = 0. (K)$
	m.a	$⊢ A = Atoms (K)$
Assertion	meetat2	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P \in A \lor X \underset{˙}{\land} P = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		m.b	$⊢ B = {Base}_{K}$
2		m.m	$⊢ \underset{˙}{\land} = meet (K)$
3		m.z	$⊢ \underset{˙}{0} = 0. (K)$
4		m.a	$⊢ A = Atoms (K)$
5	1 2 3 4	meetat	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0})$
6		eleq1a	$⊢ P \in A \to (X \underset{˙}{\land} P = P \to X \underset{˙}{\land} P \in A)$
7	6	3ad2ant3	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = P \to X \underset{˙}{\land} P \in A)$
8	7	orim1d	$⊢ (K \in OL \land X \in B \land P \in A) \to ((X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0}) \to (X \underset{˙}{\land} P \in A \lor X \underset{˙}{\land} P = \underset{˙}{0}))$
9	5 8	mpd	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P \in A \lor X \underset{˙}{\land} P = \underset{˙}{0})$

Metamath Proof Explorer