Step |
Hyp |
Ref |
Expression |
1 |
|
snex |
|- { x } e. _V |
2 |
1
|
rnex |
|- ran { x } e. _V |
3 |
2
|
uniex |
|- U. ran { x } e. _V |
4 |
|
df-2nd |
|- 2nd = ( x e. _V |-> U. ran { x } ) |
5 |
3 4
|
fnmpti |
|- 2nd Fn _V |
6 |
4
|
rnmpt |
|- ran 2nd = { y | E. x e. _V y = U. ran { x } } |
7 |
|
vex |
|- y e. _V |
8 |
|
opex |
|- <. y , y >. e. _V |
9 |
7 7
|
op2nda |
|- U. ran { <. y , y >. } = y |
10 |
9
|
eqcomi |
|- y = U. ran { <. y , y >. } |
11 |
|
sneq |
|- ( x = <. y , y >. -> { x } = { <. y , y >. } ) |
12 |
11
|
rneqd |
|- ( x = <. y , y >. -> ran { x } = ran { <. y , y >. } ) |
13 |
12
|
unieqd |
|- ( x = <. y , y >. -> U. ran { x } = U. ran { <. y , y >. } ) |
14 |
13
|
rspceeqv |
|- ( ( <. y , y >. e. _V /\ y = U. ran { <. y , y >. } ) -> E. x e. _V y = U. ran { x } ) |
15 |
8 10 14
|
mp2an |
|- E. x e. _V y = U. ran { x } |
16 |
7 15
|
2th |
|- ( y e. _V <-> E. x e. _V y = U. ran { x } ) |
17 |
16
|
abbi2i |
|- _V = { y | E. x e. _V y = U. ran { x } } |
18 |
6 17
|
eqtr4i |
|- ran 2nd = _V |
19 |
|
df-fo |
|- ( 2nd : _V -onto-> _V <-> ( 2nd Fn _V /\ ran 2nd = _V ) ) |
20 |
5 18 19
|
mpbir2an |
|- 2nd : _V -onto-> _V |