Theorem dalemcceb

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012)

	Ref	Expression
Hypotheses	da.ps0	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
	da.a1	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	dalemcceb	$$⊢\psi \to c\in {\mathrm{Base}}_K$$

Proof

Step	Hyp	Ref	Expression
1		da.ps0	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
2		da.a1	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3	1	dalemccea	$$⊢\psi \to c\in A$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 2	atbase	$$⊢c\in A\to c\in {\mathrm{Base}}_K$$
6	3 5	syl	$$⊢\psi \to c\in {\mathrm{Base}}_K$$