Theorem isat

Description: The predicate "is an atom". ( ela analog.) (Contributed by NM, 18-Sep-2011)

	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	isat	$$⊢K\in D\to \left(P\in A\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}CP\right)\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	pats	$$⊢K\in D\to A=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$
6	5	eleq2d	$$⊢K\in D\to \left(P\in A\leftrightarrow P\in \left\{x\in B|\underset{\dot{}}{0}Cx\right\}\right)$$
7		breq2	$$⊢x=P\to \left(\underset{\dot{}}{0}Cx\leftrightarrow \underset{\dot{}}{0}CP\right)$$
8	7	elrab	$$⊢P\in \left\{x\in B|\underset{\dot{}}{0}Cx\right\}\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}CP\right)$$
9	6 8	syl6bb	$$⊢K\in D\to \left(P\in A\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}CP\right)\right)$$