Step | Hyp | Ref
| Expression |
1 | | elfznelfzo 12439 |
. . . . . . 7
⊢ ((𝑦 ∈ (0...𝐾) ∧ ¬ 𝑦 ∈ (1..^𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾)) |
2 | | fvinim0ffz 12449 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |
3 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾))) |
4 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 =
𝑦 → (𝐹‘0) = (𝐹‘𝑦)) |
5 | 4 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 0 → (𝐹‘0) = (𝐹‘𝑦)) |
6 | 5 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 0 → ((𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
7 | 6 | notbid 307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 0 → (¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
8 | 7 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 0 → (¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) → ¬ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
9 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:(0...𝐾)⟶𝑉 → 𝐹 Fn (0...𝐾)) |
10 | | 1eluzge0 11608 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
(ℤ≥‘0) |
11 | | fzoss1 12364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
(ℤ≥‘0) → (1..^𝐾) ⊆ (0..^𝐾)) |
12 | 10, 11 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (1..^𝐾) ⊆
(0..^𝐾)) |
13 | | fzossfz 12357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0..^𝐾) ⊆
(0...𝐾) |
14 | 12, 13 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐾 ∈ ℕ0
→ (1..^𝐾) ⊆
(0...𝐾)) |
15 | | fvelimab 6163 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn (0...𝐾) ∧ (1..^𝐾) ⊆ (0...𝐾)) → ((𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)) ↔ ∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦))) |
16 | 9, 14, 15 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → ((𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)) ↔ ∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦))) |
17 | 16 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (¬
(𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ ∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦))) |
18 | | ralnex 2975 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑧 ∈
(1..^𝐾) ¬ (𝐹‘𝑧) = (𝐹‘𝑦) ↔ ¬ ∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦)) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
21 | 20 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
22 | 21 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ (1..^𝐾) ∧ ∀𝑧 ∈ (1..^𝐾) ¬ (𝐹‘𝑧) = (𝐹‘𝑦)) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) |
23 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
(𝐹‘𝑥) = (𝐹‘𝑦) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
24 | 23 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
(𝐹‘𝑥) = (𝐹‘𝑦) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
25 | 24 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
(𝐹‘𝑥) = (𝐹‘𝑦) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
26 | 22, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ (1..^𝐾) ∧ ∀𝑧 ∈ (1..^𝐾) ¬ (𝐹‘𝑧) = (𝐹‘𝑦)) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
27 | 26 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑧 ∈
(1..^𝐾) ¬ (𝐹‘𝑧) = (𝐹‘𝑦) → (𝑥 ∈ (1..^𝐾) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
28 | 27 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑧 ∈
(1..^𝐾) ¬ (𝐹‘𝑧) = (𝐹‘𝑦) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
29 | 18, 28 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
30 | 29 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (¬
∃𝑧 ∈ (1..^𝐾)(𝐹‘𝑧) = (𝐹‘𝑦) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
31 | 17, 30 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (¬
(𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
32 | 31 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
33 | 8, 32 | syl6com 36 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) → (𝑦 = 0 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
34 | 3, 33 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) → (𝑦 = 0 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → (𝑦 = 0 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
36 | 35 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
37 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾))) |
38 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐾 = 𝑦 → (𝐹‘𝐾) = (𝐹‘𝑦)) |
39 | 38 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝐾 → (𝐹‘𝐾) = (𝐹‘𝑦)) |
40 | 39 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝐾 → ((𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
41 | 40 | notbid 307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝐾 → (¬ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
42 | 41 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝐾 → (¬ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)) → ¬ (𝐹‘𝑦) ∈ (𝐹 “ (1..^𝐾)))) |
43 | 42, 32 | syl6com 36 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)) → (𝑦 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
44 | 37, 43 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾)) → (𝑦 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → (𝑦 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐾 → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
47 | 36, 46 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 0 ∨ 𝑦 = 𝐾) → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
48 | 47 | com13 86 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
49 | 2, 48 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → (𝑥 ∈ (0...𝐾) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
50 | 49 | com14 94 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0...𝐾) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
51 | 50 | com12 32 |
. . . . . . . . . 10
⊢ (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → (𝑥 ∈ (0...𝐾) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝑥 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
52 | 51 | com15 99 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1..^𝐾) → (𝑥 ∈ (0...𝐾) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
53 | | elfznelfzo 12439 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0...𝐾) ∧ ¬ 𝑥 ∈ (1..^𝐾)) → (𝑥 = 0 ∨ 𝑥 = 𝐾)) |
54 | | eqtr3 2631 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦) |
55 | | 2a1 28 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
56 | 55 | 2a1d 26 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
58 | 5 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 0) → (𝐹‘0) = (𝐹‘𝑦)) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 = 𝑥 → (𝐹‘𝐾) = (𝐹‘𝑥)) |
60 | 59 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐾 → (𝐹‘𝐾) = (𝐹‘𝑥)) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 0) → (𝐹‘𝐾) = (𝐹‘𝑥)) |
62 | 58, 61 | neeq12d 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 0) → ((𝐹‘0) ≠ (𝐹‘𝐾) ↔ (𝐹‘𝑦) ≠ (𝐹‘𝑥))) |
63 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ≠ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) |
64 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) = (𝐹‘𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) → 𝑥 = 𝑦)) |
65 | 64 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) → 𝑥 = 𝑦)) |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑦) = (𝐹‘𝑥) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
67 | 63, 66 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑦) ≠ (𝐹‘𝑥) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
68 | 62, 67 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 0) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
69 | 68 | 2a1d 26 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 0) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
70 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 =
𝑥 → (𝐹‘0) = (𝐹‘𝑥)) |
71 | 70 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝐹‘0) = (𝐹‘𝑥)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝐾) → (𝐹‘0) = (𝐹‘𝑥)) |
73 | 39 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝐾) → (𝐹‘𝐾) = (𝐹‘𝑦)) |
74 | 72, 73 | neeq12d 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
75 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) |
76 | 75, 23 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ≠ (𝐹‘𝑦) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
77 | 74, 76 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
78 | 77 | 2a1d 26 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
79 | | eqtr3 2631 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑦) |
80 | 79, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐾 ∧ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
81 | 57, 69, 78, 80 | ccase 984 |
. . . . . . . . . . . 12
⊢ (((𝑥 = 0 ∨ 𝑥 = 𝐾) ∧ (𝑦 = 0 ∨ 𝑦 = 𝐾)) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
82 | 81 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑥 = 0 ∨ 𝑥 = 𝐾) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
83 | 53, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0...𝐾) ∧ ¬ 𝑥 ∈ (1..^𝐾)) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
84 | 83 | expcom 450 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ (1..^𝐾) → (𝑥 ∈ (0...𝐾) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
85 | 52, 84 | pm2.61i 175 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...𝐾) → ((𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
86 | 85 | com12 32 |
. . . . . . 7
⊢ ((𝑦 = 0 ∨ 𝑦 = 𝐾) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
87 | 1, 86 | syl 17 |
. . . . . 6
⊢ ((𝑦 ∈ (0...𝐾) ∧ ¬ 𝑦 ∈ (1..^𝐾)) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
88 | 87 | ex 449 |
. . . . 5
⊢ (𝑦 ∈ (0...𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → (𝑥 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
89 | 88 | com23 84 |
. . . 4
⊢ (𝑦 ∈ (0...𝐾) → (𝑥 ∈ (0...𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))))) |
90 | 89 | impcom 445 |
. . 3
⊢ ((𝑥 ∈ (0...𝐾) ∧ 𝑦 ∈ (0...𝐾)) → (¬ 𝑦 ∈ (1..^𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
91 | 90 | com12 32 |
. 2
⊢ (¬
𝑦 ∈ (1..^𝐾) → ((𝑥 ∈ (0...𝐾) ∧ 𝑦 ∈ (0...𝐾)) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
92 | 91 | com25 97 |
1
⊢ (¬
𝑦 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑥 ∈ (0...𝐾) ∧ 𝑦 ∈ (0...𝐾)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |