# Metamath Proof Explorer

## Theorem f1omptsnlem

Description: This is the core of the proof of f1omptsn , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-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 f1omptsnlem ${⊢}{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 eqid ${⊢}\left\{{x}\right\}=\left\{{x}\right\}$
4 snex ${⊢}\left\{{x}\right\}\in \mathrm{V}$
5 eqsbc3
6 4 5 ax-mp
7 3 6 mpbir
8 sbcel2
9 csbconstg
10 4 9 ax-mp
11 10 eleq2i
12 8 11 bitri
13 2 abeq2i ${⊢}{u}\in {R}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}$
14 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {u}=\left\{{x}\right\}\right)$
15 13 14 sylbbr ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {u}=\left\{{x}\right\}\right)\to {u}\in {R}$
16 15 19.23bi ${⊢}\left({x}\in {A}\wedge {u}=\left\{{x}\right\}\right)\to {u}\in {R}$
17 16 sbcth
18 4 17 ax-mp
19 sbcimg
20 4 19 ax-mp
21 18 20 mpbi
22 sbcan
23 sbcel1v
24 21 22 23 3imtr3i
25 12 24 sylanbr
26 7 25 mpan2 ${⊢}{x}\in {A}\to \left\{{x}\right\}\in {R}$
27 1 26 fmpti ${⊢}{F}:{A}⟶{R}$
28 1 fvmpt2 ${⊢}\left({x}\in {A}\wedge \left\{{x}\right\}\in {R}\right)\to {F}\left({x}\right)=\left\{{x}\right\}$
29 26 28 mpdan ${⊢}{x}\in {A}\to {F}\left({x}\right)=\left\{{x}\right\}$
30 sneq ${⊢}{x}={y}\to \left\{{x}\right\}=\left\{{y}\right\}$
31 30 1 4 fvmpt3i ${⊢}{y}\in {A}\to {F}\left({y}\right)=\left\{{y}\right\}$
32 29 31 eqeqan12d ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to \left({F}\left({x}\right)={F}\left({y}\right)↔\left\{{x}\right\}=\left\{{y}\right\}\right)$
33 vex ${⊢}{x}\in \mathrm{V}$
34 sneqbg ${⊢}{x}\in \mathrm{V}\to \left(\left\{{x}\right\}=\left\{{y}\right\}↔{x}={y}\right)$
35 33 34 ax-mp ${⊢}\left\{{x}\right\}=\left\{{y}\right\}↔{x}={y}$
36 32 35 syl6bb ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to \left({F}\left({x}\right)={F}\left({y}\right)↔{x}={y}\right)$
37 36 biimpd ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
38 37 rgen2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
39 dff13 ${⊢}{F}:{A}\underset{1-1}{⟶}{R}↔\left({F}:{A}⟶{R}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
40 27 38 39 mpbir2an ${⊢}{F}:{A}\underset{1-1}{⟶}{R}$
41 f1f1orn ${⊢}{F}:{A}\underset{1-1}{⟶}{R}\to {F}:{A}\underset{1-1 onto}{⟶}\mathrm{ran}{F}$
42 40 41 ax-mp ${⊢}{F}:{A}\underset{1-1 onto}{⟶}\mathrm{ran}{F}$
43 rnmptsn ${⊢}\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)=\left\{{u}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}$
44 1 rneqi ${⊢}\mathrm{ran}{F}=\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)$
45 43 44 2 3eqtr4i ${⊢}\mathrm{ran}{F}={R}$
46 f1oeq3 ${⊢}\mathrm{ran}{F}={R}\to \left({F}:{A}\underset{1-1 onto}{⟶}\mathrm{ran}{F}↔{F}:{A}\underset{1-1 onto}{⟶}{R}\right)$
47 45 46 ax-mp ${⊢}{F}:{A}\underset{1-1 onto}{⟶}\mathrm{ran}{F}↔{F}:{A}\underset{1-1 onto}{⟶}{R}$
48 42 47 mpbi ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{R}$