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 
|- M = ( EndoFMnd ` NN0 )
smndex2dbas.b 
|- B = ( Base ` M )
smndex2dbas.0 
|- .0. = ( 0g ` M )
smndex2dbas.d 
|- D = ( x e. NN0 |-> ( 2 x. x ) )
Assertion smndex2dnrinv 
|- A. f e. B ( D o. f ) =/= .0.

Proof

Step Hyp Ref Expression
1 smndex2dbas.m 
 |-  M = ( EndoFMnd ` NN0 )
2 smndex2dbas.b 
 |-  B = ( Base ` M )
3 smndex2dbas.0 
 |-  .0. = ( 0g ` M )
4 smndex2dbas.d 
 |-  D = ( x e. NN0 |-> ( 2 x. x ) )
5 df-ne 
 |-  ( ( D o. f ) =/= .0. <-> -. ( D o. f ) = .0. )
6 5 ralbii 
 |-  ( A. f e. B ( D o. f ) =/= .0. <-> A. f e. B -. ( D o. f ) = .0. )
7 1 2 efmndbasf 
 |-  ( f e. B -> f : NN0 --> NN0 )
8 1nn0 
 |-  1 e. NN0
9 nn0z 
 |-  ( x e. NN0 -> x e. ZZ )
10 0zd 
 |-  ( x e. NN0 -> 0 e. ZZ )
11 zneo 
 |-  ( ( x e. ZZ /\ 0 e. ZZ ) -> ( 2 x. x ) =/= ( ( 2 x. 0 ) + 1 ) )
12 9 10 11 syl2anc 
 |-  ( x e. NN0 -> ( 2 x. x ) =/= ( ( 2 x. 0 ) + 1 ) )
13 2t0e0 
 |-  ( 2 x. 0 ) = 0
14 13 oveq1i 
 |-  ( ( 2 x. 0 ) + 1 ) = ( 0 + 1 )
15 0p1e1 
 |-  ( 0 + 1 ) = 1
16 14 15 eqtri 
 |-  ( ( 2 x. 0 ) + 1 ) = 1
17 16 a1i 
 |-  ( x e. NN0 -> ( ( 2 x. 0 ) + 1 ) = 1 )
18 12 17 neeqtrd 
 |-  ( x e. NN0 -> ( 2 x. x ) =/= 1 )
19 18 necomd 
 |-  ( x e. NN0 -> 1 =/= ( 2 x. x ) )
20 19 neneqd 
 |-  ( x e. NN0 -> -. 1 = ( 2 x. x ) )
21 20 nrex 
 |-  -. E. x e. NN0 1 = ( 2 x. x )
22 1ex 
 |-  1 e. _V
23 eqeq1 
 |-  ( y = 1 -> ( y = ( 2 x. x ) <-> 1 = ( 2 x. x ) ) )
24 23 rexbidv 
 |-  ( y = 1 -> ( E. x e. NN0 y = ( 2 x. x ) <-> E. x e. NN0 1 = ( 2 x. x ) ) )
25 22 24 elab 
 |-  ( 1 e. { y | E. x e. NN0 y = ( 2 x. x ) } <-> E. x e. NN0 1 = ( 2 x. x ) )
26 21 25 mtbir 
 |-  -. 1 e. { y | E. x e. NN0 y = ( 2 x. x ) }
27 nelss 
 |-  ( ( 1 e. NN0 /\ -. 1 e. { y | E. x e. NN0 y = ( 2 x. x ) } ) -> -. NN0 C_ { y | E. x e. NN0 y = ( 2 x. x ) } )
28 8 26 27 mp2an 
 |-  -. NN0 C_ { y | E. x e. NN0 y = ( 2 x. x ) }
29 28 intnan 
 |-  -. ( { y | E. x e. NN0 y = ( 2 x. x ) } C_ NN0 /\ NN0 C_ { y | E. x e. NN0 y = ( 2 x. x ) } )
