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 Au=\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 Au=\left\{x\right\}\right\}$$
3		eqid	$$⊢\left\{x\right\}=\left\{x\right\}$$
4		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
5		eqsbc1	$$⊢\left\{x\right\}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{x\right\}\right)$$
6	4 5	ax-mp	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{x\right\}$$
7	3 6	mpbir	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}$$
8		sbcel2	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}x\in A\leftrightarrow x\in ⦋\left\{x\right\}/u⦌A$$
9		csbconstg	$$⊢\left\{x\right\}\in \mathrm{V}\to ⦋\left\{x\right\}/u⦌A=A$$
10	4 9	ax-mp	$$⊢⦋\left\{x\right\}/u⦌A=A$$
11	10	eleq2i	$$⊢x\in ⦋\left\{x\right\}/u⦌A\leftrightarrow x\in A$$
12	8 11	bitri	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}x\in A\leftrightarrow x\in A$$
13	2	abeq2i	$$⊢u\in R\leftrightarrow \exists x\in Au=\left\{x\right\}$$
14		df-rex	$$⊢\exists x\in Au=\left\{x\right\}\leftrightarrow \exists x\left(x\in A\wedge u=\left\{x\right\}\right)$$
15	13 14	sylbbr	$$⊢\exists x\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	$$⊢\left\{x\right\}\in \mathrm{V}\to \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(\left(x\in A\wedge u=\left\{x\right\}\right)\to u\in R\right)$$
18	4 17	ax-mp	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(\left(x\in A\wedge u=\left\{x\right\}\right)\to u\in R\right)$$
19		sbcimg	$$⊢\left\{x\right\}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(\left(x\in A\wedge u=\left\{x\right\}\right)\to u\in R\right)\leftrightarrow \left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(x\in A\wedge u=\left\{x\right\}\right)\to \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u\in R\right)\right)$$
20	4 19	ax-mp	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(\left(x\in A\wedge u=\left\{x\right\}\right)\to u\in R\right)\leftrightarrow \left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(x\in A\wedge u=\left\{x\right\}\right)\to \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u\in R\right)$$
21	18 20	mpbi	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(x\in A\wedge u=\left\{x\right\}\right)\to \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u\in R$$
22		sbcan	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}\left(x\in A\wedge u=\left\{x\right\}\right)\leftrightarrow \left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}\right)$$
23		sbcel1v	$$⊢\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u\in R\leftrightarrow \left\{x\right\}\in R$$
24	21 22 23	3imtr3i	$$⊢\left(\underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}\right)\to \left\{x\right\}\in R$$
25	12 24	sylanbr	$$⊢\left(x\in A\wedge \underset{\dot{}}{[}\left\{x\right\}/u\underset{\dot{}}{]}u=\left\{x\right\}\right)\to \left\{x\right\}\in R$$
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)\leftrightarrow \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\}\leftrightarrow x=y\right)$$
35	33 34	ax-mp	$$⊢\left\{x\right\}=\left\{y\right\}\leftrightarrow x=y$$
36	32 35	bitrdi	$$⊢\left(x\in A\wedge y\in A\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow 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\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
39		dff13	$$⊢F:A\underset{1-1}{⟶}R\leftrightarrow \left(F:A⟶R\wedge \forall x\in A\forall y\in A\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 Au=\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\leftrightarrow F:A\underset{1-1\; onto}{⟶}R\right)$$
47	45 46	ax-mp	$$⊢F:A\underset{1-1\; onto}{⟶}\mathrm{ran}F\leftrightarrow F:A\underset{1-1\; onto}{⟶}R$$
48	42 47	mpbi	$$⊢F:A\underset{1-1\; onto}{⟶}R$$