| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | metakunt25.1 | . . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 2 |  | metakunt25.2 | . . 3
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 3 |  | metakunt25.3 | . . 3
⊢ (𝜑 → 𝐼 ≤ 𝑀) | 
| 4 |  | eqid 2737 | . . 3
⊢ (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) | 
| 5 | 1, 2, 3, 4 | metakunt15 42220 | . 2
⊢ (𝜑 → (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))):(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | 
| 6 |  | eqid 2737 | . . 3
⊢ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) | 
| 7 | 1, 2, 3, 6 | metakunt16 42221 | . 2
⊢ (𝜑 → (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))):(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) | 
| 8 |  | f1osng 6889 | . . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ) →
{〈𝑀, 𝑀〉}:{𝑀}–1-1-onto→{𝑀}) | 
| 9 | 1, 1, 8 | syl2anc 584 | . 2
⊢ (𝜑 → {〈𝑀, 𝑀〉}:{𝑀}–1-1-onto→{𝑀}) | 
| 10 | 1, 2, 3 | metakunt18 42223 | . . . 4
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | 
| 11 | 10 | simpld 494 | . . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) | 
| 12 | 11 | simp1d 1143 | . 2
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) | 
| 13 | 11 | simp2d 1144 | . 2
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) | 
| 14 | 11 | simp3d 1145 | . 2
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 15 | 10 | simprd 495 | . . 3
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)) | 
| 16 | 15 | simp1d 1143 | . 2
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅) | 
| 17 | 15 | simp2d 1144 | . 2
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 18 | 15 | simp3d 1145 | . 2
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅) | 
| 19 |  | eleq1 2829 | . . . . . 6
⊢ (𝑀 = if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) → (𝑀 ∈ ℤ ↔ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ)) | 
| 20 |  | eleq1 2829 | . . . . . 6
⊢ (if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) → (if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ ↔ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ)) | 
| 21 | 1 | nnzd 12640 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 22 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑀 ∈ ℤ) | 
| 23 | 22 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝑀 ∈ ℤ) | 
| 24 |  | eleq1 2829 | . . . . . . 7
⊢ ((𝑥 + (𝑀 − 𝐼)) = if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) → ((𝑥 + (𝑀 − 𝐼)) ∈ ℤ ↔ if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ)) | 
| 25 |  | eleq1 2829 | . . . . . . 7
⊢ ((𝑥 + (1 − 𝐼)) = if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) → ((𝑥 + (1 − 𝐼)) ∈ ℤ ↔ if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ)) | 
| 26 |  | elfzelz 13564 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ) | 
| 27 | 26 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ℤ) | 
| 28 | 27 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝑥 ∈ ℤ) | 
| 29 | 28 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝑥 ∈ ℤ) | 
| 30 | 22 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝑀 ∈ ℤ) | 
| 31 | 2 | nnzd 12640 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝐼 ∈ ℤ) | 
| 33 | 32 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝐼 ∈ ℤ) | 
| 34 | 33 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝐼 ∈ ℤ) | 
| 35 | 30, 34 | zsubcld 12727 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → (𝑀 − 𝐼) ∈ ℤ) | 
| 36 | 29, 35 | zaddcld 12726 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → (𝑥 + (𝑀 − 𝐼)) ∈ ℤ) | 
| 37 | 28 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 𝑥 ∈ ℤ) | 
| 38 |  | 1zzd 12648 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 1 ∈ ℤ) | 
| 39 | 33 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 𝐼 ∈ ℤ) | 
| 40 | 38, 39 | zsubcld 12727 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → (1 − 𝐼) ∈ ℤ) | 
| 41 | 37, 40 | zaddcld 12726 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → (𝑥 + (1 − 𝐼)) ∈ ℤ) | 
| 42 | 24, 25, 36, 41 | ifbothda 4564 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ) | 
| 43 | 19, 20, 23, 42 | ifbothda 4564 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ) | 
| 44 |  | metakunt25.4 | . . . . 5
⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) | 
| 45 | 43, 44 | fmptd 7134 | . . . 4
⊢ (𝜑 → 𝐵:(1...𝑀)⟶ℤ) | 
| 46 | 45 | ffnd 6737 | . . 3
⊢ (𝜑 → 𝐵 Fn (1...𝑀)) | 
| 47 | 1, 2, 3, 44, 4, 6 | metakunt19 42224 | . . . . . 6
⊢ (𝜑 → (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) Fn (1...(𝐼 − 1)) ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) Fn (𝐼...(𝑀 − 1)) ∧ ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) | 
| 48 | 47 | simpld 494 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) Fn (1...(𝐼 − 1)) ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) Fn (𝐼...(𝑀 − 1)) ∧ ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) | 
| 49 | 48 | simp3d 1145 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 50 | 47 | simprd 495 | . . . 4
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) | 
| 51 | 1, 2, 3 | metakunt24 42229 | . . . . 5
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) | 
| 52 | 51 | simp1d 1143 | . . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) | 
| 53 | 49, 50, 52 | fnund 6683 | . . 3
⊢ (𝜑 → (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉}) Fn (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) | 
| 54 | 51 | simp2d 1144 | . . 3
⊢ (𝜑 → (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) | 
| 55 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) | 
| 56 | 2 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝐼 ∈ ℕ) | 
| 57 | 3 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝐼 ≤ 𝑀) | 
| 58 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝑦 ∈ (1...𝑀)) | 
| 59 | 55, 56, 57, 44, 4, 6, 58 | metakunt23 42228 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → (𝐵‘𝑦) = ((((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉})‘𝑦)) | 
| 60 | 46, 53, 54, 59 | eqfnfv2d2 41982 | . 2
⊢ (𝜑 → 𝐵 = (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉})) | 
| 61 | 51 | simp3d 1145 | . 2
⊢ (𝜑 → (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})) | 
| 62 | 5, 7, 9, 12, 13, 14, 16, 17, 18, 60, 54, 61 | metakunt17 42222 | 1
⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) |