Metamath Proof Explorer


Theorem dprdwd

Description: A mapping being a finitely supported function in the family S . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019) (Proof shortened by OpenAI, 30-Mar-2020)

Ref Expression
Hypotheses dprdff.w W=hiISi|finSupp0˙h
dprdff.1 φGdomDProdS
dprdff.2 φdomS=I
dprdwd.3 φxIASx
dprdwd.4 φfinSupp0˙xIA
Assertion dprdwd φxIAW

Proof

Step Hyp Ref Expression
1 dprdff.w W=hiISi|finSupp0˙h
2 dprdff.1 φGdomDProdS
3 dprdff.2 φdomS=I
4 dprdwd.3 φxIASx
5 dprdwd.4 φfinSupp0˙xIA
6 breq1 h=xIAfinSupp0˙hfinSupp0˙xIA
7 4 ralrimiva φxIASx
8 2 3 dprddomcld φIV
9 mptelixpg IVxIAxISxxIASx
10 8 9 syl φxIAxISxxIASx
11 7 10 mpbird φxIAxISx
12 fveq2 x=iSx=Si
13 12 cbvixpv xISx=iISi
14 11 13 eleqtrdi φxIAiISi
15 6 14 5 elrabd φxIAhiISi|finSupp0˙h
16 15 1 eleqtrrdi φxIAW