# Metamath Proof Explorer

## Theorem f1omptsn

Description: A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypotheses f1omptsn.f ${⊢}{F}=\left({x}\in {A}⟼\left\{{x}\right\}\right)$
f1omptsn.r ${⊢}{R}=\left\{{u}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}$
Assertion f1omptsn ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{R}$

### Proof

Step Hyp Ref Expression
1 f1omptsn.f ${⊢}{F}=\left({x}\in {A}⟼\left\{{x}\right\}\right)$
2 f1omptsn.r ${⊢}{R}=\left\{{u}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}$
3 sneq ${⊢}{x}={a}\to \left\{{x}\right\}=\left\{{a}\right\}$
4 3 cbvmptv ${⊢}\left({x}\in {A}⟼\left\{{x}\right\}\right)=\left({a}\in {A}⟼\left\{{a}\right\}\right)$
5 4 eqcomi ${⊢}\left({a}\in {A}⟼\left\{{a}\right\}\right)=\left({x}\in {A}⟼\left\{{x}\right\}\right)$
6 id ${⊢}{u}={z}\to {u}={z}$
7 6 3 eqeqan12d ${⊢}\left({u}={z}\wedge {x}={a}\right)\to \left({u}=\left\{{x}\right\}↔{z}=\left\{{a}\right\}\right)$
8 7 cbvrexdva ${⊢}{u}={z}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}↔\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right)$
9 8 cbvabv ${⊢}\left\{{u}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}=\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}$
10 9 eqcomi ${⊢}\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}=\left\{{u}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}$
11 5 10 f1omptsnlem ${⊢}\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}$
12 2 9 eqtri ${⊢}{R}=\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}$
13 f1oeq3 ${⊢}{R}=\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}\to \left(\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}{R}↔\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}\right)$
14 12 13 ax-mp ${⊢}\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}{R}↔\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}\left\{{z}|\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{a}\right\}\right\}$
15 11 14 mpbir ${⊢}\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}{R}$
16 1 4 eqtri ${⊢}{F}=\left({a}\in {A}⟼\left\{{a}\right\}\right)$
17 f1oeq1 ${⊢}{F}=\left({a}\in {A}⟼\left\{{a}\right\}\right)\to \left({F}:{A}\underset{1-1 onto}{⟶}{R}↔\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}{R}\right)$
18 16 17 ax-mp ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{R}↔\left({a}\in {A}⟼\left\{{a}\right\}\right):{A}\underset{1-1 onto}{⟶}{R}$
19 15 18 mpbir ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{R}$