Step | Hyp | Ref
| Expression |
1 | | poimirlem3.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾)) |
2 | | ffn 6206 |
. . . . . . . . . . . . . . 15
⊢ (𝑇:(1...𝑀)⟶(0..^𝐾) → 𝑇 Fn (1...𝑀)) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 Fn (1...𝑀)) |
4 | 3 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀)) |
5 | | 1ex 10227 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
6 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
V → ((𝑈 “
(1...𝑗)) × {1}) Fn
(𝑈 “ (1...𝑗))) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) |
8 | | c0ex 10226 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
9 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → ((𝑈 “
((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀)) |
11 | 7, 10 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) |
12 | | poimirlem3.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀)) |
13 | | dff1o3 6304 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun ◡𝑈)) |
14 | 13 | simprbi 483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun ◡𝑈) |
15 | | imain 6135 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
16 | 12, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
17 | | elfznn0 12626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
18 | 17 | nn0red 11544 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ) |
19 | 18 | ltp1d 11146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1)) |
20 | | fzdisj 12561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅) |
22 | 21 | imaeq2d 5624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅)) |
23 | | ima0 5639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 “ ∅) =
∅ |
24 | 22, 23 | syl6eq 2810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅) |
25 | 16, 24 | sylan9req 2815 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) |
26 | | fnun 6158 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 “
(1...𝑗)) × {1}) Fn
(𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
27 | 11, 25, 26 | sylancr 698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
28 | | imaundi 5703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) |
29 | | nn0p1nn 11524 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
30 | | nnuz 11916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
31 | 29, 30 | syl6eleq 2849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
(ℤ≥‘1)) |
32 | 17, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
33 | | elfzuz3 12532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ≥‘𝑗)) |
34 | | fzsplit2 12559 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ (ℤ≥‘𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
35 | 32, 33, 34 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
36 | 35 | eqcomd 2766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀)) |
37 | 36 | imaeq2d 5624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀))) |
38 | | f1ofo 6305 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀)) |
39 | | foima 6281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀)) |
40 | 12, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀)) |
41 | 37, 40 | sylan9eqr 2816 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀)) |
42 | 28, 41 | syl5eqr 2808 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀)) |
43 | 42 | fneq2d 6143 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))) |
44 | 27, 43 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)) |
45 | | ovexd 6843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V) |
46 | | inidm 3965 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ∩
(1...𝑀)) = (1...𝑀) |
47 | | eqidd 2761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
48 | | eqidd 2761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
49 | 4, 44, 45, 45, 46, 47, 48 | offval 7069 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))) |
50 | | poimirlem4.2 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
51 | | nn0p1nn 11524 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
53 | 52 | nnzd 11673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
54 | | uzid 11894 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈ ℤ →
(𝑀 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
55 | | peano2uz 11934 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
57 | | poimirlem4.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < 𝑁) |
58 | 50 | nn0zd 11672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
59 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℕ) |
60 | 59 | nnzd 11673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
61 | | zltp1le 11619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
62 | | peano2z 11610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
63 | | eluz 11893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁)) |
64 | 62, 63 | sylan 489 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁)) |
65 | 61, 64 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
66 | 58, 60, 65 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
67 | 57, 66 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
68 | | fzsplit2 12559 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
69 | 56, 67, 68 | syl2anc 696 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
70 | | fzsn 12576 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈ ℤ →
((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)}) |
71 | 53, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)}) |
72 | 71 | uneq1d 3909 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁))) |
73 | 69, 72 | eqtrd 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁))) |
74 | 73 | xpeq1d 5295 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0})) |
75 | | xpundir 5329 |
. . . . . . . . . . . . . . 15
⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
76 | | ovex 6841 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 + 1) ∈ V |
77 | 76, 8 | xpsn 6570 |
. . . . . . . . . . . . . . . 16
⊢ ({(𝑀 + 1)} × {0}) =
{〈(𝑀 + 1),
0〉} |
78 | 77 | uneq1i 3906 |
. . . . . . . . . . . . . . 15
⊢ (({(𝑀 + 1)} × {0}) ∪
((((𝑀 + 1) + 1)...𝑁) × {0})) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
79 | 75, 78 | eqtri 2782 |
. . . . . . . . . . . . . 14
⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
80 | 74, 79 | syl6eq 2810 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
81 | 80 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
82 | 49, 81 | uneq12d 3911 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))) |
83 | | unass 3913 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
84 | 82, 83 | syl6eqr 2812 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
85 | 50 | nn0red 11544 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℝ) |
86 | 85 | ltp1d 11146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
87 | 52 | nnred 11227 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
88 | 85, 87 | ltnled 10376 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
89 | 86, 88 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
90 | | elfzle2 12538 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀) |
91 | 89, 90 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀)) |
92 | | disjsn 4390 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑀) ∩
{(𝑀 + 1)}) = ∅ ↔
¬ (𝑀 + 1) ∈
(1...𝑀)) |
93 | 91, 92 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) |
94 | | eqid 2760 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈(𝑀 + 1),
0〉} = {〈(𝑀 + 1),
0〉} |
95 | 76, 8 | fsn 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈(𝑀 + 1),
0〉}:{(𝑀 +
1)}⟶{0} ↔ {〈(𝑀 + 1), 0〉} = {〈(𝑀 + 1), 0〉}) |
96 | 94, 95 | mpbir 221 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈(𝑀 + 1),
0〉}:{(𝑀 +
1)}⟶{0} |
97 | | fun 6227 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {〈(𝑀 + 1), 0〉}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
98 | 96, 97 | mpanl2 719 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
99 | 1, 93, 98 | syl2anc 696 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
100 | | 1z 11599 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
101 | | nn0uz 11915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
ℕ0 = (ℤ≥‘0) |
102 | | 1m1e0 11281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 1) = 0 |
103 | 102 | fveq2i 6355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
104 | 101, 103 | eqtr4i 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
105 | 50, 104 | syl6eleq 2849 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(1
− 1))) |
106 | | fzsuc2 12591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ (ℤ≥‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
107 | 100, 105,
106 | sylancr 698 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
108 | 107 | eqcomd 2766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1))) |
109 | | poimirlem4.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℕ) |
110 | | lbfzo0 12702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
(0..^𝐾) ↔ 𝐾 ∈
ℕ) |
111 | 109, 110 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ (0..^𝐾)) |
112 | 111 | snssd 4485 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {0} ⊆ (0..^𝐾)) |
113 | | ssequn2 3929 |
. . . . . . . . . . . . . . . . . 18
⊢ ({0}
⊆ (0..^𝐾) ↔
((0..^𝐾) ∪ {0}) =
(0..^𝐾)) |
114 | 112, 113 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾)) |
115 | 108, 114 | feq23d 6201 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾))) |
116 | 99, 115 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
117 | | ffn 6206 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
119 | 118 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
120 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
V → (((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗))) |
121 | 5, 120 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) |
122 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → (((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
123 | 8, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) |
124 | 121, 123 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∧ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
125 | 76, 76 | f1osn 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)} |
126 | | f1oun 6317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ {〈(𝑀 + 1), (𝑀 + 1)〉}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)}) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
127 | 125, 126 | mpanl2 719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
128 | 12, 93, 93, 127 | syl12anc 1475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
129 | | dff1o3 6304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun ◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}))) |
130 | 129 | simprbi 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun ◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})) |
131 | | imain 6135 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
132 | 128, 130,
131 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
133 | | fzdisj 12561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅) |
134 | 19, 133 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅) |
135 | 134 | imaeq2d 5624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “
∅)) |
136 | | ima0 5639 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ∅) =
∅ |
137 | 135, 136 | syl6eq 2810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) |
138 | 132, 137 | sylan9req 2815 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) |
139 | | fnun 6158 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∧ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) ∧ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
140 | 124, 138,
139 | sylancr 698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
141 | | f1ofo 6305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
142 | | foima 6281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
143 | 128, 141,
142 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
144 | 107 | imaeq2d 5624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)}))) |
145 | 143, 144,
107 | 3eqtr4d 2804 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1))) |
146 | | peano2uz 11934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝑀 + 1) ∈
(ℤ≥‘𝑗)) |
147 | 33, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈
(ℤ≥‘𝑗)) |
148 | | fzsplit2 12559 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ (𝑀 + 1) ∈
(ℤ≥‘𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) |
149 | 32, 147, 148 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) |
150 | 149 | imaeq2d 5624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))) |
151 | 145, 150 | sylan9req 2815 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))) |
152 | | imaundi 5703 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
153 | 151, 152 | syl6eq 2810 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
154 | 153 | fneq2d 6143 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1)) ↔ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))))) |
155 | 140, 154 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1))) |
156 | | ovexd 6843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V) |
157 | | inidm 3965 |
. . . . . . . . . . . . 13
⊢
((1...(𝑀 + 1)) ∩
(1...(𝑀 + 1))) =
(1...(𝑀 +
1)) |
158 | | eqidd 2761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛)) |
159 | | eqidd 2761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) |
160 | 119, 155,
156, 156, 157, 158, 159 | offval 7069 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = (𝑛 ∈ (1...(𝑀 + 1)) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)))) |
161 | | ovexd 6843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ V) |
162 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ V) |
163 | 108 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1))) |
164 | | fveq2 6352 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1))) |
165 | 76 | snid 4353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 + 1) ∈ {(𝑀 + 1)} |
166 | 76, 8 | fnsn 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈(𝑀 + 1),
0〉} Fn {(𝑀 +
1)} |
167 | | fvun2 6432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 Fn (1...𝑀) ∧ {〈(𝑀 + 1), 0〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
168 | 166, 167 | mp3an2 1561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
169 | 165, 168 | mpanr2 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
170 | 3, 93, 169 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
171 | 76, 8 | fvsn 6610 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈(𝑀 + 1),
0〉}‘(𝑀 + 1)) =
0 |
172 | 170, 171 | syl6eq 2810 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0) |
173 | 164, 172 | sylan9eqr 2816 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = 0) |
174 | 173 | adantlr 753 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = 0) |
175 | | fveq2 6352 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1))) |
176 | | imadmrn 5634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)}) |
177 | 76, 76 | xpsn 6570 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑀 + 1)} × {(𝑀 + 1)}) = {〈(𝑀 + 1), (𝑀 + 1)〉} |
178 | 177 | imaeq1i 5621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) |
179 | | dmxpid 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ dom
({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)} |
180 | 179 | imaeq2i 5622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “ dom
({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
181 | 178, 180 | eqtri 2782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
182 | | rnxpid 5725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)} |
183 | 176, 181,
182 | 3eqtr3ri 2791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑀 + 1)} = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
184 | | eluzp1p1 11905 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝑀 + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
185 | | eluzfz2 12542 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1))) |
186 | 33, 184, 185 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1))) |
187 | 186 | snssd 4485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1))) |
188 | | imass2 5659 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (0...𝑀) → ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
190 | 183, 189 | syl5eqss 3790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
191 | | ssel 3738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({(𝑀 + 1)} ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → ((𝑀 + 1) ∈ {(𝑀 + 1)} → (𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
192 | 190, 165,
191 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
193 | | elun2 3924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
194 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
195 | | imaundir 5704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
196 | 194, 195 | syl6eleqr 2850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
197 | 196 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
198 | | fvun2 6432 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∧ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) ∧ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅ ∧ (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1))) |
199 | 121, 123,
198 | mp3an12 1563 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅ ∧ (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1))) |
200 | 138, 197,
199 | syl2anc 696 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1))) |
201 | 8 | fvconst2 6633 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
202 | 196, 201 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
203 | 202 | adantl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
204 | 200, 203 | eqtrd 2794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0) |
205 | 175, 204 | sylan9eqr 2816 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0) |
206 | 174, 205 | oveq12d 6831 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0)) |
207 | | 00id 10403 |
. . . . . . . . . . . . . 14
⊢ (0 + 0) =
0 |
208 | 206, 207 | syl6eq 2810 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0) |
209 | 161, 162,
163, 208 | fmptapd 6601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) = (𝑛 ∈ (1...(𝑀 + 1)) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)))) |
210 | 3, 93 | jca 555 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) |
211 | | fvun1 6431 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 Fn (1...𝑀) ∧ {〈(𝑀 + 1), 0〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
212 | 166, 211 | mp3an2 1561 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
213 | 212 | anassrs 683 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
214 | 210, 213 | sylan 489 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
215 | 214 | adantlr 753 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
216 | | fvres 6368 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) |
217 | 216 | eqcomd 2766 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛)) |
218 | | resundir 5569 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) ∪ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) |
219 | | relxp 5283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Rel
((𝑈 “ (1...𝑗)) × {1}) |
220 | | dmxpss 5723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗)) |
221 | | imassrn 5635 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ (1...𝑗)) ⊆ ran 𝑈 |
222 | 220, 221 | sstri 3753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆ ran
𝑈 |
223 | | f1of 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀)) |
224 | | frn 6214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀)) |
225 | 12, 223, 224 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑀)) |
226 | 222, 225 | syl5ss 3755 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) |
227 | | relssres 5595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Rel
((𝑈 “ (1...𝑗)) × {1}) ∧ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆
(1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
228 | 219, 226,
227 | sylancr 698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
229 | 228 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
230 | | imassrn 5635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} |
231 | 76 | rnsnop 5776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} = {(𝑀 + 1)} |
232 | 230, 231 | sseqtri 3778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ {(𝑀 + 1)} |
233 | | ssrin 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ {(𝑀 + 1)} → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))) |
234 | 232, 233 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)) |
235 | | incom 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)}) |
236 | 235, 93 | syl5eq 2806 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅) |
237 | 234, 236 | syl5sseq 3794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅) |
238 | | ss0 4117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ →
(({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅) |
239 | 237, 238 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅) |
240 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
V → (({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) × {1}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) |
241 | | fnresdisj 6162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) × {1}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)) |
242 | 5, 240, 241 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) = ∅ ↔
((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾
(1...𝑀)) =
∅) |
243 | 239, 242 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅) |
244 | 243 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅) |
245 | 229, 244 | uneq12d 3911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪
∅)) |
246 | | imaundir 5704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) |
247 | 246 | xpeq1i 5292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) × {1}) |
248 | | xpundir 5329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) |
249 | 247, 248 | eqtri 2782 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) |
250 | 249 | reseq1i 5547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) |
251 | | resundir 5569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) |
252 | 250, 251 | eqtr2i 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) |
253 | | un0 4110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1}) |
254 | 245, 252,
253 | 3eqtr3g 2817 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
255 | | f1odm 6302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀)) |
256 | 12, 255 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → dom 𝑈 = (1...𝑀)) |
257 | 256 | ineq2d 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) |
258 | 257 | reseq2d 5551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))) |
259 | | f1orel 6301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈) |
260 | | resindm 5602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Rel
𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
261 | 12, 259, 260 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
262 | 258, 261 | eqtr3d 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
263 | 35 | ineq2d 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))) |
264 | | fzssp1 12577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) |
265 | | sseqin2 3960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)) |
266 | 264, 265 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀) |
267 | 266 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)) |
268 | | incom 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) |
269 | 268, 134 | syl5eq 2806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅) |
270 | 267, 269 | uneq12d 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅)) |
271 | | uncom 3900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀))) |
272 | | indi 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀))) |
273 | 271, 272 | eqtr4i 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
274 | | un0 4110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀) |
275 | 270, 273,
274 | 3eqtr3g 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀)) |
276 | 263, 275 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀)) |
277 | 276 | reseq2d 5551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
278 | 262, 277 | sylan9req 2815 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
279 | 278 | rneqd 5508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
280 | | df-ima 5279 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) |
281 | | df-ima 5279 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)) |
282 | 279, 280,
281 | 3eqtr4g 2819 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀))) |
283 | 282 | xpeq1d 5295 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
284 | 283 | reseq1d 5550 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀))) |
285 | | relxp 5283 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ Rel
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) |
286 | | dmxpss 5723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ dom
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀)) |
287 | | imassrn 5635 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈 |
288 | 286, 287 | sstri 3753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈 |
289 | 288, 225 | syl5ss 3755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) |
290 | | relssres 5595 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Rel
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
291 | 285, 289,
290 | sylancr 698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
292 | 291 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
293 | 284, 292 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
294 | | imassrn 5635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} |
295 | 294, 231 | sseqtri 3778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} |
296 | | ssrin 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))) |
297 | 295, 296 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)) |
298 | 297, 236 | syl5sseq 3794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅) |
299 | | ss0 4117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ →
(({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅) |
300 | 298, 299 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅) |
301 | | fnconstg 6254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
V → (({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
302 | | fnresdisj 6162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)) |
303 | 8, 301, 302 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔
((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
304 | 300, 303 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
305 | 304 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
306 | 293, 305 | uneq12d 3911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪
∅)) |
307 | 195 | xpeq1i 5292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) |
308 | | xpundir 5329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) |
309 | 307, 308 | eqtri 2782 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) |
310 | 309 | reseq1i 5547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) |
311 | | resundir 5569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) |
312 | 310, 311 | eqtr2i 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) |
313 | | un0 4110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) |
314 | 306, 312,
313 | 3eqtr3g 2817 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
315 | 254, 314 | uneq12d 3911 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) ∪ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) |
316 | 218, 315 | syl5eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) |
317 | 316 | fveq1d 6354 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
318 | 217, 317 | sylan9eqr 2816 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
319 | 215, 318 | oveq12d 6831 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) |
320 | 319 | mpteq2dva 4896 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))) |
321 | 320 | uneq1d 3909 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉})) |
322 | 160, 209,
321 | 3eqtr2d 2800 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉})) |
323 | 322 | uneq1d 3909 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
324 | 84, 323 | eqtr4d 2797 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
325 | 324 | csbeq1d 3681 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵) |
326 | 325 | eqeq2d 2770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ 𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
327 | 326 | rexbidva 3187 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
328 | 327 | ralbidv 3124 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
329 | 328 | biimpd 219 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
330 | | f1ofn 6299 |
. . . . . . . 8
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀)) |
331 | 12, 330 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 Fn (1...𝑀)) |
332 | 76, 76 | fnsn 6107 |
. . . . . . . . 9
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉} Fn {(𝑀 + 1)} |
333 | | fvun2 6432 |
. . . . . . . . 9
⊢ ((𝑈 Fn (1...𝑀) ∧ {〈(𝑀 + 1), (𝑀 + 1)〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
334 | 332, 333 | mp3an2 1561 |
. . . . . . . 8
⊢ ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
335 | 165, 334 | mpanr2 722 |
. . . . . . 7
⊢ ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
336 | 331, 93, 335 | syl2anc 696 |
. . . . . 6
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
337 | 76, 76 | fvsn 6610 |
. . . . . 6
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉}‘(𝑀 + 1)) = (𝑀 + 1) |
338 | 336, 337 | syl6eq 2810 |
. . . . 5
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1)) |
339 | 172, 338 | jca 555 |
. . . 4
⊢ (𝜑 → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))) |
340 | 329, 339 | jctird 568 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))))) |
341 | | 3anass 1081 |
. . 3
⊢
((∀𝑖 ∈
(0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1)))) |
342 | 340, 341 | syl6ibr 242 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1)))) |
343 | 1, 96 | jctir 562 |
. . . . . 6
⊢ (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {〈(𝑀 + 1), 0〉}:{(𝑀 + 1)}⟶{0})) |
344 | 343, 93, 97 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
345 | 344, 115 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
346 | | ovex 6841 |
. . . . 5
⊢
(0..^𝐾) ∈
V |
347 | | ovex 6841 |
. . . . 5
⊢
(1...(𝑀 + 1)) ∈
V |
348 | 346, 347 | elmap 8052 |
. . . 4
⊢ ((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∈ ((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ↔
(𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
349 | 345, 348 | sylibr 224 |
. . 3
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∈ ((0..^𝐾) ↑𝑚
(1...(𝑀 +
1)))) |
350 | | ovex 6841 |
. . . . . . . 8
⊢
(1...𝑀) ∈
V |
351 | | f1oexrnex 7280 |
. . . . . . . 8
⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V) |
352 | 12, 350, 351 | sylancl 697 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ V) |
353 | | snex 5057 |
. . . . . . 7
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉} ∈
V |
354 | | unexg 7124 |
. . . . . . 7
⊢ ((𝑈 ∈ V ∧ {〈(𝑀 + 1), (𝑀 + 1)〉} ∈ V) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ V) |
355 | 352, 353,
354 | sylancl 697 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ V) |
356 | | f1oeq1 6288 |
. . . . . . 7
⊢ (𝑓 = (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)))) |
357 | 356 | elabg 3491 |
. . . . . 6
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ V → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)))) |
358 | 355, 357 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)))) |
359 | | f1oeq23 6291 |
. . . . . 6
⊢
(((1...(𝑀 + 1)) =
((1...𝑀) ∪ {(𝑀 + 1)}) ∧ (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))) |
360 | 107, 107,
359 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))) |
361 | 358, 360 | bitrd 268 |
. . . 4
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))) |
362 | 128, 361 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) |
363 | | opelxpi 5305 |
. . 3
⊢ (((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∈ ((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ∧ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) → 〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ×
{𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})) |
364 | 349, 362,
363 | syl2anc 696 |
. 2
⊢ (𝜑 → 〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ×
{𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})) |
365 | 342, 364 | jctild 567 |
1
⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ×
{𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))))) |