Theorem smndex2dnrinv

Description: The doubling function D has no right inverse in the monoid of endofunctions on NN0 . (Contributed by AV, 18-Feb-2024)

	Ref	Expression
Hypotheses	smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
	smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
	smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
	smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
Assertion	smndex2dnrinv	$$⊢\forall f\in BD\circ f\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
2		smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
3		smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
4		smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
5		df-ne	$$⊢D\circ f\ne \underset{\dot{}}{0}\leftrightarrow \neg D\circ f=\underset{\dot{}}{0}$$
6	5	ralbii	$$⊢\forall f\in BD\circ f\ne \underset{\dot{}}{0}\leftrightarrow \forall f\in B\neg D\circ f=\underset{\dot{}}{0}$$
7	1 2	efmndbasf	$$⊢f\in B\to f:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
8		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9		nn0z	$$⊢x\in {\mathbb{N}}_0\to x\in \mathbb{Z}$$
10		0zd	$$⊢x\in {\mathbb{N}}_0\to 0\in \mathbb{Z}$$
11		zneo	$$⊢\left(x\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to 2x\ne 2\cdot 0+1$$
12	9 10 11	syl2anc	$$⊢x\in {\mathbb{N}}_0\to 2x\ne 2\cdot 0+1$$
13		2t0e0	$$⊢2\cdot 0=0$$
14	13	oveq1i	$$⊢2\cdot 0+1=0+1$$
15		0p1e1	$$⊢0+1=1$$
16	14 15	eqtri	$$⊢2\cdot 0+1=1$$
17	16	a1i	$$⊢x\in {\mathbb{N}}_0\to 2\cdot 0+1=1$$
18	12 17	neeqtrd	$$⊢x\in {\mathbb{N}}_0\to 2x\ne 1$$
19	18	necomd	$$⊢x\in {\mathbb{N}}_0\to 1\ne 2x$$
20	19	neneqd	$$⊢x\in {\mathbb{N}}_0\to \neg 1=2x$$
21	20	nrex	$$⊢\neg \exists x\in {\mathbb{N}}_{0}1=2x$$
22		1ex	$$⊢1\in \mathrm{V}$$
23		eqeq1	$$⊢y=1\to \left(y=2x\leftrightarrow 1=2x\right)$$
24	23	rexbidv	$$⊢y=1\to \left(\exists x\in {\mathbb{N}}_{0}y=2x\leftrightarrow \exists x\in {\mathbb{N}}_{0}1=2x\right)$$
25	22 24	elab	$$⊢1\in \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\leftrightarrow \exists x\in {\mathbb{N}}_{0}1=2x$$
26	21 25	mtbir	$$⊢\neg 1\in \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}$$
27		nelss	$$⊢\left(1\in {\mathbb{N}}_0\wedge \neg 1\in \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\right)\to \neg {\mathbb{N}}_0\subseteq \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}$$
28	8 26 27	mp2an	$$⊢\neg {\mathbb{N}}_0\subseteq \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}$$
29	28	intnan	$$⊢\neg \left(\left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\subseteq {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\right)$$
30		eqss	$$⊢\left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}={\mathbb{N}}_0\leftrightarrow \left(\left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\subseteq {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}\right)$$
31	29 30	mtbir	$$⊢\neg \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}={\mathbb{N}}_0$$
32	4	rnmpt	$$⊢\mathrm{ran}D=\left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}$$
33	32	eqeq1i	$$⊢\mathrm{ran}D={\mathbb{N}}_0\leftrightarrow \left\{y|\exists x\in {\mathbb{N}}_{0}y=2x\right\}={\mathbb{N}}_0$$
34	31 33	mtbir	$$⊢\neg \mathrm{ran}D={\mathbb{N}}_0$$
35	34	olci	$$⊢\left(\neg DFn{\mathbb{N}}_0\vee \neg \mathrm{ran}D={\mathbb{N}}_0\right)$$
36		ianor	$$⊢\neg \left(DFn{\mathbb{N}}_0\wedge \mathrm{ran}D={\mathbb{N}}_0\right)\leftrightarrow \left(\neg DFn{\mathbb{N}}_0\vee \neg \mathrm{ran}D={\mathbb{N}}_0\right)$$
37		df-fo	$$⊢D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0\leftrightarrow \left(DFn{\mathbb{N}}_0\wedge \mathrm{ran}D={\mathbb{N}}_0\right)$$
38	36 37	xchnxbir	$$⊢\neg D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0\leftrightarrow \left(\neg DFn{\mathbb{N}}_0\vee \neg \mathrm{ran}D={\mathbb{N}}_0\right)$$
39	35 38	mpbir	$$⊢\neg D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0$$
40	39	a1i	$$⊢f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \neg D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0$$
41	1 2 3 4	smndex2dbas	$$⊢D\in B$$
42	1 2	efmndbasf	$$⊢D\in B\to D:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
43		simpl	$$⊢\left(D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge \left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\right)\to D:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
44		simpl	$$⊢\left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\to f:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
45	44	adantl	$$⊢\left(D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge \left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\right)\to f:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
46		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
47	1	efmndid	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
48	46 47	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
49	3 48	eqtr4i	$$⊢\underset{\dot{}}{0}={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}$$
50	49	eqeq2i	$$⊢D\circ f=\underset{\dot{}}{0}\leftrightarrow D\circ f={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}$$
51	50	bilani	$$⊢\left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\to D\circ f={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}$$
52	51	adantl	$$⊢\left(D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge \left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\right)\to D\circ f={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}$$
53		fcofo	$$⊢\left(D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\to D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0$$
54	43 45 52 53	syl3anc	$$⊢\left(D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge \left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\right)\to D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0$$
55	54	ex	$$⊢D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \left(\left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\to D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0\right)$$
56	41 42 55	mp2b	$$⊢\left(f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge D\circ f=\underset{\dot{}}{0}\right)\to D:{\mathbb{N}}_0\underset{onto}{⟶}{\mathbb{N}}_0$$
57	40 56	mtand	$$⊢f:{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \neg D\circ f=\underset{\dot{}}{0}$$
58	7 57	syl	$$⊢f\in B\to \neg D\circ f=\underset{\dot{}}{0}$$
59	6 58	mprgbir	$$⊢\forall f\in BD\circ f\ne \underset{\dot{}}{0}$$