Step |
Hyp |
Ref |
Expression |
1 |
|
dmexg |
|- ( x e. No -> dom x e. _V ) |
2 |
1
|
rgen |
|- A. x e. No dom x e. _V |
3 |
|
df-bday |
|- bday = ( x e. No |-> dom x ) |
4 |
3
|
mptfng |
|- ( A. x e. No dom x e. _V <-> bday Fn No ) |
5 |
2 4
|
mpbi |
|- bday Fn No |
6 |
3
|
rnmpt |
|- ran bday = { y | E. x e. No y = dom x } |
7 |
|
noxp1o |
|- ( y e. On -> ( y X. { 1o } ) e. No ) |
8 |
|
1oex |
|- 1o e. _V |
9 |
8
|
snnz |
|- { 1o } =/= (/) |
10 |
|
dmxp |
|- ( { 1o } =/= (/) -> dom ( y X. { 1o } ) = y ) |
11 |
9 10
|
ax-mp |
|- dom ( y X. { 1o } ) = y |
12 |
11
|
eqcomi |
|- y = dom ( y X. { 1o } ) |
13 |
|
dmeq |
|- ( x = ( y X. { 1o } ) -> dom x = dom ( y X. { 1o } ) ) |
14 |
13
|
rspceeqv |
|- ( ( ( y X. { 1o } ) e. No /\ y = dom ( y X. { 1o } ) ) -> E. x e. No y = dom x ) |
15 |
7 12 14
|
sylancl |
|- ( y e. On -> E. x e. No y = dom x ) |
16 |
|
nodmon |
|- ( x e. No -> dom x e. On ) |
17 |
|
eleq1a |
|- ( dom x e. On -> ( y = dom x -> y e. On ) ) |
18 |
16 17
|
syl |
|- ( x e. No -> ( y = dom x -> y e. On ) ) |
19 |
18
|
rexlimiv |
|- ( E. x e. No y = dom x -> y e. On ) |
20 |
15 19
|
impbii |
|- ( y e. On <-> E. x e. No y = dom x ) |
21 |
20
|
abbi2i |
|- On = { y | E. x e. No y = dom x } |
22 |
6 21
|
eqtr4i |
|- ran bday = On |
23 |
|
df-fo |
|- ( bday : No -onto-> On <-> ( bday Fn No /\ ran bday = On ) ) |
24 |
5 22 23
|
mpbir2an |
|- bday : No -onto-> On |