Metamath Proof Explorer


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 = Atoms K
watomfval.p P = 𝑃 K
watomfval.w W = WAtoms K
Assertion watvalN K B D A W D = A 𝑃 K D

Proof

Step Hyp Ref Expression
1 watomfval.a A = Atoms K
2 watomfval.p P = 𝑃 K
3 watomfval.w W = WAtoms K
4 1 2 3 watfvalN K B W = d A A 𝑃 K d
5 4 fveq1d K B W D = d A A 𝑃 K d D
6 sneq d = D d = D
7 6 fveq2d d = D 𝑃 K d = 𝑃 K D
8 7 difeq2d d = D A 𝑃 K d = A 𝑃 K D
9 eqid d A A 𝑃 K d = d A A 𝑃 K d
10 1 fvexi A V
11 10 difexi A 𝑃 K D V
12 8 9 11 fvmpt D A d A A 𝑃 K d D = A 𝑃 K D
13 5 12 sylan9eq K B D A W D = A 𝑃 K D