Proof of Theorem fseq1p1m1
Step | Hyp | Ref
| Expression |
1 | | simpr1 1067 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐹:(1...𝑁)⟶𝐴) |
2 | | nn0p1nn 11332 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝑁 + 1) ∈ ℕ) |
4 | | simpr2 1068 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐵 ∈ 𝐴) |
5 | | fseq1p1m1.1 |
. . . . . . . . 9
⊢ 𝐻 = {〈(𝑁 + 1), 𝐵〉} |
6 | | fsng 6404 |
. . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℕ ∧ 𝐵 ∈ 𝐴) → (𝐻:{(𝑁 + 1)}⟶{𝐵} ↔ 𝐻 = {〈(𝑁 + 1), 𝐵〉})) |
7 | 5, 6 | mpbiri 248 |
. . . . . . . 8
⊢ (((𝑁 + 1) ∈ ℕ ∧ 𝐵 ∈ 𝐴) → 𝐻:{(𝑁 + 1)}⟶{𝐵}) |
8 | 3, 4, 7 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐻:{(𝑁 + 1)}⟶{𝐵}) |
9 | 4 | snssd 4340 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → {𝐵} ⊆ 𝐴) |
10 | 8, 9 | fssd 6057 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐻:{(𝑁 + 1)}⟶𝐴) |
11 | | fzp1disj 12399 |
. . . . . . 7
⊢
((1...𝑁) ∩
{(𝑁 + 1)}) =
∅ |
12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
13 | | fun2 6067 |
. . . . . 6
⊢ (((𝐹:(1...𝑁)⟶𝐴 ∧ 𝐻:{(𝑁 + 1)}⟶𝐴) ∧ ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝐹 ∪ 𝐻):((1...𝑁) ∪ {(𝑁 + 1)})⟶𝐴) |
14 | 1, 10, 12, 13 | syl21anc 1325 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐹 ∪ 𝐻):((1...𝑁) ∪ {(𝑁 + 1)})⟶𝐴) |
15 | | 1z 11407 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
16 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝑁 ∈
ℕ0) |
17 | | nn0uz 11722 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
18 | | 1m1e0 11089 |
. . . . . . . . . . 11
⊢ (1
− 1) = 0 |
19 | 18 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
20 | 17, 19 | eqtr4i 2647 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
21 | 16, 20 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝑁 ∈ (ℤ≥‘(1
− 1))) |
22 | | fzsuc2 12398 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) |
23 | 15, 21, 22 | sylancr 695 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) |
24 | 23 | eqcomd 2628 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((1...𝑁) ∪ {(𝑁 + 1)}) = (1...(𝑁 + 1))) |
25 | 24 | feq2d 6031 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐹 ∪ 𝐻):((1...𝑁) ∪ {(𝑁 + 1)})⟶𝐴 ↔ (𝐹 ∪ 𝐻):(1...(𝑁 + 1))⟶𝐴)) |
26 | 14, 25 | mpbid 222 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐹 ∪ 𝐻):(1...(𝑁 + 1))⟶𝐴) |
27 | | simpr3 1069 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐺 = (𝐹 ∪ 𝐻)) |
28 | 27 | feq1d 6030 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺:(1...(𝑁 + 1))⟶𝐴 ↔ (𝐹 ∪ 𝐻):(1...(𝑁 + 1))⟶𝐴)) |
29 | 26, 28 | mpbird 247 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐺:(1...(𝑁 + 1))⟶𝐴) |
30 | | ovex 6678 |
. . . . . 6
⊢ (𝑁 + 1) ∈ V |
31 | 30 | snid 4208 |
. . . . 5
⊢ (𝑁 + 1) ∈ {(𝑁 + 1)} |
32 | | fvres 6207 |
. . . . 5
⊢ ((𝑁 + 1) ∈ {(𝑁 + 1)} → ((𝐺 ↾ {(𝑁 + 1)})‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1))) |
33 | 31, 32 | ax-mp 5 |
. . . 4
⊢ ((𝐺 ↾ {(𝑁 + 1)})‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1)) |
34 | 27 | reseq1d 5395 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺 ↾ {(𝑁 + 1)}) = ((𝐹 ∪ 𝐻) ↾ {(𝑁 + 1)})) |
35 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐹:(1...𝑁)⟶𝐴 → 𝐹 Fn (1...𝑁)) |
36 | | fnresdisj 6001 |
. . . . . . . . . . 11
⊢ (𝐹 Fn (1...𝑁) → (((1...𝑁) ∩ {(𝑁 + 1)}) = ∅ ↔ (𝐹 ↾ {(𝑁 + 1)}) = ∅)) |
37 | 1, 35, 36 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (((1...𝑁) ∩ {(𝑁 + 1)}) = ∅ ↔ (𝐹 ↾ {(𝑁 + 1)}) = ∅)) |
38 | 12, 37 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐹 ↾ {(𝑁 + 1)}) = ∅) |
39 | 38 | uneq1d 3766 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐹 ↾ {(𝑁 + 1)}) ∪ (𝐻 ↾ {(𝑁 + 1)})) = (∅ ∪ (𝐻 ↾ {(𝑁 + 1)}))) |
40 | | resundir 5411 |
. . . . . . . 8
⊢ ((𝐹 ∪ 𝐻) ↾ {(𝑁 + 1)}) = ((𝐹 ↾ {(𝑁 + 1)}) ∪ (𝐻 ↾ {(𝑁 + 1)})) |
41 | | uncom 3757 |
. . . . . . . . 9
⊢ (∅
∪ (𝐻 ↾ {(𝑁 + 1)})) = ((𝐻 ↾ {(𝑁 + 1)}) ∪ ∅) |
42 | | un0 3967 |
. . . . . . . . 9
⊢ ((𝐻 ↾ {(𝑁 + 1)}) ∪ ∅) = (𝐻 ↾ {(𝑁 + 1)}) |
43 | 41, 42 | eqtr2i 2645 |
. . . . . . . 8
⊢ (𝐻 ↾ {(𝑁 + 1)}) = (∅ ∪ (𝐻 ↾ {(𝑁 + 1)})) |
44 | 39, 40, 43 | 3eqtr4g 2681 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐹 ∪ 𝐻) ↾ {(𝑁 + 1)}) = (𝐻 ↾ {(𝑁 + 1)})) |
45 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐻:{(𝑁 + 1)}⟶𝐴 → 𝐻 Fn {(𝑁 + 1)}) |
46 | | fnresdm 6000 |
. . . . . . . 8
⊢ (𝐻 Fn {(𝑁 + 1)} → (𝐻 ↾ {(𝑁 + 1)}) = 𝐻) |
47 | 10, 45, 46 | 3syl 18 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐻 ↾ {(𝑁 + 1)}) = 𝐻) |
48 | 34, 44, 47 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺 ↾ {(𝑁 + 1)}) = 𝐻) |
49 | 48 | fveq1d 6193 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐺 ↾ {(𝑁 + 1)})‘(𝑁 + 1)) = (𝐻‘(𝑁 + 1))) |
50 | 5 | fveq1i 6192 |
. . . . . . 7
⊢ (𝐻‘(𝑁 + 1)) = ({〈(𝑁 + 1), 𝐵〉}‘(𝑁 + 1)) |
51 | | fvsng 6447 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ ℕ ∧ 𝐵 ∈ 𝐴) → ({〈(𝑁 + 1), 𝐵〉}‘(𝑁 + 1)) = 𝐵) |
52 | 50, 51 | syl5eq 2668 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ ∧ 𝐵 ∈ 𝐴) → (𝐻‘(𝑁 + 1)) = 𝐵) |
53 | 3, 4, 52 | syl2anc 693 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐻‘(𝑁 + 1)) = 𝐵) |
54 | 49, 53 | eqtrd 2656 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐺 ↾ {(𝑁 + 1)})‘(𝑁 + 1)) = 𝐵) |
55 | 33, 54 | syl5eqr 2670 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺‘(𝑁 + 1)) = 𝐵) |
56 | 27 | reseq1d 5395 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺 ↾ (1...𝑁)) = ((𝐹 ∪ 𝐻) ↾ (1...𝑁))) |
57 | | incom 3805 |
. . . . . . . 8
⊢ ({(𝑁 + 1)} ∩ (1...𝑁)) = ((1...𝑁) ∩ {(𝑁 + 1)}) |
58 | 57, 12 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ({(𝑁 + 1)} ∩ (1...𝑁)) = ∅) |
59 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐻:{(𝑁 + 1)}⟶{𝐵} → 𝐻 Fn {(𝑁 + 1)}) |
60 | | fnresdisj 6001 |
. . . . . . . 8
⊢ (𝐻 Fn {(𝑁 + 1)} → (({(𝑁 + 1)} ∩ (1...𝑁)) = ∅ ↔ (𝐻 ↾ (1...𝑁)) = ∅)) |
61 | 8, 59, 60 | 3syl 18 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (({(𝑁 + 1)} ∩ (1...𝑁)) = ∅ ↔ (𝐻 ↾ (1...𝑁)) = ∅)) |
62 | 58, 61 | mpbid 222 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐻 ↾ (1...𝑁)) = ∅) |
63 | 62 | uneq2d 3767 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐹 ↾ (1...𝑁)) ∪ (𝐻 ↾ (1...𝑁))) = ((𝐹 ↾ (1...𝑁)) ∪ ∅)) |
64 | | resundir 5411 |
. . . . 5
⊢ ((𝐹 ∪ 𝐻) ↾ (1...𝑁)) = ((𝐹 ↾ (1...𝑁)) ∪ (𝐻 ↾ (1...𝑁))) |
65 | | un0 3967 |
. . . . . 6
⊢ ((𝐹 ↾ (1...𝑁)) ∪ ∅) = (𝐹 ↾ (1...𝑁)) |
66 | 65 | eqcomi 2631 |
. . . . 5
⊢ (𝐹 ↾ (1...𝑁)) = ((𝐹 ↾ (1...𝑁)) ∪ ∅) |
67 | 63, 64, 66 | 3eqtr4g 2681 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → ((𝐹 ∪ 𝐻) ↾ (1...𝑁)) = (𝐹 ↾ (1...𝑁))) |
68 | | fnresdm 6000 |
. . . . 5
⊢ (𝐹 Fn (1...𝑁) → (𝐹 ↾ (1...𝑁)) = 𝐹) |
69 | 1, 35, 68 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐹 ↾ (1...𝑁)) = 𝐹) |
70 | 56, 67, 69 | 3eqtrrd 2661 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → 𝐹 = (𝐺 ↾ (1...𝑁))) |
71 | 29, 55, 70 | 3jca 1242 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) → (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) |
72 | | simpr1 1067 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐺:(1...(𝑁 + 1))⟶𝐴) |
73 | | fzssp1 12384 |
. . . . 5
⊢
(1...𝑁) ⊆
(1...(𝑁 +
1)) |
74 | | fssres 6070 |
. . . . 5
⊢ ((𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (1...𝑁) ⊆ (1...(𝑁 + 1))) → (𝐺 ↾ (1...𝑁)):(1...𝑁)⟶𝐴) |
75 | 72, 73, 74 | sylancl 694 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺 ↾ (1...𝑁)):(1...𝑁)⟶𝐴) |
76 | | simpr3 1069 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐹 = (𝐺 ↾ (1...𝑁))) |
77 | 76 | feq1d 6030 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐹:(1...𝑁)⟶𝐴 ↔ (𝐺 ↾ (1...𝑁)):(1...𝑁)⟶𝐴)) |
78 | 75, 77 | mpbird 247 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐹:(1...𝑁)⟶𝐴) |
79 | | simpr2 1068 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺‘(𝑁 + 1)) = 𝐵) |
80 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝑁 + 1) ∈ ℕ) |
81 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
82 | 80, 81 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝑁 + 1) ∈
(ℤ≥‘1)) |
83 | | eluzfz2 12349 |
. . . . . 6
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → (𝑁 + 1) ∈ (1...(𝑁 + 1))) |
84 | 82, 83 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝑁 + 1) ∈ (1...(𝑁 + 1))) |
85 | 72, 84 | ffvelrnd 6360 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺‘(𝑁 + 1)) ∈ 𝐴) |
86 | 79, 85 | eqeltrrd 2702 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐵 ∈ 𝐴) |
87 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐺:(1...(𝑁 + 1))⟶𝐴 → 𝐺 Fn (1...(𝑁 + 1))) |
88 | 72, 87 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐺 Fn (1...(𝑁 + 1))) |
89 | | fnressn 6425 |
. . . . . . . 8
⊢ ((𝐺 Fn (1...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (1...(𝑁 + 1))) → (𝐺 ↾ {(𝑁 + 1)}) = {〈(𝑁 + 1), (𝐺‘(𝑁 + 1))〉}) |
90 | 88, 84, 89 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺 ↾ {(𝑁 + 1)}) = {〈(𝑁 + 1), (𝐺‘(𝑁 + 1))〉}) |
91 | | opeq2 4403 |
. . . . . . . . 9
⊢ ((𝐺‘(𝑁 + 1)) = 𝐵 → 〈(𝑁 + 1), (𝐺‘(𝑁 + 1))〉 = 〈(𝑁 + 1), 𝐵〉) |
92 | 91 | sneqd 4189 |
. . . . . . . 8
⊢ ((𝐺‘(𝑁 + 1)) = 𝐵 → {〈(𝑁 + 1), (𝐺‘(𝑁 + 1))〉} = {〈(𝑁 + 1), 𝐵〉}) |
93 | 79, 92 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → {〈(𝑁 + 1), (𝐺‘(𝑁 + 1))〉} = {〈(𝑁 + 1), 𝐵〉}) |
94 | 90, 93 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺 ↾ {(𝑁 + 1)}) = {〈(𝑁 + 1), 𝐵〉}) |
95 | 94, 5 | syl6reqr 2675 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐻 = (𝐺 ↾ {(𝑁 + 1)})) |
96 | 76, 95 | uneq12d 3768 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐹 ∪ 𝐻) = ((𝐺 ↾ (1...𝑁)) ∪ (𝐺 ↾ {(𝑁 + 1)}))) |
97 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝑁 ∈
ℕ0) |
98 | 97, 20 | syl6eleq 2711 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝑁 ∈ (ℤ≥‘(1
− 1))) |
99 | 15, 98, 22 | sylancr 695 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) |
100 | 99 | reseq2d 5396 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺 ↾ (1...(𝑁 + 1))) = (𝐺 ↾ ((1...𝑁) ∪ {(𝑁 + 1)}))) |
101 | | resundi 5410 |
. . . . 5
⊢ (𝐺 ↾ ((1...𝑁) ∪ {(𝑁 + 1)})) = ((𝐺 ↾ (1...𝑁)) ∪ (𝐺 ↾ {(𝑁 + 1)})) |
102 | 100, 101 | syl6req 2673 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → ((𝐺 ↾ (1...𝑁)) ∪ (𝐺 ↾ {(𝑁 + 1)})) = (𝐺 ↾ (1...(𝑁 + 1)))) |
103 | | fnresdm 6000 |
. . . . 5
⊢ (𝐺 Fn (1...(𝑁 + 1)) → (𝐺 ↾ (1...(𝑁 + 1))) = 𝐺) |
104 | 72, 87, 103 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐺 ↾ (1...(𝑁 + 1))) = 𝐺) |
105 | 96, 102, 104 | 3eqtrrd 2661 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → 𝐺 = (𝐹 ∪ 𝐻)) |
106 | 78, 86, 105 | 3jca 1242 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))) → (𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))) |
107 | 71, 106 | impbida 877 |
1
⊢ (𝑁 ∈ ℕ0
→ ((𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁))))) |