Metamath Proof Explorer


Theorem vsetrec

Description: Construct _V using set recursion. The proof indirectly uses trcl , which relies on rec , but theoretically C in trcl could be constructed using setrecs instead. The proof of this theorem uses the dummy variable a rather than x to avoid a distinct variable requirement between F and x . (Contributed by Emmett Weisz, 23-Jun-2021)

Ref Expression
Hypothesis vsetrec.1 F=xV𝒫x
Assertion vsetrec setrecsF=V

Proof

Step Hyp Ref Expression
1 vsetrec.1 F=xV𝒫x
2 setind aasetrecsFasetrecsFsetrecsF=V
3 vex aV
4 3 pwid a𝒫a
5 pweq x=a𝒫x=𝒫a
6 3 pwex 𝒫aV
7 5 1 6 fvmpt aVFa=𝒫a
8 3 7 ax-mp Fa=𝒫a
9 eqid setrecsF=setrecsF
10 3 a1i asetrecsFaV
11 id asetrecsFasetrecsF
12 9 10 11 setrec1 asetrecsFFasetrecsF
13 8 12 eqsstrrid asetrecsF𝒫asetrecsF
14 13 sseld asetrecsFa𝒫aasetrecsF
15 4 14 mpi asetrecsFasetrecsF
16 2 15 mpg setrecsF=V