Metamath Proof Explorer


Theorem metakunt25

Description: B is a permutation. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt25.1 φ M
metakunt25.2 φ I
metakunt25.3 φ I M
metakunt25.4 B = x 1 M if x = M M if x < I x + M - I x + 1 - I
Assertion metakunt25 φ B : 1 M 1-1 onto 1 M

Proof

Step Hyp Ref Expression
1 metakunt25.1 φ M
2 metakunt25.2 φ I
3 metakunt25.3 φ I M
4 metakunt25.4 B = x 1 M if x = M M if x < I x + M - I x + 1 - I
5 eqid x 1 I 1 x + M - I = x 1 I 1 x + M - I
6 1 2 3 5 metakunt15 φ x 1 I 1 x + M - I : 1 I 1 1-1 onto M - I + 1 M 1
7 eqid x I M 1 x + 1 - I = x I M 1 x + 1 - I
8 1 2 3 7 metakunt16 φ x I M 1 x + 1 - I : I M 1 1-1 onto 1 M I
9 f1osng M M M M : M 1-1 onto M
10 1 1 9 syl2anc φ M M : M 1-1 onto M
11 1 2 3 metakunt18 φ 1 I 1 I M 1 = 1 I 1 M = I M 1 M = M - I + 1 M 1 1 M I = M - I + 1 M 1 M = 1 M I M =
12 11 simpld φ 1 I 1 I M 1 = 1 I 1 M = I M 1 M =
13 12 simp1d φ 1 I 1 I M 1 =
14 12 simp2d φ 1 I 1 M =
15 12 simp3d φ I M 1 M =
16 11 simprd φ M - I + 1 M 1 1 M I = M - I + 1 M 1 M = 1 M I M =
17 16 simp1d φ M - I + 1 M 1 1 M I =
18 16 simp2d φ M - I + 1 M 1 M =
19 16 simp3d φ 1 M I M =
20 eleq1 M = if x = M M if x < I x + M - I x + 1 - I M if x = M M if x < I x + M - I x + 1 - I
21 eleq1 if x < I x + M - I x + 1 - I = if x = M M if x < I x + M - I x + 1 - I if x < I x + M - I x + 1 - I if x = M M if x < I x + M - I x + 1 - I
22 1 nnzd φ M
23 22 adantr φ x 1 M M
24 23 adantr φ x 1 M x = M M
25 eleq1 x + M - I = if x < I x + M - I x + 1 - I x + M - I if x < I x + M - I x + 1 - I
26 eleq1 x + 1 - I = if x < I x + M - I x + 1 - I x + 1 - I if x < I x + M - I x + 1 - I
27 elfzelz x 1 M x
28 27 adantl φ x 1 M x
29 28 adantr φ x 1 M ¬ x = M x
30 29 adantr φ x 1 M ¬ x = M x < I x
31 23 ad2antrr φ x 1 M ¬ x = M x < I M
32 2 nnzd φ I
33 32 adantr φ x 1 M I
34 33 adantr φ x 1 M ¬ x = M I
35 34 adantr φ x 1 M ¬ x = M x < I I
36 31 35 zsubcld φ x 1 M ¬ x = M x < I M I
37 30 36 zaddcld φ x 1 M ¬ x = M x < I x + M - I
38 29 adantr φ x 1 M ¬ x = M ¬ x < I x
39 1zzd φ x 1 M ¬ x = M ¬ x < I 1
40 34 adantr φ x 1 M ¬ x = M ¬ x < I I
41 39 40 zsubcld φ x 1 M ¬ x = M ¬ x < I 1 I
42 38 41 zaddcld φ x 1 M ¬ x = M ¬ x < I x + 1 - I
43 25 26 37 42 ifbothda φ x 1 M ¬ x = M if x < I x + M - I x + 1 - I
44 20 21 24 43 ifbothda φ x 1 M if x = M M if x < I x + M - I x + 1 - I
45 44 4 fmptd φ B : 1 M
46 45 ffnd φ B Fn 1 M
47 1 2 3 4 5 7 metakunt19 φ x 1 I 1 x + M - I Fn 1 I 1 x I M 1 x + 1 - I Fn I M 1 x 1 I 1 x + M - I x I M 1 x + 1 - I Fn 1 I 1 I M 1 M M Fn M
48 47 simpld φ x 1 I 1 x + M - I Fn 1 I 1 x I M 1 x + 1 - I Fn I M 1 x 1 I 1 x + M - I x I M 1 x + 1 - I Fn 1 I 1 I M 1
49 48 simp3d φ x 1 I 1 x + M - I x I M 1 x + 1 - I Fn 1 I 1 I M 1
50 47 simprd φ M M Fn M
51 1 2 3 metakunt24 φ 1 I 1 I M 1 M = 1 M = 1 I 1 I M 1 M 1 M = M - I + 1 M 1 1 M I M
52 51 simp1d φ 1 I 1 I M 1 M =
53 49 50 52 fnund φ x 1 I 1 x + M - I x I M 1 x + 1 - I M M Fn 1 I 1 I M 1 M
54 51 simp2d φ 1 M = 1 I 1 I M 1 M
55 1 adantr φ y 1 M M
56 2 adantr φ y 1 M I
57 3 adantr φ y 1 M I M
58 simpr φ y 1 M y 1 M
59 55 56 57 4 5 7 58 metakunt23 φ y 1 M B y = x 1 I 1 x + M - I x I M 1 x + 1 - I M M y
60 46 53 54 59 eqfnfv2d2 φ B = x 1 I 1 x + M - I x I M 1 x + 1 - I M M
61 51 simp3d φ 1 M = M - I + 1 M 1 1 M I M
62 6 8 10 13 14 15 17 18 19 60 54 61 metakunt17 φ B : 1 M 1-1 onto 1 M