Proof of Theorem metakunt11
Step | Hyp | Ref
| Expression |
1 | | metakunt11.4 |
. . 3
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
3 | | eqeq1 2763 |
. . . . 5
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 = 𝐼 ↔ (𝐶‘𝑋) = 𝐼)) |
4 | | breq1 5028 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 < 𝐼 ↔ (𝐶‘𝑋) < 𝐼)) |
5 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → 𝑥 = (𝐶‘𝑋)) |
6 | | oveq1 7150 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 − 1) = ((𝐶‘𝑋) − 1)) |
7 | 4, 5, 6 | ifbieq12d 4441 |
. . . . 5
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
8 | 3, 7 | ifbieq2d 4439 |
. . . 4
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
9 | 8 | adantl 486 |
. . 3
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
10 | | metakunt11.5 |
. . . . . . . 8
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
12 | | eqeq1 2763 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (𝑦 = 𝑀 ↔ 𝑋 = 𝑀)) |
13 | | breq1 5028 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → (𝑦 < 𝐼 ↔ 𝑋 < 𝐼)) |
14 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → 𝑦 = 𝑋) |
15 | | oveq1 7150 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
16 | 13, 14, 15 | ifbieq12d 4441 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
17 | 12, 16 | ifbieq2d 4439 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
18 | 17 | adantl 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
19 | | metakunt11.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
20 | | elfznn 12970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℕ) |
22 | 21 | nnred 11674 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
23 | 22 | adantr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ ℝ) |
24 | | metakunt11.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 ∈ ℕ) |
25 | 24 | nnred 11674 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ ℝ) |
26 | 25 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℝ) |
27 | | metakunt11.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℕ) |
28 | 27 | nnred 11674 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) |
29 | 28 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℝ) |
30 | | simpr 489 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝐼) |
31 | | metakunt11.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
32 | 31 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ≤ 𝑀) |
33 | 23, 26, 29, 30, 32 | ltletrd 10823 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝑀) |
34 | 23, 33 | ltned 10799 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝑀) |
35 | | df-ne 2950 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝑀 ↔ ¬ 𝑋 = 𝑀) |
36 | 34, 35 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝑀) |
37 | | iffalse 4422 |
. . . . . . . . . . 11
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
39 | | iftrue 4419 |
. . . . . . . . . . 11
⊢ (𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
40 | 39 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
41 | 38, 40 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
42 | 41 | adantr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
43 | 18, 42 | eqtrd 2794 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
44 | 19 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
45 | 11, 43, 44, 44 | fvmptd 6759 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘𝑋) = 𝑋) |
46 | | eqeq1 2763 |
. . . . . . 7
⊢ ((𝐶‘𝑋) = 𝑋 → ((𝐶‘𝑋) = 𝐼 ↔ 𝑋 = 𝐼)) |
47 | 46 | ifbid 4436 |
. . . . . 6
⊢ ((𝐶‘𝑋) = 𝑋 → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if(𝑋 = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
48 | 45, 47 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if(𝑋 = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
49 | 23, 30 | ltned 10799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝐼) |
50 | 49 | neneqd 2954 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝐼) |
51 | | iffalse 4422 |
. . . . . . 7
⊢ (¬
𝑋 = 𝐼 → if(𝑋 = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
53 | 45 | eqcomd 2765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 = (𝐶‘𝑋)) |
54 | | breq1 5028 |
. . . . . . . . . 10
⊢ (𝑋 = (𝐶‘𝑋) → (𝑋 < 𝐼 ↔ (𝐶‘𝑋) < 𝐼)) |
55 | | id 22 |
. . . . . . . . . 10
⊢ (𝑋 = (𝐶‘𝑋) → 𝑋 = (𝐶‘𝑋)) |
56 | | oveq1 7150 |
. . . . . . . . . 10
⊢ (𝑋 = (𝐶‘𝑋) → (𝑋 − 1) = ((𝐶‘𝑋) − 1)) |
57 | 54, 55, 56 | ifbieq12d 4441 |
. . . . . . . . 9
⊢ (𝑋 = (𝐶‘𝑋) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
58 | 53, 57 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
59 | 58 | eqcomd 2765 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
60 | 30 | iftrued 4421 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = 𝑋) |
61 | 59, 60 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)) = 𝑋) |
62 | 52, 61 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
63 | 48, 62 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
64 | 63 | adantr 485 |
. . 3
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
65 | 9, 64 | eqtrd 2794 |
. 2
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
66 | 27, 24, 31, 10 | metakunt2 39633 |
. . . 4
⊢ (𝜑 → 𝐶:(1...𝑀)⟶(1...𝑀)) |
67 | 66 | adantr 485 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐶:(1...𝑀)⟶(1...𝑀)) |
68 | 67, 44 | ffvelrnd 6836 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘𝑋) ∈ (1...𝑀)) |
69 | 2, 65, 68, 44 | fvmptd 6759 |
1
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋) |