Metamath Proof Explorer

Theorem metakunt25

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

Ref Expression
Hypotheses metakunt25.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt25.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt25.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt25.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
Assertion metakunt25 ( 𝜑 → 𝐵 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )

Proof

Step Hyp Ref Expression
1 metakunt25.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt25.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt25.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt25.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5 eqid ⊢ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6 1 2 3 5 metakunt15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) : ( 1 ... ( 𝐼 − 1 ) ) –1-1-onto→ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )
7 eqid ⊢ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
8 1 2 3 7 metakunt16 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) : ( 𝐼 ... ( 𝑀 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑀 − 𝐼 ) ) )
9 f1osng ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → { ⟨ 𝑀 , 𝑀 ⟩ } : { 𝑀 } –1-1-onto→ { 𝑀 } )
10 1 1 9 syl2anc ⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 ⟩ } : { 𝑀 } –1-1-onto→ { 𝑀 } )
11 1 2 3 metakunt18 ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )
12 11 simpld ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
13 12 simp1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
14 12 simp2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
15 12 simp3d ⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
16 11 simprd ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) )
17 16 simp1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ )
18 16 simp2d ⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
19 16 simp3d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ )
20 eleq1 ⊢ ( 𝑀 = if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) → ( 𝑀 ∈ ℤ ↔ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∈ ℤ ) )
21 eleq1 ⊢ ( if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) = if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) → ( if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ∈ ℤ ↔ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∈ ℤ ) )
22 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℤ )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 𝑀 ∈ ℤ )
25 eleq1 ⊢ ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) = if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) → ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) ∈ ℤ ↔ if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ∈ ℤ ) )
26 eleq1 ⊢ ( ( 𝑥 + ( 1 − 𝐼 ) ) = if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) → ( ( 𝑥 + ( 1 − 𝐼 ) ) ∈ ℤ ↔ if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ∈ ℤ ) )
27 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℤ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ∈ ℤ )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → 𝑥 ∈ ℤ )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → 𝑥 ∈ ℤ )
31 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → 𝑀 ∈ ℤ )
32 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ∈ ℤ )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → 𝐼 ∈ ℤ )
35 34 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → 𝐼 ∈ ℤ )
36 31 35 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → ( 𝑀 − 𝐼 ) ∈ ℤ )
37 30 36 zaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → ( 𝑥 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
38 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → 𝑥 ∈ ℤ )
39 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → 1 ∈ ℤ )
40 34 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → 𝐼 ∈ ℤ )
41 39 40 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → ( 1 − 𝐼 ) ∈ ℤ )
42 38 41 zaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → ( 𝑥 + ( 1 − 𝐼 ) ) ∈ ℤ )
43 25 26 37 42 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ∈ ℤ )
44 20 21 24 43 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∈ ℤ )
45 44 4 fmptd ⊢ ( 𝜑 → 𝐵 : ( 1 ... 𝑀 ) ⟶ ℤ )
46 45 ffnd ⊢ ( 𝜑 → 𝐵 Fn ( 1 ... 𝑀 ) )
47 1 2 3 4 5 7 metakunt19 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) ∧ { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } ) )
48 47 simpld ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) )
49 48 simp3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
50 47 simprd ⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } )
51 1 2 3 metakunt24 ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ ∧ ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) ∧ ( 1 ... 𝑀 ) = ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) ) )
52 51 simp1d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ )
53 49 50 52 fnund ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) Fn ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
54 51 simp2d ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
55 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
56 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ∈ ℕ )
57 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ≤ 𝑀 )
58 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) → 𝑦 ∈ ( 1 ... 𝑀 ) )
59 55 56 57 4 5 7 58 metakunt23 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑦 ) = ( ( ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑦 ) )
60 46 53 54 59 eqfnfv2d2 ⊢ ( 𝜑 → 𝐵 = ( ( ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) ∪ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) )
61 51 simp3d ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) )
62 6 8 10 13 14 15 17 18 19 60 54 61 metakunt17 ⊢ ( 𝜑 → 𝐵 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )