atlex

Description: Every nonzero element of an atomic lattice is greater than or equal to an atom. ( hatomic analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	atlex.b	$⊢ B = {Base}_{K}$
	atlex.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlex.z	$⊢ \underset{˙}{0} = 0. (K)$
	atlex.a	$⊢ A = Atoms (K)$
Assertion	atlex	$⊢ (K \in AtLat \land X \in B \land X \neq \underset{˙}{0}) \to \exists y \in A y \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		atlex.b	$⊢ B = {Base}_{K}$
2		atlex.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlex.z	$⊢ \underset{˙}{0} = 0. (K)$
4		atlex.a	$⊢ A = Atoms (K)$
5		eqid	$⊢ glb (K) = glb (K)$
6	1 5 2 3 4	isatl	$⊢ K \in AtLat \leftrightarrow (K \in Lat \land B \in dom glb (K) \land \forall x \in B (x \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} x))$
7	6	simp3bi	$⊢ K \in AtLat \to \forall x \in B (x \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} x)$
8		neeq1	$⊢ x = X \to (x \neq \underset{˙}{0} \leftrightarrow X \neq \underset{˙}{0})$
9		breq2	$⊢ x = X \to (y \underset{˙}{\leq} x \leftrightarrow y \underset{˙}{\leq} X)$
10	9	rexbidv	$⊢ x = X \to (\exists y \in A y \underset{˙}{\leq} x \leftrightarrow \exists y \in A y \underset{˙}{\leq} X)$
11	8 10	imbi12d	$⊢ x = X \to ((x \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} x) \leftrightarrow (X \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} X))$
12	11	rspccv	$⊢ \forall x \in B (x \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} x) \to (X \in B \to (X \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} X))$
13	7 12	syl	$⊢ K \in AtLat \to (X \in B \to (X \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} X))$
14	13	3imp	$⊢ (K \in AtLat \land X \in B \land X \neq \underset{˙}{0}) \to \exists y \in A y \underset{˙}{\leq} X$

Metamath Proof Explorer