This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimpi ⊢ ( ( 𝐷 ∘ 𝑓 ) = 0 → ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
52 51 adantl ⊢ ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
53 52 adantl ⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) )
54 fcofo ⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = ( I ↾ ℕ0 ) ) → 𝐷 : ℕ0 –onto→ ℕ0 )
55 43 45 53 54 syl3anc ⊢ ( ( 𝐷 : ℕ0 ⟶ ℕ0 ∧ ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) ) → 𝐷 : ℕ0 –onto→ ℕ0 )
56 55 ex ⊢ ( 𝐷 : ℕ0 ⟶ ℕ0 → ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → 𝐷 : ℕ0 –onto→ ℕ0 ) )
57 41 42 56 mp2b ⊢ ( ( 𝑓 : ℕ0 ⟶ ℕ0 ∧ ( 𝐷 ∘ 𝑓 ) = 0 ) → 𝐷 : ℕ0 –onto→ ℕ0 )
58 40 57 mtand ⊢ ( 𝑓 : ℕ0 ⟶ ℕ0 → ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
59 7 58 syl ⊢ ( 𝑓 ∈ 𝐵 → ¬ ( 𝐷 ∘ 𝑓 ) = 0 )
60 6 59 mprgbir ⊢ ∀ 𝑓 ∈ 𝐵 ( 𝐷 ∘ 𝑓 ) ≠ 0