atlle0

Description: An element less than or equal to zero equals zero. ( chle0 analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	atl0le.b	$⊢ B = {Base}_{K}$
	atl0le.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atl0le.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	atlle0	$⊢ (K \in AtLat \land X \in B) \to (X \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		atl0le.b	$⊢ B = {Base}_{K}$
2		atl0le.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atl0le.z	$⊢ \underset{˙}{0} = 0. (K)$
4	1 2 3	atl0le	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} X$
5	4	biantrud	$⊢ (K \in AtLat \land X \in B) \to (X \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow (X \underset{˙}{\leq} \underset{˙}{0} \land \underset{˙}{0} \underset{˙}{\leq} X))$
6		atlpos	$⊢ K \in AtLat \to K \in Poset$
7	6	adantr	$⊢ (K \in AtLat \land X \in B) \to K \in Poset$
8		simpr	$⊢ (K \in AtLat \land X \in B) \to X \in B$
9	1 3	atl0cl	$⊢ K \in AtLat \to \underset{˙}{0} \in B$
10	9	adantr	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \in B$
11	1 2	posasymb	$⊢ (K \in Poset \land X \in B \land \underset{˙}{0} \in B) \to ((X \underset{˙}{\leq} \underset{˙}{0} \land \underset{˙}{0} \underset{˙}{\leq} X) \leftrightarrow X = \underset{˙}{0})$
12	7 8 10 11	syl3anc	$⊢ (K \in AtLat \land X \in B) \to ((X \underset{˙}{\leq} \underset{˙}{0} \land \underset{˙}{0} \underset{˙}{\leq} X) \leftrightarrow X = \underset{˙}{0})$
13	5 12	bitrd	$⊢ (K \in AtLat \land X \in B) \to (X \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer