# Metamath Proof Explorer

## 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}×\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}×\mathrm{V}$
2 df-rel ${⊢}\mathrm{Rel}\left(\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)↔\left(\mathrm{V}×\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}×\mathrm{V}$
3 1 2 mpbir ${⊢}\mathrm{Rel}\left(\left(\mathrm{V}×\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}×\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{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}↔\mathrm{Rel}\left(\left(\mathrm{V}×\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}↔{y}=\left\{{x}\right\}$
10 vex ${⊢}{z}\in \mathrm{V}$
11 7 10 brsingle ${⊢}{x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{z}↔{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}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{y}\wedge {x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{z}\right)\to {y}={z}\right)$
15 14 gen2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{y}\wedge {x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{z}\right)\to {y}={z}\right)$
16 dffun2 ${⊢}\mathrm{Fun}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}↔\left(\mathrm{Rel}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\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}↔\forall {x}\phantom{\rule{.4em}{0ex}}{x}\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\}↔\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}↔{x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{{x}\right\}\right)$
24 20 23 spcev ${⊢}{x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{{x}\right\}\to \exists {y}\phantom{\rule{.4em}{0ex}}{x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{y}$
25 22 24 ax-mp ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{x}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}{y}$
26 7 eldm ${⊢}{x}\in \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}↔\exists {y}\phantom{\rule{.4em}{0ex}}{x}\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}↔\left(\mathrm{Fun}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\wedge \mathrm{dom}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\mathrm{V}\right)$
30 17 28 29 mpbir2an ${⊢}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}$