Complexity of a proper class of extendibles If consistent, is existence of a proper class of extendible cardinals provably equivalent to a $Σ^V_5$ statement?
Recall that in ZFC, a cardinal $κ$ is extendible iff for every $λ>κ$ there is an elementary embedding $j$ of $V_λ$ into some $V_μ$ with $\mathrm{crit}(j)=κ$. (In ZF, one also requires $j(k)>λ$, but this does not affect the above definition in ZFC.)
Extendibles are unusual in being a natural large cardinal property with high quantifier complexity (see this question for other examples of high quantifier complexity).  The property of being some $V_μ$ is $Π^V_1$ (or $Π_1$ for short), being $λ$-extendible is $Σ_2$, and being extendible is $Π_3$, and so existence of an extendible cardinal is $Σ_4$, and existence of a proper class of extendibles is $Π_5$.
In the other direction, if $κ$ is extendible, then $V_κ ≺_{Σ_3} V$, and thus (assuming consistency) existence of an extendible cardinal is not equivalent in ZFC to a $Π_4$ statement.  Analogously, I expect that existence of a proper class of extendibles is not provably (in ZFC) $Σ_5$, but it is easy to be confused by quantifier counting.
Offered in Q/A format as I was able to solve this question while working on its exposition.
 A: No, it is not; existence of a proper class of extendible cardinals is not provable in ZFC from any consistent $Σ^V_5$ statement.
Assume a proper class of extendibles and let $φ$ be a true $Σ_5$ statement (or even the conjunction of all true $Σ_5$ statements), and let a set $S$ witness $φ$, and let $κ$ be the least extendible above $S$.  Then $V_κ$ satisfies $\mathrm{ZFC} + φ \, +$ non-existence of a proper class of extendibles. ($V_κ ≺_{Σ_3} V$, so $V_κ$ satisfies all true $Π_4$ statements with parameters in $V_κ$, and by $S∈V_κ$, $V_κ ⊨ φ$.)
$V_κ ≺_{Σ_3} V$ is a standard fact about extendibles (as an aside, despite its similarity, being supercompact is $Π_2$) and follows from existence of arbitrarily high $λ$ such that $V_κ ≺ V_λ$ (or just $V_κ ≺_{Σ_3} V_λ$):  Let $λ$ with $V_κ ≺ V_λ$ be large enough.  By Downward Löwenheim-Skolem, $V_λ ≺_{Σ_1} V$, so $V_λ$ satisfies all true $Π_2$ statements with parameters in $V_λ$, so (since $λ$ is large enough relative to $κ$) $V_λ$ (and thus $V_κ$) satisfies all true $Σ_3$ statements with parameters in $V_κ$, so $V_κ ≺_{Σ_3} V$.
