Step | Hyp | Ref
| Expression |
1 | | poimirlem3.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾)) |
2 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑇:(1...𝑀)⟶(0..^𝐾) → 𝑇 Fn (1...𝑀)) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 Fn (1...𝑀)) |
4 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑇 Fn (1...𝑀)) |
5 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
6 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
V → ((𝑈 “
(1...𝑗)) × {1}) Fn
(𝑈 “ (1...𝑗))) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) |
8 | | c0ex 9913 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
9 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 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 6056 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑈:(1...𝑀)–onto→(1...𝑀) ∧ Fun ◡𝑈)) |
14 | 13 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Fun ◡𝑈) |
15 | | imain 5888 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
16 | 12, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
17 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
18 | 17 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ) |
19 | 18 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 < (𝑗 + 1)) |
20 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑀)) = ∅) |
22 | 21 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = (𝑈 “ ∅)) |
23 | | ima0 5400 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 “ ∅) =
∅ |
24 | 22, 23 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑀))) = ∅) |
25 | 16, 24 | sylan9req 2665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) |
26 | | fnun 5911 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 “
(1...𝑗)) × {1}) Fn
(𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑀))) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑀))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
27 | 11, 25, 26 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀)))) |
28 | | imaundi 5464 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) |
29 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
30 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
31 | 29, 30 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
(ℤ≥‘1)) |
32 | 17, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
33 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ (ℤ≥‘𝑗)) |
34 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ (ℤ≥‘𝑗)) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
35 | 32, 33, 34 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (1...𝑀) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
36 | 35 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)) = (1...𝑀)) |
37 | 36 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (𝑈 “ (1...𝑀))) |
38 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)–onto→(1...𝑀)) |
39 | | foima 6033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑀)–onto→(1...𝑀) → (𝑈 “ (1...𝑀)) = (1...𝑀)) |
40 | 12, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 “ (1...𝑀)) = (1...𝑀)) |
41 | 37, 40 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = (1...𝑀)) |
42 | 28, 41 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) = (1...𝑀)) |
43 | 42 | fneq2d 5896 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑀))) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀))) |
44 | 27, 43 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) Fn (1...𝑀)) |
45 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) ∈
V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...𝑀) ∈ V) |
47 | | inidm 3784 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ∩
(1...𝑀)) = (1...𝑀) |
48 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
49 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
50 | 4, 44, 46, 46, 47, 48, 49 | offval 6802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))) |
51 | | poimirlem4.2 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
52 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
54 | 53 | nnzd 11357 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
55 | | uzid 11578 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈ ℤ →
(𝑀 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
56 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑀 + 1)) → ((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
58 | | poimirlem4.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < 𝑁) |
59 | 51 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
60 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℕ) |
61 | 60 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
62 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
63 | | peano2z 11295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
64 | | eluz 11577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁)) |
65 | 63, 64 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ (𝑀 + 1) ≤ 𝑁)) |
66 | 62, 65 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
67 | 59, 61, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
68 | 58, 67 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
69 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 + 1) + 1) ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
70 | 57, 68, 69 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
71 | | fzsn 12254 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ∈ ℤ →
((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)}) |
72 | 54, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1)...(𝑀 + 1)) = {(𝑀 + 1)}) |
73 | 72 | uneq1d 3728 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑀 + 1)...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁))) |
74 | 70, 73 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1)...𝑁) = ({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁))) |
75 | 74 | xpeq1d 5062 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0})) |
76 | | xpundir 5095 |
. . . . . . . . . . . . . . 15
⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = (({(𝑀 + 1)} × {0}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
77 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 + 1) ∈ V |
78 | 77, 8 | xpsn 6313 |
. . . . . . . . . . . . . . . 16
⊢ ({(𝑀 + 1)} × {0}) =
{〈(𝑀 + 1),
0〉} |
79 | 78 | uneq1i 3725 |
. . . . . . . . . . . . . . 15
⊢ (({(𝑀 + 1)} × {0}) ∪
((((𝑀 + 1) + 1)...𝑁) × {0})) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
80 | 76, 79 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ (({(𝑀 + 1)} ∪ (((𝑀 + 1) + 1)...𝑁)) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) |
81 | 75, 80 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑀 + 1)...𝑁) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀 + 1)...𝑁) × {0}) = ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
83 | 50, 82 | uneq12d 3730 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})))) |
84 | | unass 3732 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ ({〈(𝑀 + 1), 0〉} ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
85 | 83, 84 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
86 | 51 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℝ) |
87 | 86 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
88 | 53 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
89 | 86, 88 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
90 | 87, 89 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
91 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ (1...𝑀) → (𝑀 + 1) ≤ 𝑀) |
92 | 90, 91 | nsyl 134 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝑀 + 1) ∈ (1...𝑀)) |
93 | | disjsn 4192 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑀) ∩
{(𝑀 + 1)}) = ∅ ↔
¬ (𝑀 + 1) ∈
(1...𝑀)) |
94 | 92, 93 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) |
95 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈(𝑀 + 1),
0〉} = {〈(𝑀 + 1),
0〉} |
96 | 77, 8 | fsn 6308 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈(𝑀 + 1),
0〉}:{(𝑀 +
1)}⟶{0} ↔ {〈(𝑀 + 1), 0〉} = {〈(𝑀 + 1), 0〉}) |
97 | 95, 96 | mpbir 220 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈(𝑀 + 1),
0〉}:{(𝑀 +
1)}⟶{0} |
98 | | fun 5979 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {〈(𝑀 + 1), 0〉}:{(𝑀 + 1)}⟶{0}) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
99 | 97, 98 | mpanl2 713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇:(1...𝑀)⟶(0..^𝐾) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
100 | 1, 94, 99 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
101 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
102 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
ℕ0 = (ℤ≥‘0) |
103 | | 1m1e0 10966 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 1) = 0 |
104 | 103 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
105 | 102, 104 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
106 | 51, 105 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(1
− 1))) |
107 | | fzsuc2 12268 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ (ℤ≥‘(1 − 1))) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
108 | 101, 106,
107 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
109 | 108 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1))) |
110 | | poimirlem4.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℕ) |
111 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
(0..^𝐾) ↔ 𝐾 ∈
ℕ) |
112 | 110, 111 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ (0..^𝐾)) |
113 | 112 | snssd 4281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {0} ⊆ (0..^𝐾)) |
114 | | ssequn2 3748 |
. . . . . . . . . . . . . . . . . 18
⊢ ({0}
⊆ (0..^𝐾) ↔
((0..^𝐾) ∪ {0}) =
(0..^𝐾)) |
115 | 113, 114 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0..^𝐾) ∪ {0}) = (0..^𝐾)) |
116 | 109, 115 | feq23d 5953 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0}) ↔ (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾))) |
117 | 100, 116 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
118 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) Fn (1...(𝑀 + 1))) |
121 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
V → (((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗))) |
122 | 5, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) |
123 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → (((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
124 | 8, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) |
125 | 122, 124 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∧ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
126 | 77, 77 | f1osn 6088 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉}:{(𝑀 + 1)}–1-1-onto→{(𝑀 + 1)} |
127 | | f1oun 6069 |
. . . . . . . . . . . . . . . . . . 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)})) |
128 | 126, 127 | mpanl2 713 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
129 | 12, 94, 94, 128 | syl12anc 1316 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
130 | | dff1o3 6056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) ↔ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) ∧ Fun ◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}))) |
131 | 130 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → Fun ◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})) |
132 | | imain 5888 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡(𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
133 | 129, 131,
132 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
134 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅) |
135 | 19, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) = ∅) |
136 | 135 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “
∅)) |
137 | | ima0 5400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ∅) =
∅ |
138 | 136, 137 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) |
139 | 133, 138 | sylan9req 2665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∩ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) = ∅) |
140 | | fnun 5911 |
. . . . . . . . . . . . . . 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))))) |
141 | 125, 139,
140 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
142 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)})) |
143 | | foima 6033 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–onto→((1...𝑀) ∪ {(𝑀 + 1)}) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
144 | 129, 142,
143 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)})) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
145 | 108 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑀) ∪ {(𝑀 + 1)}))) |
146 | 144, 145,
108 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = (1...(𝑀 + 1))) |
147 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝑀 + 1) ∈
(ℤ≥‘𝑗)) |
148 | 33, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈
(ℤ≥‘𝑗)) |
149 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ (𝑀 + 1) ∈
(ℤ≥‘𝑗)) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) |
150 | 32, 148, 149 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → (1...(𝑀 + 1)) = ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) |
151 | 150 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...(𝑀 + 1))) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))) |
152 | 146, 151 | sylan9req 2665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1))))) |
153 | | imaundi 5464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((1...𝑗) ∪ ((𝑗 + 1)...(𝑀 + 1)))) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
154 | 152, 153 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) = (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) ∪ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))))) |
155 | 154 | fneq2d 5896 |
. . . . . . . . . . . . . 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)))))) |
156 | 141, 155 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) Fn (1...(𝑀 + 1))) |
157 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...(𝑀 + 1)) ∈
V |
158 | 157 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1...(𝑀 + 1)) ∈ V) |
159 | | inidm 3784 |
. . . . . . . . . . . . 13
⊢
((1...(𝑀 + 1)) ∩
(1...(𝑀 + 1))) =
(1...(𝑀 +
1)) |
160 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛)) |
161 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...(𝑀 + 1))) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) |
162 | 120, 156,
158, 158, 159, 160, 161 | offval 6802 |
. . . . . . . . . . . 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}))‘𝑛)))) |
163 | 77 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ V) |
164 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ V) |
165 | 109 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((1...𝑀) ∪ {(𝑀 + 1)}) = (1...(𝑀 + 1))) |
166 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑀 + 1) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1))) |
167 | 77 | snid 4155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 + 1) ∈ {(𝑀 + 1)} |
168 | 77, 8 | fnsn 5860 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈(𝑀 + 1),
0〉} Fn {(𝑀 +
1)} |
169 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 Fn (1...𝑀) ∧ {〈(𝑀 + 1), 0〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
170 | 168, 169 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
171 | 167, 170 | mpanr2 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
172 | 3, 94, 171 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), 0〉}‘(𝑀 + 1))) |
173 | 77, 8 | fvsn 6351 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈(𝑀 + 1),
0〉}‘(𝑀 + 1)) =
0 |
174 | 172, 173 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0) |
175 | 166, 174 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = 0) |
176 | 175 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = 0) |
177 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑀 + 1) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1))) |
178 | | imadmrn 5395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ran ({(𝑀 + 1)} × {(𝑀 + 1)}) |
179 | 77, 77 | xpsn 6313 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑀 + 1)} × {(𝑀 + 1)}) = {〈(𝑀 + 1), (𝑀 + 1)〉} |
180 | 179 | imaeq1i 5382 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) |
181 | | dmxpid 5266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ dom
({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)} |
182 | 181 | imaeq2i 5383 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “ dom
({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
183 | 180, 182 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({(𝑀 + 1)} × {(𝑀 + 1)}) “ dom ({(𝑀 + 1)} × {(𝑀 + 1)})) = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
184 | | rnxpid 5486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
({(𝑀 + 1)} × {(𝑀 + 1)}) = {(𝑀 + 1)} |
185 | 178, 183,
184 | 3eqtr3ri 2641 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑀 + 1)} = ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) |
186 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝑀 + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
187 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑗 + 1)) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1))) |
188 | 33, 186, 187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑗 + 1)...(𝑀 + 1))) |
189 | 188 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1))) |
190 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({(𝑀 + 1)} ⊆ ((𝑗 + 1)...(𝑀 + 1)) → ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (0...𝑀) → ({〈(𝑀 + 1), (𝑀 + 1)〉} “ {(𝑀 + 1)}) ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
192 | 185, 191 | syl5eqss 3612 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ (0...𝑀) → {(𝑀 + 1)} ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
193 | | ssel 3562 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({(𝑀 + 1)} ⊆ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → ((𝑀 + 1) ∈ {(𝑀 + 1)} → (𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
194 | 192, 167,
193 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
195 | | elun2 3743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 + 1) ∈ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))))) |
197 | | imaundir 5465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) = ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
198 | 196, 197 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
199 | 198 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1)))) |
200 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . 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))) |
201 | 122, 124,
200 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . 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))) |
202 | 139, 199,
201 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1))) |
203 | 8 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
204 | 198, 203 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
205 | 204 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})‘(𝑀 + 1)) = 0) |
206 | 202, 205 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘(𝑀 + 1)) = 0) |
207 | 177, 206 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = 0) |
208 | 176, 207 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = (0 + 0)) |
209 | | 00id 10090 |
. . . . . . . . . . . . . 14
⊢ (0 + 0) =
0 |
210 | 208, 209 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 = (𝑀 + 1)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = 0) |
211 | 163, 164,
165, 210 | fmptapd 6342 |
. . . . . . . . . . . 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}))‘𝑛)))) |
212 | 3, 94 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅)) |
213 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 Fn (1...𝑀) ∧ {〈(𝑀 + 1), 0〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
214 | 168, 213 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ 𝑛 ∈ (1...𝑀))) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
215 | 214 | anassrs 678 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
216 | 212, 215 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
217 | 216 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) = (𝑇‘𝑛)) |
218 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑀) → ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) |
219 | 218 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑀) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛)) |
220 | | resundir 5331 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑈 ∪
{〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) ∪ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) |
221 | | relxp 5150 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Rel
((𝑈 “ (1...𝑗)) × {1}) |
222 | | dmxpss 5484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆ (𝑈 “ (1...𝑗)) |
223 | | imassrn 5396 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ (1...𝑗)) ⊆ ran 𝑈 |
224 | 222, 223 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆ ran
𝑈 |
225 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈:(1...𝑀)⟶(1...𝑀)) |
226 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈:(1...𝑀)⟶(1...𝑀) → ran 𝑈 ⊆ (1...𝑀)) |
227 | 12, 225, 226 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑀)) |
228 | 224, 227 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom ((𝑈 “ (1...𝑗)) × {1}) ⊆ (1...𝑀)) |
229 | | relssres 5357 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Rel
((𝑈 “ (1...𝑗)) × {1}) ∧ dom
((𝑈 “ (1...𝑗)) × {1}) ⊆
(1...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
230 | 221, 228,
229 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
231 | 230 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
232 | | imassrn 5396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} |
233 | 77 | rnsnop 5534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} = {(𝑀 + 1)} |
234 | 232, 233 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ {(𝑀 + 1)} |
235 | | ssrin 3800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ⊆ {(𝑀 + 1)} → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))) |
236 | 234, 235 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)) |
237 | | incom 3767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑀 + 1)} ∩ (1...𝑀)) = ((1...𝑀) ∩ {(𝑀 + 1)}) |
238 | 237, 94 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ({(𝑀 + 1)} ∩ (1...𝑀)) = ∅) |
239 | 236, 238 | syl5sseq 3616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) ⊆ ∅) |
240 | | ss0 3926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) ⊆ ∅ →
(({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅) |
242 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
V → (({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) × {1}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) |
243 | | fnresdisj 5915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) × {1}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) ∩ (1...𝑀)) = ∅ ↔ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅)) |
244 | 5, 242, 243 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
(1...𝑗)) ∩ (1...𝑀)) = ∅ ↔
((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾
(1...𝑀)) =
∅) |
245 | 241, 244 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅) |
246 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀)) = ∅) |
247 | 231, 246 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪
∅)) |
248 | | imaundir 5465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) = ((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) |
249 | 248 | xpeq1i 5059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) × {1}) |
250 | | xpundir 5095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 “ (1...𝑗)) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗))) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) |
251 | 249, 250 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) = (((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) |
252 | 251 | reseq1i 5313 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) |
253 | | resundir 5331 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...𝑗)) × {1}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1})) ↾ (1...𝑀)) = ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) |
254 | 252, 253 | eqtr2i 2633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑗)) × {1}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ (1...𝑗)) × {1}) ↾ (1...𝑀))) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) |
255 | | un0 3919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑈 “ (1...𝑗)) × {1}) ∪ ∅) = ((𝑈 “ (1...𝑗)) × {1}) |
256 | 247, 254,
255 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) = ((𝑈 “ (1...𝑗)) × {1})) |
257 | | f1odm 6054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → dom 𝑈 = (1...𝑀)) |
258 | 12, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → dom 𝑈 = (1...𝑀)) |
259 | 258 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈) = (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) |
260 | 259 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)))) |
261 | | f1orel 6053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → Rel 𝑈) |
262 | | resindm 5364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Rel
𝑈 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
263 | 12, 261, 262 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ dom 𝑈)) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
264 | 260, 263 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1)))) |
265 | 35 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀)))) |
266 | | fzssp1 12255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) |
267 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑗 + 1)...𝑀) ⊆ ((𝑗 + 1)...(𝑀 + 1)) ↔ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)) |
268 | 266, 267 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀) |
269 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) = ((𝑗 + 1)...𝑀)) |
270 | | incom 3767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ((1...𝑗) ∩ ((𝑗 + 1)...(𝑀 + 1))) |
271 | 270, 135 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) = ∅) |
272 | 269, 271 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ (0...𝑀) → ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...𝑀) ∪ ∅)) |
273 | | uncom 3719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀))) |
274 | | indi 3832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀))) |
275 | 273, 274 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑗 + 1)...(𝑀 + 1)) ∩ ((𝑗 + 1)...𝑀)) ∪ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑗))) = (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) |
276 | | un0 3919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑗 + 1)...𝑀) ∪ ∅) = ((𝑗 + 1)...𝑀) |
277 | 272, 275,
276 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ ((1...𝑗) ∪ ((𝑗 + 1)...𝑀))) = ((𝑗 + 1)...𝑀)) |
278 | 265, 277 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑀) → (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀)) = ((𝑗 + 1)...𝑀)) |
279 | 278 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑀) → (𝑈 ↾ (((𝑗 + 1)...(𝑀 + 1)) ∩ (1...𝑀))) = (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
280 | 264, 279 | sylan9req 2665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
281 | 280 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀))) |
282 | | df-ima 5051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = ran (𝑈 ↾ ((𝑗 + 1)...(𝑀 + 1))) |
283 | | df-ima 5051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) = ran (𝑈 ↾ ((𝑗 + 1)...𝑀)) |
284 | 281, 282,
283 | 3eqtr4g 2669 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) = (𝑈 “ ((𝑗 + 1)...𝑀))) |
285 | 284 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
286 | 285 | reseq1d 5316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀))) |
287 | | relxp 5150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ Rel
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) |
288 | | dmxpss 5484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ dom
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (𝑈 “ ((𝑗 + 1)...𝑀)) |
289 | | imassrn 5396 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑈 “ ((𝑗 + 1)...𝑀)) ⊆ ran 𝑈 |
290 | 288, 289 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ ran 𝑈 |
291 | 290, 227 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) |
292 | | relssres 5357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Rel
((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∧ dom ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ⊆ (1...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
293 | 287, 291,
292 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
294 | 293 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
295 | 286, 294 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
296 | | imassrn 5396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ ran
{〈(𝑀 + 1), (𝑀 + 1)〉} |
297 | 296, 233 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} |
298 | | ssrin 3800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ⊆ {(𝑀 + 1)} → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀))) |
299 | 297, 298 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ({(𝑀 + 1)} ∩ (1...𝑀)) |
300 | 299, 238 | syl5sseq 3616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅) |
301 | | ss0 3926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) ⊆ ∅ →
(({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅) |
302 | 300, 301 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅) |
303 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
V → (({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) |
304 | | fnresdisj 5915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) × {0}) Fn
({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅)) |
305 | 8, 303, 304 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((({〈(𝑀 + 1),
(𝑀 + 1)〉} “
((𝑗 + 1)...(𝑀 + 1))) ∩ (1...𝑀)) = ∅ ↔
((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
306 | 302, 305 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
307 | 306 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ∅) |
308 | 295, 307 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪
∅)) |
309 | 197 | xpeq1i 5059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) |
310 | | xpundir 5095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) ∪ ({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1)))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) |
311 | 309, 310 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) = (((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) |
312 | 311 | reseq1i 5313 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) |
313 | | resundir 5331 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ∪ (({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) |
314 | 312, 313 | eqtr2i 2633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) ∪ ((({〈(𝑀 + 1), (𝑀 + 1)〉} “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) |
315 | | un0 3919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) ∪ ∅) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}) |
316 | 308, 314,
315 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀)) = ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0})) |
317 | 256, 316 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ↾
(1...𝑀)) ∪ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}) ↾ (1...𝑀))) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) |
318 | 220, 317 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀)) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) |
319 | 318 | fveq1d 6105 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0})) ↾ (1...𝑀))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
320 | 219, 319 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)) |
321 | 217, 320 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑛 ∈ (1...𝑀)) → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛)) = ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) |
322 | 321 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛)))) |
323 | 322 | uneq1d 3728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑛 ∈ (1...𝑀) ↦ (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘𝑛) + (((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉}) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉})) |
324 | 162, 211,
323 | 3eqtr2d 2650 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) = ((𝑛 ∈ (1...𝑀) ↦ ((𝑇‘𝑛) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))‘𝑛))) ∪ {〈(𝑀 + 1), 0〉})) |
325 | 324 | uneq1d 3728 |
. . . . . . . . . 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}))) |
326 | 85, 325 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) = (((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0}))) |
327 | 326 | csbeq1d 3506 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵) |
328 | 327 | eqeq2d 2620 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ 𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
329 | 328 | rexbidva 3031 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ↔ ∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘𝑓
+ ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵)) |
330 | 329 | ralbidv 2969 |
. . . . 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})) / 𝑝⦌𝐵)) |
331 | 330 | biimpd 218 |
. . . 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})) / 𝑝⦌𝐵)) |
332 | | f1ofn 6051 |
. . . . . . . 8
⊢ (𝑈:(1...𝑀)–1-1-onto→(1...𝑀) → 𝑈 Fn (1...𝑀)) |
333 | 12, 332 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 Fn (1...𝑀)) |
334 | 77, 77 | fnsn 5860 |
. . . . . . . . 9
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉} Fn {(𝑀 + 1)} |
335 | | fvun2 6180 |
. . . . . . . . 9
⊢ ((𝑈 Fn (1...𝑀) ∧ {〈(𝑀 + 1), (𝑀 + 1)〉} Fn {(𝑀 + 1)} ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
336 | 334, 335 | mp3an2 1404 |
. . . . . . . 8
⊢ ((𝑈 Fn (1...𝑀) ∧ (((1...𝑀) ∩ {(𝑀 + 1)}) = ∅ ∧ (𝑀 + 1) ∈ {(𝑀 + 1)})) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
337 | 167, 336 | mpanr2 716 |
. . . . . . 7
⊢ ((𝑈 Fn (1...𝑀) ∧ ((1...𝑀) ∩ {(𝑀 + 1)}) = ∅) → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
338 | 333, 94, 337 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = ({〈(𝑀 + 1), (𝑀 + 1)〉}‘(𝑀 + 1))) |
339 | 77, 77 | fvsn 6351 |
. . . . . 6
⊢
({〈(𝑀 + 1),
(𝑀 + 1)〉}‘(𝑀 + 1)) = (𝑀 + 1) |
340 | 338, 339 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1)) |
341 | 174, 340 | jca 553 |
. . . 4
⊢ (𝜑 → (((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))) |
342 | 331, 341 | jctird 565 |
. . 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))))) |
343 | | 3anass 1035 |
. . 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)))) |
344 | 342, 343 | syl6ibr 241 |
. 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)))) |
345 | 1, 97 | jctir 559 |
. . . . . 6
⊢ (𝜑 → (𝑇:(1...𝑀)⟶(0..^𝐾) ∧ {〈(𝑀 + 1), 0〉}:{(𝑀 + 1)}⟶{0})) |
346 | 345, 94, 98 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):((1...𝑀) ∪ {(𝑀 + 1)})⟶((0..^𝐾) ∪ {0})) |
347 | 346, 116 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
348 | | ovex 6577 |
. . . . 5
⊢
(0..^𝐾) ∈
V |
349 | 348, 157 | elmap 7772 |
. . . 4
⊢ ((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∈ ((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ↔
(𝑇 ∪ {〈(𝑀 + 1), 0〉}):(1...(𝑀 + 1))⟶(0..^𝐾)) |
350 | 347, 349 | sylibr 223 |
. . 3
⊢ (𝜑 → (𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∈ ((0..^𝐾) ↑𝑚
(1...(𝑀 +
1)))) |
351 | | f1oexrnex 7008 |
. . . . . . . 8
⊢ ((𝑈:(1...𝑀)–1-1-onto→(1...𝑀) ∧ (1...𝑀) ∈ V) → 𝑈 ∈ V) |
352 | 12, 45, 351 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ V) |
353 | | snex 4835 |
. . . . . . 7
⊢
{〈(𝑀 + 1),
(𝑀 + 1)〉} ∈
V |
354 | | unexg 6857 |
. . . . . . 7
⊢ ((𝑈 ∈ V ∧ {〈(𝑀 + 1), (𝑀 + 1)〉} ∈ V) → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ V) |
355 | 352, 353,
354 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ V) |
356 | | f1oeq1 6040 |
. . . . . . 7
⊢ (𝑓 = (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) → (𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)))) |
357 | 356 | elabg 3320 |
. . . . . 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 6043 |
. . . . . 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 | 108, 108,
359 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1)) ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))) |
361 | 358, 360 | bitrd 267 |
. . . 4
⊢ (𝜑 → ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))} ↔ (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}):((1...𝑀) ∪ {(𝑀 + 1)})–1-1-onto→((1...𝑀) ∪ {(𝑀 + 1)}))) |
362 | 129, 361 | mpbird 246 |
. . 3
⊢ (𝜑 → (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) ∈ {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) |
363 | | opelxpi 5072 |
. . 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 | 350, 362,
363 | syl2anc 691 |
. 2
⊢ (𝜑 → 〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑𝑚
(1...(𝑀 + 1))) ×
{𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))})) |
365 | 344, 364 | jctild 564 |
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))))) |