Step | Hyp | Ref
| Expression |
1 | | nfv 1873 |
. . . . . . . . 9
⊢
Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) |
2 | | nfcsb1v 3800 |
. . . . . . . . . 10
⊢
Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) |
3 | | nfcv 2926 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(1...𝑁) |
4 | | nfcv 2926 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(0...𝐾) |
5 | 2, 3, 4 | nff 6334 |
. . . . . . . . 9
⊢
Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) |
6 | 1, 5 | nfim 1859 |
. . . . . . . 8
⊢
Ⅎ𝑗((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
7 | | eleq1 2847 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1)))) |
8 | 7 | anbi2d 619 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))))) |
9 | | csbeq1a 3791 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
10 | 9 | feq1d 6323 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))) |
11 | 8, 10 | imbi12d 337 |
. . . . . . . 8
⊢ (𝑗 = 𝑦 → (((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))) |
12 | | poimir.0 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
13 | 12 | nncnd 11449 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
14 | | npcan1 10858 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
16 | 12 | nnzd 11892 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
17 | | peano2zm 11831 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
19 | | uzid 12066 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
20 | | peano2uz 12108 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
22 | 15, 21 | eqeltrrd 2861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
23 | | fzss2 12756 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
25 | 24 | sselda 3854 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁)) |
26 | | elun 4010 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ({1} ∪ {0}) ↔
(𝑦 ∈ {1} ∨ 𝑦 ∈ {0})) |
27 | | fzofzp1 12942 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾)) |
28 | | elsni 4452 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {1} → 𝑦 = 1) |
29 | 28 | oveq2d 6986 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1)) |
30 | 29 | eleq1d 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾))) |
31 | 27, 30 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾))) |
32 | | elfzoelz 12847 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ) |
33 | 32 | zcnd 11894 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ) |
34 | 33 | addid1d 10632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥) |
35 | | elfzofz 12862 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾)) |
36 | 34, 35 | eqeltrd 2860 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾)) |
37 | | elsni 4452 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {0} → 𝑦 = 0) |
38 | 37 | oveq2d 6986 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0)) |
39 | 38 | eleq1d 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾))) |
40 | 36, 39 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾))) |
41 | 31, 40 | jaod 845 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾))) |
42 | 26, 41 | syl5bi 234 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾))) |
43 | 42 | imp 398 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾)) |
44 | 43 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾)) |
45 | | poimirlem25.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) |
46 | 45 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾)) |
47 | | 1ex 10427 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
48 | 47 | fconst 6388 |
. . . . . . . . . . . . 13
⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} |
49 | | c0ex 10425 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
50 | 49 | fconst 6388 |
. . . . . . . . . . . . 13
⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0} |
51 | 48, 50 | pm3.2i 463 |
. . . . . . . . . . . 12
⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) |
52 | | poimirlem25.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
53 | | dff1o3 6444 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
54 | 53 | simprbi 489 |
. . . . . . . . . . . . . 14
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
55 | | imain 6266 |
. . . . . . . . . . . . . 14
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁)))) |
56 | 52, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁)))) |
57 | | elfznn0 12809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0) |
58 | 57 | nn0red 11761 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
59 | 58 | ltp1d 11363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1)) |
60 | | fzdisj 12743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
62 | 61 | imaeq2d 5764 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅)) |
63 | | ima0 5779 |
. . . . . . . . . . . . . 14
⊢ (𝑈 “ ∅) =
∅ |
64 | 62, 63 | syl6eq 2824 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
65 | 56, 64 | sylan9req 2829 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) |
66 | | fun 6363 |
. . . . . . . . . . . 12
⊢
(((((𝑈 “
(1...𝑗)) ×
{1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
67 | 51, 65, 66 | sylancr 578 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
68 | | nn0p1nn 11741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
69 | 57, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ) |
70 | | nnuz 12088 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
71 | 69, 70 | syl6eleq 2870 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
72 | | elfzuz3 12714 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
73 | | fzsplit2 12741 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
74 | 71, 72, 73 | syl2anc 576 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
75 | 74 | imaeq2d 5764 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))) |
76 | | imaundi 5842 |
. . . . . . . . . . . . . 14
⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) |
77 | 75, 76 | syl6req 2825 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁))) |
78 | | f1ofo 6445 |
. . . . . . . . . . . . . 14
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
79 | | foima 6418 |
. . . . . . . . . . . . . 14
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
80 | 52, 78, 79 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
81 | 77, 80 | sylan9eqr 2830 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
82 | 81 | feq2d 6324 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))) |
83 | 67, 82 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})) |
84 | | ovex 7002 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
85 | 84 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V) |
86 | | inidm 4077 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
87 | 44, 46, 83, 85, 85, 86 | off 7236 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
88 | 25, 87 | syldan 582 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
89 | 6, 11, 88 | chvar 2324 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
90 | | fzp1elp1 12769 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) |
91 | 15 | oveq2d 6986 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁)) |
92 | 91 | eleq2d 2845 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁))) |
93 | 92 | biimpa 469 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁)) |
94 | 90, 93 | sylan2 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁)) |
95 | | nfv 1873 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) |
96 | | nfcsb1v 3800 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) |
97 | 96, 3, 4 | nff 6334 |
. . . . . . . . . 10
⊢
Ⅎ𝑗⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) |
98 | 95, 97 | nfim 1859 |
. . . . . . . . 9
⊢
Ⅎ𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
99 | | ovex 7002 |
. . . . . . . . 9
⊢ (𝑦 + 1) ∈ V |
100 | | eleq1 2847 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁))) |
101 | 100 | anbi2d 619 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑦 + 1) → ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)))) |
102 | | csbeq1a 3791 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
103 | 102 | feq1d 6323 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑦 + 1) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))) |
104 | 101, 103 | imbi12d 337 |
. . . . . . . . 9
⊢ (𝑗 = (𝑦 + 1) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))) |
105 | 98, 99, 104, 87 | vtoclf 3471 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
106 | 94, 105 | syldan 582 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
107 | | csbeq1 3785 |
. . . . . . . . 9
⊢ (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
108 | 107 | feq1d 6323 |
. . . . . . . 8
⊢ (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))) |
109 | | csbeq1 3785 |
. . . . . . . . 9
⊢ ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
110 | 109 | feq1d 6323 |
. . . . . . . 8
⊢ ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))) |
111 | 108, 110 | ifboth 4382 |
. . . . . . 7
⊢
((⦋𝑦 /
𝑗⦌(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ∧ ⦋(𝑦 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
112 | 89, 106, 111 | syl2anc 576 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
113 | | ovex 7002 |
. . . . . . 7
⊢
(0...𝐾) ∈
V |
114 | 113, 84 | elmap 8227 |
. . . . . 6
⊢
(⦋if(𝑦
< 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑𝑚
(1...𝑁)) ↔
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
115 | 112, 114 | sylibr 226 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑𝑚
(1...𝑁))) |
116 | 115 | fmpttd 6696 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
117 | | ovex 7002 |
. . . . 5
⊢
((0...𝐾)
↑𝑚 (1...𝑁)) ∈ V |
118 | | ovex 7002 |
. . . . 5
⊢
(0...(𝑁 − 1))
∈ V |
119 | 117, 118 | elmap 8227 |
. . . 4
⊢ ((𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚
(1...𝑁))
↑𝑚 (0...(𝑁 − 1))) ↔ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
120 | 116, 119 | sylibr 226 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚
(1...𝑁))
↑𝑚 (0...(𝑁 − 1)))) |
121 | | rneq 5642 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
122 | 121 | mpteq1d 5010 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥 ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)) |
123 | 122 | rneqd 5644 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)) |
124 | 123 | sseq2d 3885 |
. . . . 5
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ↔ (0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))) |
125 | 121 | rexeqdv 3350 |
. . . . 5
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0 ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0)) |
126 | 124, 125 | anbi12d 621 |
. . . 4
⊢ (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0))) |
127 | 126 | ceqsrexv 3557 |
. . 3
⊢ ((𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚
(1...𝑁))
↑𝑚 (0...(𝑁 − 1))) → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚
(0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0))) |
128 | 120, 127 | syl 17 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚
(0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0))) |
129 | | dfss3 3843 |
. . . 4
⊢
((0...(𝑁 − 1))
⊆ ran (𝑝 ∈ ran
(𝑦 ∈ (0...(𝑁 − 1)) ↦
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)) |
130 | | ovex 7002 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑠) ∘𝑓 +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
131 | | poimirlem28.1 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) |
132 | 130, 131 | csbie 3810 |
. . . . . . . . . . . 12
⊢
⦋((1st ‘𝑠) ∘𝑓 +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = 𝐶 |
133 | 132 | csbeq2i 4251 |
. . . . . . . . . . 11
⊢
⦋〈𝑇, 𝑈〉 / 𝑠⦌⦋((1st
‘𝑠)
∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
134 | | opex 5206 |
. . . . . . . . . . . . 13
⊢
〈𝑇, 𝑈〉 ∈ V |
135 | 134 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈𝑇, 𝑈〉 ∈ V) |
136 | | fveq2 6493 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 〈𝑇, 𝑈〉 → (1st ‘𝑠) = (1st
‘〈𝑇, 𝑈〉)) |
137 | | fex 6809 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V) |
138 | 45, 84, 137 | sylancl 577 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ V) |
139 | | f1oexrnex 7441 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V) |
140 | 52, 84, 139 | sylancl 577 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ∈ V) |
141 | | op1stg 7506 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ V ∧ 𝑈 ∈ V) →
(1st ‘〈𝑇, 𝑈〉) = 𝑇) |
142 | 138, 140,
141 | syl2anc 576 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1st
‘〈𝑇, 𝑈〉) = 𝑇) |
143 | 136, 142 | sylan9eqr 2830 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 = 〈𝑇, 𝑈〉) → (1st ‘𝑠) = 𝑇) |
144 | | fveq2 6493 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 〈𝑇, 𝑈〉 → (2nd ‘𝑠) = (2nd
‘〈𝑇, 𝑈〉)) |
145 | | op2ndg 7507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ V ∧ 𝑈 ∈ V) →
(2nd ‘〈𝑇, 𝑈〉) = 𝑈) |
146 | 138, 140,
145 | syl2anc 576 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘〈𝑇, 𝑈〉) = 𝑈) |
147 | 144, 146 | sylan9eqr 2830 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 = 〈𝑇, 𝑈〉) → (2nd ‘𝑠) = 𝑈) |
148 | | imaeq1 5759 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑠) = 𝑈 → ((2nd ‘𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗))) |
149 | 148 | xpeq1d 5429 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑠) = 𝑈 → (((2nd ‘𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1})) |
150 | | imaeq1 5759 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑠) = 𝑈 → ((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁))) |
151 | 150 | xpeq1d 5429 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑠) = 𝑈 → (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) |
152 | 149, 151 | uneq12d 4025 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑠) = 𝑈 → ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) |
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 = 〈𝑇, 𝑈〉) → ((((2nd
‘𝑠) “
(1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) |
154 | 143, 153 | oveq12d 6988 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 = 〈𝑇, 𝑈〉) → ((1st ‘𝑠) ∘𝑓 +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
155 | 154 | csbeq1d 3789 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 = 〈𝑇, 𝑈〉) →
⦋((1st ‘𝑠) ∘𝑓 +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = ⦋(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
156 | 135, 155 | csbied 3811 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋〈𝑇, 𝑈〉 / 𝑠⦌⦋((1st
‘𝑠)
∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = ⦋(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
157 | 133, 156 | syl5eqr 2822 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
158 | 157 | csbeq2dv 4250 |
. . . . . . . . 9
⊢ (𝜑 → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
159 | 158 | eqeq2d 2782 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵)) |
160 | 159 | rexbidv 3236 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵)) |
161 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑖 ∈ V |
162 | | eqid 2772 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) |
163 | 162 | elrnmpt 5664 |
. . . . . . . . 9
⊢ (𝑖 ∈ V → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵)) |
164 | 161, 163 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵) |
165 | | nfv 1873 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑖 = 𝐵 |
166 | | nfcsb1v 3800 |
. . . . . . . . . 10
⊢
Ⅎ𝑝⦋𝑘 / 𝑝⦌𝐵 |
167 | 166 | nfeq2 2941 |
. . . . . . . . 9
⊢
Ⅎ𝑝 𝑖 = ⦋𝑘 / 𝑝⦌𝐵 |
168 | | csbeq1a 3791 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑝⦌𝐵) |
169 | 168 | eqeq2d 2782 |
. . . . . . . . 9
⊢ (𝑝 = 𝑘 → (𝑖 = 𝐵 ↔ 𝑖 = ⦋𝑘 / 𝑝⦌𝐵)) |
170 | 165, 167,
169 | cbvrex 3374 |
. . . . . . . 8
⊢
(∃𝑝 ∈ ran
(𝑦 ∈ (0...(𝑁 − 1)) ↦
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = ⦋𝑘 / 𝑝⦌𝐵) |
171 | | ovex 7002 |
. . . . . . . . . . 11
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
172 | 171 | csbex 5066 |
. . . . . . . . . 10
⊢
⦋if(𝑦
< 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
173 | 172 | rgenw 3094 |
. . . . . . . . 9
⊢
∀𝑦 ∈
(0...(𝑁 −
1))⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
174 | | eqid 2772 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
175 | | csbeq1 3785 |
. . . . . . . . . . . 12
⊢ (𝑘 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) →
⦋𝑘 / 𝑝⦌𝐵 = ⦋⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
176 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
177 | 176, 99 | ifex 4392 |
. . . . . . . . . . . . 13
⊢ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V |
178 | | csbnestg 4256 |
. . . . . . . . . . . . 13
⊢ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V →
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = ⦋⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
⦋if(𝑦
< 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 = ⦋⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵 |
180 | 175, 179 | syl6eqr 2826 |
. . . . . . . . . . 11
⊢ (𝑘 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) →
⦋𝑘 / 𝑝⦌𝐵 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
181 | 180 | eqeq2d 2782 |
. . . . . . . . . 10
⊢ (𝑘 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = ⦋𝑘 / 𝑝⦌𝐵 ↔ 𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵)) |
182 | 174, 181 | rexrnmpt 6680 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(0...(𝑁 −
1))⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V →
(∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = ⦋𝑘 / 𝑝⦌𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵)) |
183 | 173, 182 | ax-mp 5 |
. . . . . . . 8
⊢
(∃𝑘 ∈ ran
(𝑦 ∈ (0...(𝑁 − 1)) ↦
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = ⦋𝑘 / 𝑝⦌𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
184 | 164, 170,
183 | 3bitri 289 |
. . . . . . 7
⊢ (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝⦌𝐵) |
185 | 160, 184 | syl6bbr 281 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))) |
186 | 24 | sselda 3854 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁)) |
187 | 186 | adantr 473 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁)) |
188 | | elfzelz 12717 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ) |
189 | 188 | zred 11893 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
190 | 189 | adantl 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) |
191 | | ltne 10529 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉 ≠ 𝑦) |
192 | 191 | necomd 3016 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦 ≠ 𝑉) |
193 | 190, 192 | sylan 572 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ≠ 𝑉) |
194 | | eldifsn 4587 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦 ≠ 𝑉)) |
195 | 187, 193,
194 | sylanbrc 575 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉})) |
196 | 94 | adantr 473 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁)) |
197 | | poimirlem24.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ∈ (0...𝑁)) |
198 | | elfzelz 12717 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ) |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ∈ ℤ) |
200 | 199 | zred 11893 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ ℝ) |
201 | 200 | ad2antrr 713 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ) |
202 | | zre 11790 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ ℤ → 𝑉 ∈
ℝ) |
203 | | zre 11790 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
204 | | lenlt 10511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉)) |
205 | 202, 203,
204 | syl2an 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉)) |
206 | | zleltp1 11839 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉 ≤ 𝑦 ↔ 𝑉 < (𝑦 + 1))) |
207 | 205, 206 | bitr3d 273 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬
𝑦 < 𝑉 ↔ 𝑉 < (𝑦 + 1))) |
208 | 199, 188,
207 | syl2an 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉 ↔ 𝑉 < (𝑦 + 1))) |
209 | 208 | biimpa 469 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1)) |
210 | 201, 209 | gtned 10567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉) |
211 | | eldifsn 4587 |
. . . . . . . . . . 11
⊢ ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉)) |
212 | 196, 210,
211 | sylanbrc 575 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉})) |
213 | 195, 212 | ifclda 4378 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉})) |
214 | | nfcsb1v 3800 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
215 | 214 | nfeq2 2941 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗 𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
216 | | csbeq1a 3791 |
. . . . . . . . . . . 12
⊢ (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
217 | 216 | eqeq2d 2782 |
. . . . . . . . . . 11
⊢ (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
218 | 215, 217 | rspce 3524 |
. . . . . . . . . 10
⊢
((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
219 | 218 | ex 405 |
. . . . . . . . 9
⊢ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
220 | 213, 219 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
221 | 220 | rexlimdva 3223 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
222 | | nfv 1873 |
. . . . . . . 8
⊢
Ⅎ𝑗𝜑 |
223 | | nfcv 2926 |
. . . . . . . . 9
⊢
Ⅎ𝑗(0...(𝑁 − 1)) |
224 | 223, 215 | nfrex 3247 |
. . . . . . . 8
⊢
Ⅎ𝑗∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
225 | | eldifi 3989 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁)) |
226 | 225, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0) |
227 | 226 | nn0ge0d 11763 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗) |
228 | 227 | ad2antlr 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗) |
229 | 226 | nn0red 11761 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ) |
230 | 229 | ad2antlr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ) |
231 | 200 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ) |
232 | 16 | zred 11893 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
233 | 232 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ) |
234 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉) |
235 | | elfzle2 12720 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁) |
236 | 197, 235 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ≤ 𝑁) |
237 | 236 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ≤ 𝑁) |
238 | 230, 231,
233, 234, 237 | ltletrd 10592 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁) |
239 | 226 | nn0zd 11891 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ) |
240 | | zltlem1 11841 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ 𝑗 ≤ (𝑁 − 1))) |
241 | 239, 16, 240 | syl2anr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁 ↔ 𝑗 ≤ (𝑁 − 1))) |
242 | 241 | adantr 473 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁 ↔ 𝑗 ≤ (𝑁 − 1))) |
243 | 238, 242 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1)) |
244 | | 0z 11797 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
245 | | elfz 12707 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℤ ∧ 0 ∈
ℤ ∧ (𝑁 − 1)
∈ ℤ) → (𝑗
∈ (0...(𝑁 − 1))
↔ (0 ≤ 𝑗 ∧
𝑗 ≤ (𝑁 − 1)))) |
246 | 244, 245 | mp3an2 1428 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
→ (𝑗 ∈
(0...(𝑁 − 1)) ↔
(0 ≤ 𝑗 ∧ 𝑗 ≤ (𝑁 − 1)))) |
247 | 239, 18, 246 | syl2anr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝑁 − 1)))) |
248 | 247 | adantr 473 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝑁 − 1)))) |
249 | 228, 243,
248 | mpbir2and 700 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1))) |
250 | | 0red 10435 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ) |
251 | 200 | ad2antrr 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ) |
252 | 229 | ad2antlr 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ) |
253 | | elfzle1 12719 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉) |
254 | 197, 253 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝑉) |
255 | 254 | ad2antrr 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉) |
256 | | lenlt 10511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉)) |
257 | 200, 229,
256 | syl2an 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉)) |
258 | 257 | biimpar 470 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ≤ 𝑗) |
259 | | eldifsni 4590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ≠ 𝑉) |
260 | 259 | ad2antlr 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ≠ 𝑉) |
261 | | ltlen 10533 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉))) |
262 | 200, 229,
261 | syl2an 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉))) |
263 | 262 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉))) |
264 | 258, 260,
263 | mpbir2and 700 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗) |
265 | 250, 251,
252, 255, 264 | lelttrd 10590 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗) |
266 | | zgt0ge1 11842 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℤ → (0 <
𝑗 ↔ 1 ≤ 𝑗)) |
267 | 239, 266 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗)) |
268 | 267 | ad2antlr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗)) |
269 | 265, 268 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗) |
270 | | elfzle2 12720 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ≤ 𝑁) |
271 | 225, 270 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ≤ 𝑁) |
272 | 271 | ad2antlr 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ≤ 𝑁) |
273 | | 1z 11818 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
274 | | elfz 12707 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑗 ∈
(1...𝑁) ↔ (1 ≤
𝑗 ∧ 𝑗 ≤ 𝑁))) |
275 | 273, 274 | mp3an2 1428 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
276 | 239, 16, 275 | syl2anr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
277 | 276 | adantr 473 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
278 | 269, 272,
277 | mpbir2and 700 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁)) |
279 | | elfzmlbm 12826 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1))) |
280 | 278, 279 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1))) |
281 | 249, 280 | ifclda 4378 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1))) |
282 | | breq1 4926 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉)) |
283 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1))) |
284 | | oveq1 6977 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) |
285 | 282, 283,
284 | ifbieq12d 4371 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))) |
286 | 285 | eqeq2d 2782 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))) |
287 | | breq1 4926 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉)) |
288 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1))) |
289 | | oveq1 6977 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) |
290 | 287, 288,
289 | ifbieq12d 4371 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))) |
291 | 290 | eqeq2d 2782 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))) |
292 | | iftrue 4350 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗) |
293 | 292 | eqcomd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 < 𝑉 → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1))) |
294 | 293 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1))) |
295 | | zlem1lt 11840 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗 ≤ 𝑉 ↔ (𝑗 − 1) < 𝑉)) |
296 | 239, 199,
295 | syl2anr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ≤ 𝑉 ↔ (𝑗 − 1) < 𝑉)) |
297 | 259 | necomd 3016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉 ≠ 𝑗) |
298 | 297 | adantl 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉 ≠ 𝑗) |
299 | | ltlen 10533 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗))) |
300 | 229, 200,
299 | syl2anr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗))) |
301 | 300 | biimprd 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗) → 𝑗 < 𝑉)) |
302 | 298, 301 | mpan2d 681 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ≤ 𝑉 → 𝑗 < 𝑉)) |
303 | 296, 302 | sylbird 252 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉 → 𝑗 < 𝑉)) |
304 | 303 | con3dimp 400 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉) |
305 | 304 | iffalsed 4355 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1)) |
306 | 226 | nn0cnd 11762 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ) |
307 | | npcan1 10858 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗) |
308 | 306, 307 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗) |
309 | 308 | ad2antlr 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗) |
310 | 305, 309 | eqtr2d 2809 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1))) |
311 | 286, 291,
294, 310 | ifbothda 4381 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))) |
312 | | csbeq1a 3791 |
. . . . . . . . . . . . 13
⊢ (𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) →
⦋〈𝑇,
𝑈〉 / 𝑠⦌𝐶 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
313 | 311, 312 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
314 | 313 | eqeq2d 2782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
315 | 314 | biimpd 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑖 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
316 | | breq1 4926 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉)) |
317 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1))) |
318 | | oveq1 6977 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) |
319 | 316, 317,
318 | ifbieq12d 4371 |
. . . . . . . . . . . . 13
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))) |
320 | 319 | csbeq1d 3789 |
. . . . . . . . . . . 12
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
321 | 320 | eqeq2d 2782 |
. . . . . . . . . . 11
⊢ (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
322 | 321 | rspcev 3529 |
. . . . . . . . . 10
⊢
((if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)) ∧ 𝑖 = ⦋if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
323 | 281, 315,
322 | syl6an 671 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
324 | 323 | ex 405 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
325 | 222, 224,
324 | rexlimd 3254 |
. . . . . . 7
⊢ (𝜑 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
326 | 221, 325 | impbid 204 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
327 | 185, 326 | bitr3d 273 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
328 | 327 | ralbidv 3141 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
329 | 129, 328 | syl5bb 275 |
. . 3
⊢ (𝜑 → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
330 | 329 | anbi1d 620 |
. 2
⊢ (𝜑 → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0))) |
331 | 12, 45, 52, 197 | poimirlem23 34304 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) |
332 | 331 | anbi2d 619 |
. 2
⊢ (𝜑 → ((∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))) |
333 | 128, 330,
332 | 3bitrd 297 |
1
⊢ (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚
(0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))) |