Theorem watvalN

Description: Value of the W atoms function. (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	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)$$

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	watfvalN	$$⊢K\in B\to W=\left(d\in A⟼A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)\right)$$
5	4	fveq1d	$$⊢K\in B\to W\left(D\right)=\left(d\in A⟼A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)\right)\left(D\right)$$
6		sneq	$$⊢d=D\to \left\{d\right\}=\left\{D\right\}$$
7	6	fveq2d	$$⊢d=D\to {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)={\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)$$
8	7	difeq2d	$$⊢d=D\to A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)=A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)$$
9		eqid	$$⊢\left(d\in A⟼A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)\right)=\left(d\in A⟼A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)\right)$$
10	1	fvexi	$$⊢A\in \mathrm{V}$$
11	10	difexi	$$⊢A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)\in \mathrm{V}$$
12	8 9 11	fvmpt	$$⊢D\in A\to \left(d\in A⟼A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{d\right\}\right)\right)\left(D\right)=A\setminus {\perp }_{𝑃}\left(K\right)\left(\left\{D\right\}\right)$$
13	5 12	sylan9eq	$$⊢\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)$$