This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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