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