Metamath Proof Explorer

Theorem metakunt34

Description: D is a permutation. (Contributed by metakunt, 18-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 metakunt34.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt34.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt34.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt34.4 ⊢ 𝐷 = ( 𝑤 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑤 = 𝐼 , 𝑤 , if ( 𝑤 < 𝐼 , ( ( 𝑤 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑤 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑤 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑤 − 𝐼 ) , 1 , 0 ) ) ) ) )
5 eqid ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
6 eqid ⊢ ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) )
7 1 2 3 5 6 metakunt14 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ◡ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) ) )
8 7 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
9 f1ocnv ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → ◡ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
10 8 9 syl ⊢ ( 𝜑 → ◡ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
11 7 simprd ⊢ ( 𝜑 → ◡ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) )
12 eqidd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( 1 ... 𝑀 ) )
13 11 12 12 f1oeq123d ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ) )
14 10 13 mpbid ⊢ ( 𝜑 → ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
15 eqid ⊢ ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) )
16 1 2 3 15 metakunt25 ⊢ ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
17 f1oco ⊢ ( ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ) → ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
18 16 8 17 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
19 f1oco ⊢ ( ( ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ) → ( ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) ∘ ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
20 14 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) ∘ ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
21 1 2 3 5 15 6 4 metakunt33 ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) ∘ ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) ) = 𝐷 )
22 21 12 12 f1oeq123d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝐼 , if ( 𝑧 < 𝐼 , 𝑧 , ( 𝑧 + 1 ) ) ) ) ∘ ( ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝑀 , if ( 𝑦 < 𝐼 , ( 𝑦 + ( 𝑀 − 𝐼 ) ) , ( 𝑦 + ( 1 − 𝐼 ) ) ) ) ) ∘ ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ 𝐷 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ) )
23 20 22 mpbid ⊢ ( 𝜑 → 𝐷 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )