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\in \mathrm{Fin}\to \mathrm{dom}F\preccurlyeq F$$

Proof

Step	Hyp	Ref	Expression
1		dmresv	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)=\mathrm{dom}F$$
2		finresfin	$$⊢F\in \mathrm{Fin}\to {F\upharpoonright }_{\mathrm{V}}\in \mathrm{Fin}$$
3		fvex	$$⊢1^{st}\left(x\right)\in \mathrm{V}$$
4		eqid	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)=\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
5	3 4	fnmpti	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)Fn\left({F\upharpoonright }_{\mathrm{V}}\right)$$
6		dffn4	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)Fn\left({F\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
7	5 6	mpbi	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
8		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\mathrm{V}}\right)$$
9		reldm	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\mathrm{V}}\right)\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
10		foeq3	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)\to \left(\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)\right)$$
11	8 9 10	mp2b	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
12	7 11	mpbir	$$⊢\left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)$$
13		fodomfi	$$⊢\left({F\upharpoonright }_{\mathrm{V}}\in \mathrm{Fin}\wedge \left(x\in \left({F\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{F\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\right)\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({F\upharpoonright }_{\mathrm{V}}\right)$$
14	2 12 13	sylancl	$$⊢F\in \mathrm{Fin}\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({F\upharpoonright }_{\mathrm{V}}\right)$$
15		resss	$$⊢{F\upharpoonright }_{\mathrm{V}}\subseteq F$$
16		ssdomg	$$⊢F\in \mathrm{Fin}\to \left({F\upharpoonright }_{\mathrm{V}}\subseteq F\to \left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq F\right)$$
17	15 16	mpi	$$⊢F\in \mathrm{Fin}\to \left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq F$$
18		domtr	$$⊢\left(\mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({F\upharpoonright }_{\mathrm{V}}\right)\wedge \left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq F\right)\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq F$$
19	14 17 18	syl2anc	$$⊢F\in \mathrm{Fin}\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq F$$
20	1 19	eqbrtrrid	$$⊢F\in \mathrm{Fin}\to \mathrm{dom}F\preccurlyeq F$$