Theorem isat2

Description: The predicate "is an atom". ( elatcv0 analog.) (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	isatom.b	$$⊢B={\mathrm{Base}}_K$$
	isatom.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	isatom.c	$$⊢C={⋖}_K$$
	isatom.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	isat2	$$⊢\left(K\in D\wedge P\in B\right)\to \left(P\in A\leftrightarrow \underset{\dot{}}{0}CP\right)$$

Proof

Step	Hyp	Ref	Expression
1		isatom.b	$$⊢B={\mathrm{Base}}_K$$
2		isatom.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		isatom.c	$$⊢C={⋖}_K$$
4		isatom.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5	1 2 3 4	isat	$$⊢K\in D\to \left(P\in A\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}CP\right)\right)$$
6	5	baibd	$$⊢\left(K\in D\wedge P\in B\right)\to \left(P\in A\leftrightarrow \underset{\dot{}}{0}CP\right)$$