Theorem fobigcup

Description: Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	fobigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢x\in \mathrm{V}\to \bigcup x\in \mathrm{V}$$
2	1	rgen	$$⊢\forall x\in \mathrm{V}\bigcup x\in \mathrm{V}$$
3		dfbigcup2	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\left(x\in \mathrm{V}⟼\bigcup x\right)$$
4	3	mptfng	$$⊢\forall x\in \mathrm{V}\bigcup x\in \mathrm{V}\leftrightarrow \mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$
5	2 4	mpbi	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$
6	3	rnmpt	$$⊢\mathrm{ran}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\left\{y|\exists x\in \mathrm{V}y=\bigcup x\right\}$$
7		vex	$$⊢y\in \mathrm{V}$$
8		vsnex	$$⊢\left\{y\right\}\in \mathrm{V}$$
9		unisnv	$$⊢\bigcup \left\{y\right\}=y$$
10	9	eqcomi	$$⊢y=\bigcup \left\{y\right\}$$
11		unieq	$$⊢x=\left\{y\right\}\to \bigcup x=\bigcup \left\{y\right\}$$
12	11	rspceeqv	$$⊢\left(\left\{y\right\}\in \mathrm{V}\wedge y=\bigcup \left\{y\right\}\right)\to \exists x\in \mathrm{V}y=\bigcup x$$
13	8 10 12	mp2an	$$⊢\exists x\in \mathrm{V}y=\bigcup x$$
14	7 13	2th	$$⊢y\in \mathrm{V}\leftrightarrow \exists x\in \mathrm{V}y=\bigcup x$$
15	14	eqabi	$$⊢\mathrm{V}=\left\{y|\exists x\in \mathrm{V}y=\bigcup x\right\}$$
16	6 15	eqtr4i	$$⊢\mathrm{ran}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\mathrm{V}$$
17		df-fo	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\leftrightarrow \left(\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}\wedge \mathrm{ran}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\mathrm{V}\right)$$
18	5 16 17	mpbir2an	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$