Metamath Proof Explorer


Theorem metakunt2

Description: A is an endomapping. (Contributed by metakunt, 23-May-2024)

Ref Expression
Hypotheses metakunt2.1 φ M
metakunt2.2 φ I
metakunt2.3 φ I M
metakunt2.4 A = x 1 M if x = M I if x < I x x + 1
Assertion metakunt2 φ A : 1 M 1 M

Proof

Step Hyp Ref Expression
1 metakunt2.1 φ M
2 metakunt2.2 φ I
3 metakunt2.3 φ I M
4 metakunt2.4 A = x 1 M if x = M I if x < I x x + 1
5 eleq1 I = if x = M I if x < I x x + 1 I 1 M if x = M I if x < I x x + 1 1 M
6 eleq1 if x < I x x + 1 = if x = M I if x < I x x + 1 if x < I x x + 1 1 M if x = M I if x < I x x + 1 1 M
7 1zzd φ x 1 M x = M 1
8 1 nnzd φ M
9 8 ad2antrr φ x 1 M x = M M
10 2 nnzd φ I
11 10 ad2antrr φ x 1 M x = M I
12 2 nnge1d φ 1 I
13 12 ad2antrr φ x 1 M x = M 1 I
14 3 ad2antrr φ x 1 M x = M I M
15 7 9 11 13 14 elfzd φ x 1 M x = M I 1 M
16 eleq1 x = if x < I x x + 1 x 1 M if x < I x x + 1 1 M
17 eleq1 x + 1 = if x < I x x + 1 x + 1 1 M if x < I x x + 1 1 M
18 simpllr φ x 1 M ¬ x = M x < I x 1 M
19 1zzd φ x 1 M ¬ x = M ¬ x < I 1
20 8 ad2antrr φ x 1 M ¬ x = M ¬ x < I M
21 elfznn x 1 M x
22 21 nnzd x 1 M x
23 22 ad2antlr φ x 1 M ¬ x = M ¬ x < I x
24 23 peano2zd φ x 1 M ¬ x = M ¬ x < I x + 1
25 0p1e1 0 + 1 = 1
26 0red x 1 M 0
27 21 nnred x 1 M x
28 1red x 1 M 1
29 21 nnnn0d x 1 M x 0
30 29 nn0ge0d x 1 M 0 x
31 26 27 28 30 leadd1dd x 1 M 0 + 1 x + 1
32 25 31 eqbrtrrid x 1 M 1 x + 1
33 32 ad2antlr φ x 1 M ¬ x = M ¬ x < I 1 x + 1
34 simplr φ x 1 M ¬ x = M x 1 M
35 neqne ¬ x = M x M
36 35 adantl φ x 1 M ¬ x = M x M
37 34 36 fzne2d φ x 1 M ¬ x = M x < M
38 37 adantrr φ x 1 M ¬ x = M ¬ x < I x < M
39 22 adantl φ x 1 M x
40 8 adantr φ x 1 M M
41 39 40 zltp1led φ x 1 M x < M x + 1 M
42 41 adantr φ x 1 M ¬ x = M ¬ x < I x < M x + 1 M
43 38 42 mpbid φ x 1 M ¬ x = M ¬ x < I x + 1 M
44 19 20 24 33 43 elfzd φ x 1 M ¬ x = M ¬ x < I x + 1 1 M
45 44 anassrs φ x 1 M ¬ x = M ¬ x < I x + 1 1 M
46 16 17 18 45 ifbothda φ x 1 M ¬ x = M if x < I x x + 1 1 M
47 5 6 15 46 ifbothda φ x 1 M if x = M I if x < I x x + 1 1 M
48 47 4 fmptd φ A : 1 M 1 M