Metamath Proof Explorer


Theorem watfvalN

Description: 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 watfvalN K B W = d A 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 elex K B K V
5 fveq2 k = K Atoms k = Atoms K
6 5 1 eqtr4di k = K Atoms k = A
7 fveq2 k = K 𝑃 k = 𝑃 K
8 7 fveq1d k = K 𝑃 k d = 𝑃 K d
9 6 8 difeq12d k = K Atoms k 𝑃 k d = A 𝑃 K d
10 6 9 mpteq12dv k = K d Atoms k Atoms k 𝑃 k d = d A A 𝑃 K d
11 df-watsN WAtoms = k V d Atoms k Atoms k 𝑃 k d
12 10 11 1 mptfvmpt K V WAtoms K = d A A 𝑃 K d
13 3 12 syl5eq K V W = d A A 𝑃 K d
14 4 13 syl K B W = d A A 𝑃 K d