Theorem fosetex

Description: The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024)

	Ref	Expression
Assertion	fosetex	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢B^A\in \mathrm{V}$$
2		mapfoss	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\subseteq B^A$$
3	1 2	ssexi	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\in \mathrm{V}$$