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