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 |