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