Step |
Hyp |
Ref |
Expression |
1 |
|
dmresv |
|- dom ( F |` _V ) = dom F |
2 |
|
finresfin |
|- ( F e. Fin -> ( F |` _V ) e. Fin ) |
3 |
|
fvex |
|- ( 1st ` x ) e. _V |
4 |
|
eqid |
|- ( x e. ( F |` _V ) |-> ( 1st ` x ) ) = ( x e. ( F |` _V ) |-> ( 1st ` x ) ) |
5 |
3 4
|
fnmpti |
|- ( x e. ( F |` _V ) |-> ( 1st ` x ) ) Fn ( F |` _V ) |
6 |
|
dffn4 |
|- ( ( x e. ( F |` _V ) |-> ( 1st ` x ) ) Fn ( F |` _V ) <-> ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) ) |
7 |
5 6
|
mpbi |
|- ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) |
8 |
|
relres |
|- Rel ( F |` _V ) |
9 |
|
reldm |
|- ( Rel ( F |` _V ) -> dom ( F |` _V ) = ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) ) |
10 |
|
foeq3 |
|- ( dom ( F |` _V ) = ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) -> ( ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> dom ( F |` _V ) <-> ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) ) ) |
11 |
8 9 10
|
mp2b |
|- ( ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> dom ( F |` _V ) <-> ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> ran ( x e. ( F |` _V ) |-> ( 1st ` x ) ) ) |
12 |
7 11
|
mpbir |
|- ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> dom ( F |` _V ) |
13 |
|
fodomfi |
|- ( ( ( F |` _V ) e. Fin /\ ( x e. ( F |` _V ) |-> ( 1st ` x ) ) : ( F |` _V ) -onto-> dom ( F |` _V ) ) -> dom ( F |` _V ) ~<_ ( F |` _V ) ) |
14 |
2 12 13
|
sylancl |
|- ( F e. Fin -> dom ( F |` _V ) ~<_ ( F |` _V ) ) |
15 |
|
resss |
|- ( F |` _V ) C_ F |
16 |
|
ssdomg |
|- ( F e. Fin -> ( ( F |` _V ) C_ F -> ( F |` _V ) ~<_ F ) ) |
17 |
15 16
|
mpi |
|- ( F e. Fin -> ( F |` _V ) ~<_ F ) |
18 |
|
domtr |
|- ( ( dom ( F |` _V ) ~<_ ( F |` _V ) /\ ( F |` _V ) ~<_ F ) -> dom ( F |` _V ) ~<_ F ) |
19 |
14 17 18
|
syl2anc |
|- ( F e. Fin -> dom ( F |` _V ) ~<_ F ) |
20 |
1 19
|
eqbrtrrid |
|- ( F e. Fin -> dom F ~<_ F ) |