Theorem fnbigcup

Description: Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	fnbigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fobigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
2		fofn	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$
3	1 2	ax-mp	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$