30 eqss 
 |-  ( { y | E. x e. NN0 y = ( 2 x. x ) } = NN0 <-> ( { y | E. x e. NN0 y = ( 2 x. x ) } C_ NN0 /\ NN0 C_ { y | E. x e. NN0 y = ( 2 x. x ) } ) )
31 29 30 mtbir 
 |-  -. { y | E. x e. NN0 y = ( 2 x. x ) } = NN0
32 4 rnmpt 
 |-  ran D = { y | E. x e. NN0 y = ( 2 x. x ) }
33 32 eqeq1i 
 |-  ( ran D = NN0 <-> { y | E. x e. NN0 y = ( 2 x. x ) } = NN0 )
34 31 33 mtbir 
 |-  -. ran D = NN0
35 34 olci 
 |-  ( -. D Fn NN0 \/ -. ran D = NN0 )
36 ianor 
 |-  ( -. ( D Fn NN0 /\ ran D = NN0 ) <-> ( -. D Fn NN0 \/ -. ran D = NN0 ) )
37 df-fo 
 |-  ( D : NN0 -onto-> NN0 <-> ( D Fn NN0 /\ ran D = NN0 ) )
38 36 37 xchnxbir 
 |-  ( -. D : NN0 -onto-> NN0 <-> ( -. D Fn NN0 \/ -. ran D = NN0 ) )
39 35 38 mpbir 
 |-  -. D : NN0 -onto-> NN0
40 39 a1i 
 |-  ( f : NN0 --> NN0 -> -. D : NN0 -onto-> NN0 )
41 1 2 3 4 smndex2dbas 
 |-  D e. B
42 1 2 efmndbasf 
 |-  ( D e. B -> D : NN0 --> NN0 )
43 simpl 
 |-  ( ( D : NN0 --> NN0 /\ ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) ) -> D : NN0 --> NN0 )
44 simpl 
 |-  ( ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) -> f : NN0 --> NN0 )
45 44 adantl 
 |-  ( ( D : NN0 --> NN0 /\ ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) ) -> f : NN0 --> NN0 )
46 nn0ex 
 |-  NN0 e. _V
47 1 efmndid 
 |-  ( NN0 e. _V -> ( _I |` NN0 ) = ( 0g ` M ) )
48 46 47 ax-mp 
 |-  ( _I |` NN0 ) = ( 0g ` M )
49 3 48 eqtr4i 
 |-  .0. = ( _I |` NN0 )
50 49 eqeq2i 
 |-  ( ( D o. f ) = .0. <-> ( D o. f ) = ( _I |` NN0 ) )
51 50 biimpi 
 |-  ( ( D o. f ) = .0. -> ( D o. f ) = ( _I |` NN0 ) )
52 51 adantl 
 |-  ( ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) -> ( D o. f ) = ( _I |` NN0 ) )
53 52 adantl 
 |-  ( ( D : NN0 --> NN0 /\ ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) ) -> ( D o. f ) = ( _I |` NN0 ) )
54 fcofo 
 |-  ( ( D : NN0 --> NN0 /\ f : NN0 --> NN0 /\ ( D o. f ) = ( _I |` NN0 ) ) -> D : NN0 -onto-> NN0 )
55 43 45 53 54 syl3anc 
 |-  ( ( D : NN0 --> NN0 /\ ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) ) -> D : NN0 -onto-> NN0 )
56 55 ex 
 |-  ( D : NN0 --> NN0 -> ( ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) -> D : NN0 -onto-> NN0 ) )
57 41 42 56 mp2b 
 |-  ( ( f : NN0 --> NN0 /\ ( D o. f ) = .0. ) -> D : NN0 -onto-> NN0 )
58 40 57 mtand 
 |-  ( f : NN0 --> NN0 -> -. ( D o. f ) = .0. )
59 7 58 syl 
 |-  ( f e. B -> -. ( D o. f ) = .0. )
60 6 59 mprgbir 
 |-  A. f e. B ( D o. f ) =/= .0.