leat2

Description: A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013)

	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	leat2	$⊢ ((K \in OP \land X \in B \land P \in A) \land (X \neq \underset{˙}{0} \land X \underset{˙}{\leq} P)) \to X = P$

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	leatb	$⊢ (K \in OP \land X \in B \land P \in A) \to (X \underset{˙}{\leq} P \leftrightarrow (X = P \lor X = \underset{˙}{0}))$
6		orcom	$⊢ (X = P \lor X = \underset{˙}{0}) \leftrightarrow (X = \underset{˙}{0} \lor X = P)$
7		neor	$⊢ (X = \underset{˙}{0} \lor X = P) \leftrightarrow (X \neq \underset{˙}{0} \to X = P)$
8	6 7	bitri	$⊢ (X = P \lor X = \underset{˙}{0}) \leftrightarrow (X \neq \underset{˙}{0} \to X = P)$
9	5 8	bitrdi	$⊢ (K \in OP \land X \in B \land P \in A) \to (X \underset{˙}{\leq} P \leftrightarrow (X \neq \underset{˙}{0} \to X = P))$
10	9	biimpd	$⊢ (K \in OP \land X \in B \land P \in A) \to (X \underset{˙}{\leq} P \to (X \neq \underset{˙}{0} \to X = P))$
11	10	com23	$⊢ (K \in OP \land X \in B \land P \in A) \to (X \neq \underset{˙}{0} \to (X \underset{˙}{\leq} P \to X = P))$
12	11	imp32	$⊢ ((K \in OP \land X \in B \land P \in A) \land (X \neq \underset{˙}{0} \land X \underset{˙}{\leq} P)) \to X = P$

Metamath Proof Explorer