Step | Hyp | Ref
| Expression |
1 | | vdw.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Fin) |
2 | | hashcl 13009 |
. . . . . . 7
⊢ (𝑅 ∈ Fin →
(#‘𝑅) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝑅) ∈
ℕ0) |
4 | 3 | nn0red 11229 |
. . . . 5
⊢ (𝜑 → (#‘𝑅) ∈ ℝ) |
5 | 4 | ltp1d 10833 |
. . . 4
⊢ (𝜑 → (#‘𝑅) < ((#‘𝑅) + 1)) |
6 | | nn0p1nn 11209 |
. . . . . . 7
⊢
((#‘𝑅) ∈
ℕ0 → ((#‘𝑅) + 1) ∈ ℕ) |
7 | 3, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((#‘𝑅) + 1) ∈
ℕ) |
8 | 7 | nnnn0d 11228 |
. . . . 5
⊢ (𝜑 → ((#‘𝑅) + 1) ∈
ℕ0) |
9 | | hashfz1 12996 |
. . . . 5
⊢
(((#‘𝑅) + 1)
∈ ℕ0 → (#‘(1...((#‘𝑅) + 1))) = ((#‘𝑅) + 1)) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝜑 →
(#‘(1...((#‘𝑅)
+ 1))) = ((#‘𝑅) +
1)) |
11 | 5, 10 | breqtrrd 4611 |
. . 3
⊢ (𝜑 → (#‘𝑅) < (#‘(1...((#‘𝑅) + 1)))) |
12 | | fzfi 12633 |
. . . 4
⊢
(1...((#‘𝑅) +
1)) ∈ Fin |
13 | | hashsdom 13031 |
. . . 4
⊢ ((𝑅 ∈ Fin ∧
(1...((#‘𝑅) + 1))
∈ Fin) → ((#‘𝑅) < (#‘(1...((#‘𝑅) + 1))) ↔ 𝑅 ≺ (1...((#‘𝑅) + 1)))) |
14 | 1, 12, 13 | sylancl 693 |
. . 3
⊢ (𝜑 → ((#‘𝑅) <
(#‘(1...((#‘𝑅)
+ 1))) ↔ 𝑅 ≺
(1...((#‘𝑅) +
1)))) |
15 | 11, 14 | mpbid 221 |
. 2
⊢ (𝜑 → 𝑅 ≺ (1...((#‘𝑅) + 1))) |
16 | | vdwlem12.f |
. . . . 5
⊢ (𝜑 → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅) |
17 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
18 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦)) |
19 | 17, 18 | eqeqan12d 2626 |
. . . . . . . 8
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
20 | | eqeq12 2623 |
. . . . . . . 8
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝑧 = 𝑤 ↔ 𝑥 = 𝑦)) |
21 | 19, 20 | imbi12d 333 |
. . . . . . 7
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
22 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
23 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
24 | 22, 23 | eqeqan12d 2626 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))) |
25 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝐹‘𝑦) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)) |
26 | 24, 25 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
27 | | eqeq12 2623 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝑧 = 𝑤 ↔ 𝑦 = 𝑥)) |
28 | | eqcom 2617 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
29 | 27, 28 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝑧 = 𝑤 ↔ 𝑥 = 𝑦)) |
30 | 26, 29 | imbi12d 333 |
. . . . . . 7
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
31 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈
ℕ) |
32 | 31 | nnred 10912 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈
ℝ) |
33 | 32 | ssriv 3572 |
. . . . . . . 8
⊢
(1...((#‘𝑅) +
1)) ⊆ ℝ |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1...((#‘𝑅) + 1)) ⊆
ℝ) |
35 | | biidd 251 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
36 | | simplr3 1098 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ≤ 𝑦) |
37 | | vdwlem12.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 2 MonoAP 𝐹) |
38 | 37 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ¬ 2 MonoAP 𝐹) |
39 | | 3simpa 1051 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦) → (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) |
40 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1))) |
41 | 40, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℕ) |
42 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
43 | | simplrr 797 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1))) |
44 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...((#‘𝑅) + 1)) → 𝑦 ∈
ℕ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℕ) |
46 | | nnsub 10936 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℕ)) |
47 | 41, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℕ)) |
48 | 42, 47 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦 − 𝑥) ∈ ℕ) |
49 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 = (1 +
1) |
50 | 49 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . 18
⊢
(AP‘2) = (AP‘(1 + 1)) |
51 | 50 | oveqi 6562 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(AP‘2)(𝑦 − 𝑥)) = (𝑥(AP‘(1 + 1))(𝑦 − 𝑥)) |
52 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ0 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈
ℕ0) |
54 | | vdwapun 15516 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℕ0 ∧ 𝑥 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ) → (𝑥(AP‘(1 + 1))(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)))) |
55 | 53, 41, 48, 54 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘(1 + 1))(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)))) |
56 | 51, 55 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)))) |
57 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
58 | 16 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅) |
59 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:(1...((#‘𝑅) + 1))⟶𝑅 → 𝐹 Fn (1...((#‘𝑅) + 1))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝐹 Fn (1...((#‘𝑅) + 1))) |
61 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
63 | 40, 57, 62 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑦)})) |
64 | 63 | snssd 4281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → {𝑥} ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
65 | 41 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ) |
66 | 45 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℂ) |
67 | 65, 66 | pncan3d 10274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 + (𝑦 − 𝑥)) = 𝑦) |
68 | 67 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) = (𝑦(AP‘1)(𝑦 − 𝑥))) |
69 | | vdwap1 15519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ) → (𝑦(AP‘1)(𝑦 − 𝑥)) = {𝑦}) |
70 | 45, 48, 69 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦(AP‘1)(𝑦 − 𝑥)) = {𝑦}) |
71 | 68, 70 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) = {𝑦}) |
72 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
73 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑦) = (𝐹‘𝑦)))) |
74 | 60, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑦) = (𝐹‘𝑦)))) |
75 | 43, 72, 74 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑦)})) |
76 | 75 | snssd 4281 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → {𝑦} ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
77 | 71, 76 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
78 | 64, 77 | unssd 3751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥))) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
79 | 56, 78 | eqsstrd 3602 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
80 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑥 → (𝑎(AP‘2)𝑑) = (𝑥(AP‘2)𝑑)) |
81 | 80 | sseq1d 3595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → ((𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}))) |
82 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑦 − 𝑥) → (𝑥(AP‘2)𝑑) = (𝑥(AP‘2)(𝑦 − 𝑥))) |
83 | 82 | sseq1d 3595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑦 − 𝑥) → ((𝑥(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}))) |
84 | 81, 83 | rspc2ev 3295 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ ∧ (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
85 | 41, 48, 79, 84 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)})) |
86 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑦) ∈ V |
87 | | sneq 4135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝐹‘𝑦) → {𝑐} = {(𝐹‘𝑦)}) |
88 | 87 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝐹‘𝑦) → (◡𝐹 “ {𝑐}) = (◡𝐹 “ {(𝐹‘𝑦)})) |
89 | 88 | sseq2d 3596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐹‘𝑦) → ((𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}))) |
90 | 89 | 2rexbidv 3039 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐹‘𝑦) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}))) |
91 | 86, 90 | spcev 3273 |
. . . . . . . . . . . . . 14
⊢
(∃𝑎 ∈
ℕ ∃𝑑 ∈
ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝑦)}) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
92 | 85, 91 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
93 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...((#‘𝑅) +
1)) ∈ V |
94 | | 2nn0 11186 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈
ℕ0) |
96 | 93, 95, 58 | vdwmc 15520 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (2 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
97 | 92, 96 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹) |
98 | 39, 97 | sylanl2 681 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹) |
99 | 98 | expr 641 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 < 𝑦 → 2 MonoAP 𝐹)) |
100 | 38, 99 | mtod 188 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ¬ 𝑥 < 𝑦) |
101 | | simplr1 1096 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1))) |
102 | 101, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ ℝ) |
103 | | simplr2 1097 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1))) |
104 | 33, 103 | sseldi 3566 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ ℝ) |
105 | 102, 104 | eqleltd 10060 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ ¬ 𝑥 < 𝑦))) |
106 | 36, 100, 105 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦) |
107 | 106 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
108 | 21, 30, 34, 35, 107 | wlogle 10440 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
109 | 108 | ralrimivva 2954 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
110 | | dff13 6416 |
. . . . 5
⊢ (𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅 ↔ (𝐹:(1...((#‘𝑅) + 1))⟶𝑅 ∧ ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
111 | 16, 109, 110 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅) |
112 | | f1domg 7861 |
. . . 4
⊢ (𝑅 ∈ Fin → (𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅 → (1...((#‘𝑅) + 1)) ≼ 𝑅)) |
113 | 1, 111, 112 | sylc 63 |
. . 3
⊢ (𝜑 → (1...((#‘𝑅) + 1)) ≼ 𝑅) |
114 | | domnsym 7971 |
. . 3
⊢
((1...((#‘𝑅) +
1)) ≼ 𝑅 → ¬
𝑅 ≺
(1...((#‘𝑅) +
1))) |
115 | 113, 114 | syl 17 |
. 2
⊢ (𝜑 → ¬ 𝑅 ≺ (1...((#‘𝑅) + 1))) |
116 | 15, 115 | pm2.65i 184 |
1
⊢ ¬
𝜑 |