![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > watvalN | Structured version Visualization version GIF version |
Description: Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Ref | Expression |
---|---|
watomfval.a | ⊢ 𝐴 = (Atoms‘𝐾) |
watomfval.p | ⊢ 𝑃 = (⊥𝑃‘𝐾) |
watomfval.w | ⊢ 𝑊 = (WAtoms‘𝐾) |
Ref | Expression |
---|---|
watvalN | ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | watomfval.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
2 | watomfval.p | . . . 4 ⊢ 𝑃 = (⊥𝑃‘𝐾) | |
3 | watomfval.w | . . . 4 ⊢ 𝑊 = (WAtoms‘𝐾) | |
4 | 1, 2, 3 | watfvalN 35781 | . . 3 ⊢ (𝐾 ∈ 𝐵 → 𝑊 = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})))) |
5 | 4 | fveq1d 6354 | . 2 ⊢ (𝐾 ∈ 𝐵 → (𝑊‘𝐷) = ((𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})))‘𝐷)) |
6 | sneq 4331 | . . . . 5 ⊢ (𝑑 = 𝐷 → {𝑑} = {𝐷}) | |
7 | 6 | fveq2d 6356 | . . . 4 ⊢ (𝑑 = 𝐷 → ((⊥𝑃‘𝐾)‘{𝑑}) = ((⊥𝑃‘𝐾)‘{𝐷})) |
8 | 7 | difeq2d 3871 | . . 3 ⊢ (𝑑 = 𝐷 → (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) |
9 | eqid 2760 | . . 3 ⊢ (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑}))) = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑}))) | |
10 | fvex 6362 | . . . . 5 ⊢ (Atoms‘𝐾) ∈ V | |
11 | 1, 10 | eqeltri 2835 | . . . 4 ⊢ 𝐴 ∈ V |
12 | difexg 4960 | . . . 4 ⊢ (𝐴 ∈ V → (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷})) ∈ V) | |
13 | 11, 12 | ax-mp 5 | . . 3 ⊢ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷})) ∈ V |
14 | 8, 9, 13 | fvmpt 6444 | . 2 ⊢ (𝐷 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})))‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) |
15 | 5, 14 | sylan9eq 2814 | 1 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2139 Vcvv 3340 ∖ cdif 3712 {csn 4321 ↦ cmpt 4881 ‘cfv 6049 Atomscatm 35053 ⊥𝑃cpolN 35691 WAtomscwpointsN 35775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-rep 4923 ax-sep 4933 ax-nul 4941 ax-pr 5055 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-reu 3057 df-rab 3059 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-iun 4674 df-br 4805 df-opab 4865 df-mpt 4882 df-id 5174 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-res 5278 df-ima 5279 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056 df-fv 6057 df-watsN 35779 |
This theorem is referenced by: iswatN 35783 |
Copyright terms: Public domain | W3C validator |