This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )