| Step | Hyp | Ref
| Expression |
| 1 | | fz1ssfz0 13663 |
. . 3
⊢
(1...𝐾) ⊆
(0...𝐾) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (1...𝐾) ⊆ (0...𝐾)) |
| 3 | | f1resfz0f1d.2 |
. 2
⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉) |
| 4 | | f1resfz0f1d.3 |
. 2
⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉) |
| 5 | | f1resfz0f1d.1 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 6 | | 0elfz 13664 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ 0 ∈ (0...𝐾)) |
| 7 | | snssi 4808 |
. . . . . 6
⊢ (0 ∈
(0...𝐾) → {0} ⊆
(0...𝐾)) |
| 8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ (𝜑 → {0} ⊆ (0...𝐾)) |
| 9 | 3, 8 | fssresd 6775 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ {0}):{0}⟶𝑉) |
| 10 | | eqidd 2738 |
. . . . 5
⊢ (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘0) → 0
= 0) |
| 11 | | 0nn0 12541 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
| 12 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑥 = 0 → (((𝐹 ↾ {0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) ↔ ((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘𝑦))) |
| 13 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑥 = 𝑦 ↔ 0 = 𝑦)) |
| 14 | 12, 13 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 0 → ((((𝐹 ↾ {0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘𝑦) → 0 = 𝑦))) |
| 15 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 0 → ((𝐹 ↾ {0})‘𝑦) = ((𝐹 ↾ {0})‘0)) |
| 16 | 15 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = 0 → (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘𝑦) ↔ ((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘0))) |
| 17 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑦 = 0 → (0 = 𝑦 ↔ 0 = 0)) |
| 18 | 16, 17 | imbi12d 344 |
. . . . . . 7
⊢ (𝑦 = 0 → ((((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘𝑦) → 0 = 𝑦) ↔ (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘0) → 0 =
0))) |
| 19 | 14, 18 | 2ralsng 4678 |
. . . . . 6
⊢ ((0
∈ ℕ0 ∧ 0 ∈ ℕ0) →
(∀𝑥 ∈
{0}∀𝑦 ∈ {0}
(((𝐹 ↾
{0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘0) → 0 =
0))) |
| 20 | 11, 11, 19 | mp2an 692 |
. . . . 5
⊢
(∀𝑥 ∈
{0}∀𝑦 ∈ {0}
(((𝐹 ↾
{0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐹 ↾ {0})‘0) = ((𝐹 ↾ {0})‘0) → 0 =
0)) |
| 21 | 10, 20 | mpbir 231 |
. . . 4
⊢
∀𝑥 ∈
{0}∀𝑦 ∈ {0}
(((𝐹 ↾
{0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) → 𝑥 = 𝑦) |
| 22 | | dff13 7275 |
. . . 4
⊢ ((𝐹 ↾ {0}):{0}–1-1→𝑉 ↔ ((𝐹 ↾ {0}):{0}⟶𝑉 ∧ ∀𝑥 ∈ {0}∀𝑦 ∈ {0} (((𝐹 ↾ {0})‘𝑥) = ((𝐹 ↾ {0})‘𝑦) → 𝑥 = 𝑦))) |
| 23 | 9, 21, 22 | sylanblrc 590 |
. . 3
⊢ (𝜑 → (𝐹 ↾ {0}):{0}–1-1→𝑉) |
| 24 | | uncom 4158 |
. . . . . . . 8
⊢
((1...𝐾) ∪ {0})
= ({0} ∪ (1...𝐾)) |
| 25 | | fz0sn0fz1 13685 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (0...𝐾) = ({0} ∪
(1...𝐾))) |
| 26 | 5, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0...𝐾) = ({0} ∪ (1...𝐾))) |
| 27 | 24, 26 | eqtr4id 2796 |
. . . . . . 7
⊢ (𝜑 → ((1...𝐾) ∪ {0}) = (0...𝐾)) |
| 28 | | 0nelfz1 13583 |
. . . . . . . . . 10
⊢ 0 ∉
(1...𝐾) |
| 29 | 28 | neli 3048 |
. . . . . . . . 9
⊢ ¬ 0
∈ (1...𝐾) |
| 30 | | disjsn 4711 |
. . . . . . . . 9
⊢
(((1...𝐾) ∩ {0})
= ∅ ↔ ¬ 0 ∈ (1...𝐾)) |
| 31 | 29, 30 | mpbir 231 |
. . . . . . . 8
⊢
((1...𝐾) ∩ {0})
= ∅ |
| 32 | | uneqdifeq 4493 |
. . . . . . . 8
⊢
(((1...𝐾) ⊆
(0...𝐾) ∧ ((1...𝐾) ∩ {0}) = ∅) →
(((1...𝐾) ∪ {0}) =
(0...𝐾) ↔ ((0...𝐾) ∖ (1...𝐾)) = {0})) |
| 33 | 1, 31, 32 | mp2an 692 |
. . . . . . 7
⊢
(((1...𝐾) ∪ {0})
= (0...𝐾) ↔
((0...𝐾) ∖ (1...𝐾)) = {0}) |
| 34 | 27, 33 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ((0...𝐾) ∖ (1...𝐾)) = {0}) |
| 35 | 34 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → {0} = ((0...𝐾) ∖ (1...𝐾))) |
| 36 | 35 | reseq2d 5997 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ {0}) = (𝐹 ↾ ((0...𝐾) ∖ (1...𝐾)))) |
| 37 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → 𝑉 = 𝑉) |
| 38 | 36, 35, 37 | f1eq123d 6840 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ {0}):{0}–1-1→𝑉 ↔ (𝐹 ↾ ((0...𝐾) ∖ (1...𝐾))):((0...𝐾) ∖ (1...𝐾))–1-1→𝑉)) |
| 39 | 23, 38 | mpbid 232 |
. 2
⊢ (𝜑 → (𝐹 ↾ ((0...𝐾) ∖ (1...𝐾))):((0...𝐾) ∖ (1...𝐾))–1-1→𝑉) |
| 40 | 35 | imaeq2d 6078 |
. . . 4
⊢ (𝜑 → (𝐹 “ {0}) = (𝐹 “ ((0...𝐾) ∖ (1...𝐾)))) |
| 41 | 40 | ineq2d 4220 |
. . 3
⊢ (𝜑 → ((𝐹 “ (1...𝐾)) ∩ (𝐹 “ {0})) = ((𝐹 “ (1...𝐾)) ∩ (𝐹 “ ((0...𝐾) ∖ (1...𝐾))))) |
| 42 | | incom 4209 |
. . . 4
⊢ ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ((𝐹 “ (1...𝐾)) ∩ (𝐹 “ {0})) |
| 43 | | f1resfz0f1d.4 |
. . . 4
⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅) |
| 44 | 42, 43 | eqtr3id 2791 |
. . 3
⊢ (𝜑 → ((𝐹 “ (1...𝐾)) ∩ (𝐹 “ {0})) = ∅) |
| 45 | 41, 44 | eqtr3d 2779 |
. 2
⊢ (𝜑 → ((𝐹 “ (1...𝐾)) ∩ (𝐹 “ ((0...𝐾) ∖ (1...𝐾)))) = ∅) |
| 46 | 2, 3, 4, 39, 45 | f1resrcmplf1d 35101 |
1
⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉) |