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 Fin dom F F

Proof

Step Hyp Ref Expression
1 dmresv dom F V = dom F
2 finresfin F Fin F V Fin
3 fvex 1 st x V
4 eqid x F V 1 st x = x F V 1 st x
5 3 4 fnmpti x F V 1 st x Fn F V
6 dffn4 x F V 1 st x Fn F V x F V 1 st x : F V onto ran x F V 1 st x
7 5 6 mpbi x F V 1 st x : F V onto ran x F V 1 st x
8 relres Rel F V
9 reldm Rel F V dom F V = ran x F V 1 st x
10 foeq3 dom F V = ran x F V 1 st x x F V 1 st x : F V onto dom F V x F V 1 st x : F V onto ran x F V 1 st x
11 8 9 10 mp2b x F V 1 st x : F V onto dom F V x F V 1 st x : F V onto ran x F V 1 st x
12 7 11 mpbir x F V 1 st x : F V onto dom F V
13 fodomfi F V Fin x F V 1 st x : F V onto dom F V dom F V F V
14 2 12 13 sylancl F Fin dom F V F V
15 resss F V F
16 ssdomg F Fin F V F F V F
17 15 16 mpi F Fin F V F
18 domtr dom F V F V F V F dom F V F
19 14 17 18 syl2anc F Fin dom F V F
20 1 19 eqbrtrrid F Fin dom F F