Metamath Proof Explorer


Theorem fidomdm

Description: Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion fidomdm
|- ( F e. Fin -> dom F ~<_ F )

Proof

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 )