Metamath Proof Explorer


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 snex
 |-  { y } e. _V
9 7 unisn
 |-  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 abbi2i
 |-  _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