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	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
	smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
Assertion	smndex2dnrinv	⊢ ∀ 𝑓 ∈ 𝐵 ( 𝐷 ∘ 𝑓 ) ≠ 0

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
4		smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
5		df-ne	⊢ ( ( 𝐷 ∘ 𝑓 ) ≠ 0 ↔ ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
6	5	ralbii	⊢ ( ∀ 𝑓 ∈ 𝐵 ( 𝐷 ∘ 𝑓 ) ≠ 0 ↔ ∀ 𝑓 ∈ 𝐵 ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
7	1 2	efmndbasf	⊢ ( 𝑓 ∈ 𝐵 → 𝑓 : ℕ0 ⟶ ℕ0 )
8		1nn0	⊢ 1 ∈ ℕ0
9		nn0z	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
10		0zd	⊢ ( 𝑥 ∈ ℕ0 → 0 ∈ ℤ )
11		zneo	⊢ ( ( 𝑥 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 2 · 𝑥 ) ≠ ( ( 2 · 0 ) + 1 ) )
12	9 10 11	syl2anc	⊢ ( 𝑥 ∈ ℕ0 → ( 2 · 𝑥 ) ≠ ( ( 2 · 0 ) + 1 ) )
13		2t0e0	⊢ ( 2 · 0 ) = 0
14	13	oveq1i	⊢ ( ( 2 · 0 ) + 1 ) = ( 0 + 1 )
15		0p1e1	⊢ ( 0 + 1 ) = 1
16	14 15	eqtri	⊢ ( ( 2 · 0 ) + 1 ) = 1
17	16	a1i	⊢ ( 𝑥 ∈ ℕ0 → ( ( 2 · 0 ) + 1 ) = 1 )
18	12 17	neeqtrd	⊢ ( 𝑥 ∈ ℕ0 → ( 2 · 𝑥 ) ≠ 1 )
19	18	necomd	⊢ ( 𝑥 ∈ ℕ0 → 1 ≠ ( 2 · 𝑥 ) )
20	19	neneqd	⊢ ( 𝑥 ∈ ℕ0 → ¬ 1 = ( 2 · 𝑥 ) )
21	20	nrex	⊢ ¬ ∃ 𝑥 ∈ ℕ0 1 = ( 2 · 𝑥 )
22		1ex	⊢ 1 ∈ V
23		eqeq1	⊢ ( 𝑦 = 1 → ( 𝑦 = ( 2 · 𝑥 ) ↔ 1 = ( 2 · 𝑥 ) ) )
24	23	rexbidv	⊢ ( 𝑦 = 1 → ( ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ0 1 = ( 2 · 𝑥 ) ) )
25	22 24	elab	⊢ ( 1 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } ↔ ∃ 𝑥 ∈ ℕ0 1 = ( 2 · 𝑥 ) )
26	21 25	mtbir	⊢ ¬ 1 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) }
27		nelss	⊢ ( ( 1 ∈ ℕ0 ∧ ¬ 1 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } ) → ¬ ℕ0 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } )
28	8 26 27	mp2an	⊢ ¬ ℕ0 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) }
29	28	intnan	⊢ ¬ ( { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } ⊆ ℕ0 ∧ ℕ0 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } )
30		eqss	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } = ℕ0 ↔ ( { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } ⊆ ℕ0 ∧ ℕ0 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } ) )
31	29 30	mtbir	⊢ ¬ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } = ℕ0
32	4	rnmpt	⊢ ran 𝐷 = { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) }
33	32	eqeq1i	⊢ ( ran 𝐷 = ℕ0 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ ℕ0 𝑦 = ( 2 · 𝑥 ) } = ℕ0 )
34	31 33	mtbir	⊢ ¬ ran 𝐷 = ℕ0
35	34	olci	⊢ ( ¬ 𝐷 Fn ℕ0 ∨ ¬ ran 𝐷 = ℕ0 )
36		ianor	⊢ ( ¬ ( 𝐷 Fn ℕ0 ∧ ran 𝐷 = ℕ0 ) ↔ ( ¬ 𝐷 Fn ℕ0 ∨ ¬ ran 𝐷 = ℕ0 ) )
37		df-fo	⊢ ( 𝐷 : ℕ0 –onto→ ℕ0 ↔ ( 𝐷 Fn ℕ0 ∧ ran 𝐷 = ℕ0 ) )
38	36 37	xchnxbir	⊢ ( ¬ 𝐷 : ℕ0 –onto→ ℕ0 ↔ ( ¬ 𝐷 Fn ℕ0 ∨ ¬ ran 𝐷 = ℕ0 ) )
39	35 38	mpbir	⊢ ¬ 𝐷 : ℕ0 –onto→ ℕ0
40	39	a1i	⊢ ( 𝑓 : ℕ0 ⟶ ℕ0 → ¬ 𝐷 : ℕ0 –onto→ ℕ0 )
41	1 2 3 4	smndex2dbas	⊢ 𝐷 ∈ 𝐵
42	1 2	efmndbasf	⊢ ( 𝐷 ∈ 𝐵 → 𝐷 : ℕ0 ⟶ ℕ0 )
43		simpl	⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → 𝐷 : ℕ0 ⟶ ℕ0 )
44		simpl	⊢ ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → 𝑓 : ℕ0 ⟶ ℕ0 )
45	44	adantl	⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → 𝑓 : ℕ0 ⟶ ℕ0 )
46		nn0ex	⊢ ℕ0 ∈ V
47	1	efmndid	⊢ ( ℕ0 ∈ V → ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 ) )
48	46 47	ax-mp	⊢ ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 )
49	3 48	eqtr4i	⊢ 0 = ( I ↾ ℕ0 )
50	49	eqeq2i	⊢ ( ( 𝐷 ∘ 𝑓 ) = 0 ↔ ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
51	50	bilani	⊢ ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
52	51	adantl	⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
53		fcofo	⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) ) → 𝐷 : ℕ0 –onto→ ℕ0 )
54	43 45 52 53	syl3anc	⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → 𝐷 : ℕ0 –onto→ ℕ0 )
55	54	ex	⊢ ( 𝐷 : ℕ0 ⟶ ℕ0 → ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → 𝐷 : ℕ0 –onto→ ℕ0 ) )
56	41 42 55	mp2b	⊢ ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → 𝐷 : ℕ0 –onto→ ℕ0 )
57	40 56	mtand	⊢ ( 𝑓 : ℕ0 ⟶ ℕ0 → ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
58	7 57	syl	⊢ ( 𝑓 ∈ 𝐵 → ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
59	6 58	mprgbir	⊢ ∀ 𝑓 ∈ 𝐵 ( 𝐷 ∘ 𝑓 ) ≠ 0