Theorem iswatN

Description: The predicate "is a W atom" (corresponding to fiducial atom D ). (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	watomfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	watomfval.p	$$⊢P={\perp }_{𝑃}\left(K\right)$$
	watomfval.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
Assertion	iswatN	$$⊢\left(K\in B\wedge D\in A\right)\to \left(P\in W\left(D\right)\leftrightarrow \left(P\in A\wedge \neg P\in {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		watomfval.p	$$⊢P={\perp }_{𝑃}\left(K\right)$$
3		watomfval.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
4	1 2 3	watvalN	$$⊢\left(K\in B\wedge D\in A\right)\to W\left(D\right)=A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)$$
5	4	eleq2d	$$⊢\left(K\in B\wedge D\in A\right)\to \left(P\in W\left(D\right)\leftrightarrow P\in \left(A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\right)\right)$$
6		eldif	$$⊢P\in \left(A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\right)\leftrightarrow \left(P\in A\wedge \neg P\in {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\right)$$
7	5 6	bitrdi	$$⊢\left(K\in B\wedge D\in A\right)\to \left(P\in W\left(D\right)\leftrightarrow \left(P\in A\wedge \neg P\in {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\right)\right)$$