Theorem fnsingle

Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	fnsingle	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
2		df-rel	$$⊢\mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)\leftrightarrow \left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	mpbir	$$⊢\mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)$$
4		df-singleton	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$
5	4	releqi	$$⊢\mathrm{Rel}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\leftrightarrow \mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)$$
6	3 5	mpbir	$$⊢\mathrm{Rel}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	brsingle	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\leftrightarrow y=\left\{x\right\}$$
10		vex	$$⊢z\in \mathrm{V}$$
11	7 10	brsingle	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}z\leftrightarrow z=\left\{x\right\}$$
12		eqtr3	$$⊢\left(y=\left\{x\right\}\wedge z=\left\{x\right\}\right)\to y=z$$
13	9 11 12	syl2anb	$$⊢\left(x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\wedge x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}z\right)\to y=z$$
14	13	ax-gen	$$⊢\forall z\left(\left(x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\wedge x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}z\right)\to y=z\right)$$
15	14	gen2	$$⊢\forall x\forall y\forall z\left(\left(x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\wedge x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}z\right)\to y=z\right)$$
16		dffun2	$$⊢\mathrm{Fun}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\leftrightarrow \left(\mathrm{Rel}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\wedge \forall x\forall y\forall z\left(\left(x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\wedge x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}z\right)\to y=z\right)\right)$$
17	6 15 16	mpbir2an	$$⊢\mathrm{Fun}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
18		eqv	$$⊢\mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\mathrm{V}\leftrightarrow \forall xx\in \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
19		eqid	$$⊢\left\{x\right\}=\left\{x\right\}$$
20		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
21	7 20	brsingle	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{x\right\}$$
22	19 21	mpbir	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}$$
23		breq2	$$⊢y=\left\{x\right\}\to \left(x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\leftrightarrow x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}\right)$$
24	20 23	spcev	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}\to \exists yx\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y$$
25	22 24	ax-mp	$$⊢\exists yx\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y$$
26	7	eldm	$$⊢x\in \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\leftrightarrow \exists yx\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y$$
27	25 26	mpbir	$$⊢x\in \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
28	18 27	mpgbir	$$⊢\mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\mathrm{V}$$
29		df-fn	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}\leftrightarrow \left(\mathrm{Fun}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\wedge \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\mathrm{V}\right)$$
30	17 28 29	mpbir2an	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}$$