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