Theorem fobigcup

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

	Ref	Expression
Assertion	fobigcup	|- Bigcup : _V -onto-> _V

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( x e. _V -> U. x e. _V )
2	1	rgen	|- A. x e. _V U. x e. _V
3		dfbigcup2	|- Bigcup = ( x e. _V |-> U. x )
4	3	mptfng	|- ( A. x e. _V U. x e. _V <-> Bigcup Fn _V )
5	2 4	mpbi	|- Bigcup Fn _V
6	3	rnmpt	|- ran Bigcup = { y | E. x e. _V y = U. x }
7		vex	|- y e. _V
8		vsnex	|- { y } e. _V
9		unisnv	|- U. { y } = y
10	9	eqcomi	|- y = U. { y }
11		unieq	|- ( x = { y } -> U. x = U. { y } )
12	11	rspceeqv	|- ( ( { y } e. _V /\ y = U. { y } ) -> E. x e. _V y = U. x )
13	8 10 12	mp2an	|- E. x e. _V y = U. x
14	7 13	2th	|- ( y e. _V <-> E. x e. _V y = U. x )
15	14	eqabi	|- _V = { y | E. x e. _V y = U. x }
16	6 15	eqtr4i	|- ran Bigcup = _V
17		df-fo	|- ( Bigcup : _V -onto-> _V <-> ( Bigcup Fn _V /\ ran Bigcup = _V ) )
18	5 16 17	mpbir2an	|- Bigcup : _V -onto-> _V