leat3

Description: A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012)

	Ref	Expression
Hypotheses	leatom.b	$⊢ B = {Base}_{K}$
	leatom.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	leatom.z	$⊢ \underset{˙}{0} = 0. (K)$
	leatom.a	$⊢ A = Atoms (K)$
Assertion	leat3	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to (X \in A \lor X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		leatom.b	$⊢ B = {Base}_{K}$
2		leatom.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		leatom.z	$⊢ \underset{˙}{0} = 0. (K)$
4		leatom.a	$⊢ A = Atoms (K)$
5	1 2 3 4	leat	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to (X = P \lor X = \underset{˙}{0})$
6		simpl3	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to P \in A$
7		eleq1a	$⊢ P \in A \to (X = P \to X \in A)$
8	6 7	syl	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to (X = P \to X \in A)$
9	8	orim1d	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to ((X = P \lor X = \underset{˙}{0}) \to (X \in A \lor X = \underset{˙}{0}))$
10	5 9	mpd	$⊢ ((K \in OP \land X \in B \land P \in A) \land X \underset{˙}{\leq} P) \to (X \in A \lor X = \underset{˙}{0})$

Metamath Proof Explorer