Step | Hyp | Ref
| Expression |
1 | | neq0 4244 |
. . 3
⊢ (¬
{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) |
2 | | 2z 12107 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
3 | | iddvds 15727 |
. . . . . . . 8
⊢ (2 ∈
ℤ → 2 ∥ 2) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢ 2 ∥
2 |
5 | | df-2 11791 |
. . . . . . 7
⊢ 2 = (1 +
1) |
6 | 4, 5 | breqtri 5065 |
. . . . . 6
⊢ 2 ∥
(1 + 1) |
7 | | vex 3404 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
8 | | fzfi 13443 |
. . . . . . . . . . . . 13
⊢
(0...𝑁) ∈
Fin |
9 | | rabfi 8833 |
. . . . . . . . . . . . 13
⊢
((0...𝑁) ∈ Fin
→ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∈ Fin) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∈ Fin |
11 | | diffi 8839 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∈ Fin) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∈ Fin |
13 | | neldifsn 4690 |
. . . . . . . . . . 11
⊢ ¬
𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) |
14 | 12, 13 | pm3.2i 474 |
. . . . . . . . . 10
⊢ (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) |
15 | | hashunsng 13857 |
. . . . . . . . . 10
⊢ (𝑡 ∈ V → ((({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∪ {𝑡})) = ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) + 1))) |
16 | 7, 14, 15 | mp2 9 |
. . . . . . . . 9
⊢
(♯‘(({𝑦
∈ (0...𝑁) ∣
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∪ {𝑡})) = ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) + 1) |
17 | | difsnid 4708 |
. . . . . . . . . 10
⊢ (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) |
18 | 17 | fveq2d 6690 |
. . . . . . . . 9
⊢ (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∪ {𝑡})) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |
19 | 16, 18 | eqtr3id 2788 |
. . . . . . . 8
⊢ (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |
21 | | sneq 4536 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑡 → {𝑦} = {𝑡}) |
22 | 21 | difeq2d 4023 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡})) |
23 | 22 | rexeqdv 3318 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
24 | 23 | ralbidv 3110 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
25 | 24 | elrab 3593 |
. . . . . . . . 9
⊢ (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
26 | | poimirlem25.5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ≠ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
27 | 26 | ralrimiva 3097 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁 ≠ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
28 | | nfcv 2900 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗𝑁 |
29 | | nfcsb1v 3824 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
30 | 28, 29 | nfne 3035 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗 𝑁 ≠ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
31 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑡 → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
32 | 31 | neeq2d 2995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑡 → (𝑁 ≠ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑁 ≠ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
33 | 30, 32 | rspc 3517 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁 ≠ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑁 ≠ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
34 | 27, 33 | mpan9 510 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → 𝑁 ≠ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
35 | | nesym 2991 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ≠ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁) |
36 | 34, 35 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁) |
37 | | nfv 1921 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗(𝜑 ∧ 𝑡 ∈ (0...𝑁)) |
38 | 29 | nfel1 2916 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) |
39 | 37, 38 | nfim 1903 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)) |
40 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁))) |
41 | 40 | anbi2d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑡 → ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑡 ∈ (0...𝑁)))) |
42 | 31 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑡 → (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁))) |
43 | 41, 42 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑡 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)) ↔ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)))) |
44 | | poimirlem25.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) |
45 | | ovex 7215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0..^𝐾) ∈
V |
46 | | ovex 7215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1...𝑁) ∈
V |
47 | 45, 46 | elmap 8493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾)) |
48 | 44, 47 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁))) |
49 | | poimirlem25.4 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
50 | | fzfi 13443 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1...𝑁) ∈
Fin |
51 | | f1oexrnex 7670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V) |
52 | 50, 51 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V) |
53 | | f1oeq1 6618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))) |
54 | 53 | elabg 3576 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈 ∈ V → (𝑈 ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → (𝑈 ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))) |
56 | 55 | ibir 271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
57 | 49, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
58 | | opelxpi 5572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁)) ∧ 𝑈 ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 〈𝑇, 𝑈〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
59 | 48, 57, 58 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 〈𝑇, 𝑈〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
60 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 〈𝑇, 𝑈〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
61 | | nfcv 2900 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑠〈𝑇, 𝑈〉 |
62 | | nfv 1921 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑠(𝜑 ∧ 𝑗 ∈ (0...𝑁)) |
63 | | nfcsb1v 3824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑠⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
64 | 63 | nfel1 2916 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑠⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) |
65 | 62, 64 | nfim 1903 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑠((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)) |
66 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 〈𝑇, 𝑈〉 → 𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
67 | 66 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 〈𝑇, 𝑈〉 → (𝐶 ∈ (0...𝑁) ↔ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁))) |
68 | 67 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 〈𝑇, 𝑈〉 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)))) |
69 | | elun 4049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 ∈ ({1} ∪ {0}) ↔
(𝑝 ∈ {1} ∨ 𝑝 ∈ {0})) |
70 | | fzofzp1 13237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾)) |
71 | | elsni 4543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑝 ∈ {1} → 𝑝 = 1) |
72 | 71 | oveq2d 7198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1)) |
73 | 72 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾))) |
74 | 70, 73 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾))) |
75 | | elfzonn0 13185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0) |
76 | 75 | nn0cnd 12050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ) |
77 | 76 | addid1d 10930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖) |
78 | | elfzofz 13156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾)) |
79 | 77, 78 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾)) |
80 | | elsni 4543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑝 ∈ {0} → 𝑝 = 0) |
81 | 80 | oveq2d 7198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0)) |
82 | 81 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾))) |
83 | 79, 82 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾))) |
84 | 74, 83 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾))) |
85 | 69, 84 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾))) |
86 | 85 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾)) |
87 | 86 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾)) |
88 | | xp1st 7758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘𝑠) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
89 | | elmapi 8471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘𝑠) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘𝑠):(1...𝑁)⟶(0..^𝐾)) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘𝑠):(1...𝑁)⟶(0..^𝐾)) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘𝑠):(1...𝑁)⟶(0..^𝐾)) |
92 | | xp2nd 7759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘𝑠) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
93 | | fvex 6699 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(2nd ‘𝑠) ∈ V |
94 | | f1oeq1 6618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (2nd ‘𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁))) |
95 | 93, 94 | elab 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((2nd ‘𝑠) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁)) |
96 | 92, 95 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁)) |
97 | | 1ex 10727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
V |
98 | 97 | fconst 6574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘𝑠) “ (1...𝑗)) × {1}):((2nd ‘𝑠) “ (1...𝑗))⟶{1} |
99 | | c0ex 10725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
V |
100 | 99 | fconst 6574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))⟶{0} |
101 | 98, 100 | pm3.2i 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((2nd ‘𝑠) “ (1...𝑗)) × {1}):((2nd ‘𝑠) “ (1...𝑗))⟶{1} ∧
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}) |
102 | | dff1o3 6636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘𝑠))) |
103 | | imain 6434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡(2nd ‘𝑠) → ((2nd
‘𝑠) “
((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘𝑠) “ (1...𝑗)) ∩ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)))) |
104 | 102, 103 | simplbiim 508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘𝑠) “ (1...𝑗)) ∩ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)))) |
105 | | elfznn0 13103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0) |
106 | 105 | nn0red 12049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
107 | 106 | ltp1d 11660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1)) |
108 | | fzdisj 13037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
110 | 109 | imaeq2d 5913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘𝑠) “
∅)) |
111 | | ima0 5929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘𝑠) “ ∅) = ∅ |
112 | 110, 111 | eqtrdi 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
113 | 104, 112 | sylan9req 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘𝑠) “ (1...𝑗)) ∩ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))) = ∅) |
114 | | fun 6550 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((2nd ‘𝑠) “ (1...𝑗)) × {1}):((2nd ‘𝑠) “ (1...𝑗))⟶{1} ∧
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ (((2nd
‘𝑠) “
(1...𝑗)) ∩
((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁))) = ∅) →
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd
‘𝑠) “
(1...𝑗)) ∪
((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)))⟶({1} ∪
{0})) |
115 | 101, 113,
114 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) ×
{0})):(((2nd ‘𝑠) “ (1...𝑗)) ∪ ((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
116 | | nn0p1nn 12027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
117 | 105, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ) |
118 | | nnuz 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ℕ =
(ℤ≥‘1) |
119 | 117, 118 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
120 | | elfzuz3 13007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
121 | | fzsplit2 13035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
122 | 119, 120,
121 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
123 | 122 | imaeq2d 5913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘𝑠) “ (1...𝑁)) = ((2nd ‘𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))) |
124 | | imaundi 5992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘𝑠) “ (1...𝑗)) ∪ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))) |
125 | 123, 124 | eqtr2di 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑁) → (((2nd ‘𝑠) “ (1...𝑗)) ∪ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd ‘𝑠) “ (1...𝑁))) |
126 | | f1ofo 6637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘𝑠):(1...𝑁)–onto→(1...𝑁)) |
127 | | foima 6607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘𝑠) “ (1...𝑁)) = (1...𝑁)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘𝑠) “ (1...𝑁)) = (1...𝑁)) |
129 | 125, 128 | sylan9eqr 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘𝑠) “ (1...𝑗)) ∪ ((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
130 | 129 | feq2d 6500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) ×
{0})):(((2nd ‘𝑠) “ (1...𝑗)) ∪ ((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))) |
131 | 115, 130 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((2nd ‘𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪
{0})) |
132 | 96, 131 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪
{0})) |
133 | | fzfid 13444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
134 | | inidm 4119 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
135 | 87, 91, 132, 133, 133, 134 | off 7454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) |
136 | | ovex 7215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘𝑠) ∘f + ((((2nd
‘𝑠) “
(1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0}))) ∈
V |
137 | | feq1 6495 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))) |
138 | 137 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) ↔ (𝜑 ∧ ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))) |
139 | | poimirlem28.1 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) |
140 | 139 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐵 ∈ (0...𝑁) ↔ 𝐶 ∈ (0...𝑁))) |
141 | 138, 140 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) ↔ ((𝜑 ∧ ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁)))) |
142 | | poimirlem28.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) |
143 | 136, 141,
142 | vtocl 3466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((1st
‘𝑠)
∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁)) |
144 | 135, 143 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁)) |
145 | 144 | an12s 649 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (𝜑 ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁)) |
146 | 145 | ex 416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁))) |
147 | 61, 65, 68, 146 | vtoclgaf 3480 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑇, 𝑈〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁))) |
148 | 60, 147 | mpcom 38 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)) |
149 | 39, 43, 148 | chvarfv 2242 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁)) |
150 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℕ) |
151 | 150 | nnnn0d 12048 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
152 | | nn0uz 12374 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
153 | 151, 152 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
154 | | fzm1 13090 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘0) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
156 | 155 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
157 | 149, 156 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁)) |
158 | 157 | ord 863 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁)) |
159 | 36, 158 | mt3d 150 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
160 | 159 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
161 | | fzfi 13443 |
. . . . . . . . . . . . . . 15
⊢
(0...(𝑁 − 1))
∈ Fin |
162 | 150 | nncnd 11744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
163 | | 1cnd 10726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 ∈
ℂ) |
164 | 162, 163,
163 | addsubd 11108 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1)) |
165 | | hashfz0 13897 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...𝑁)) = (𝑁 + 1)) |
166 | 151, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1)) |
167 | 166 | oveq1d 7197 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((♯‘(0...𝑁)) − 1) = ((𝑁 + 1) −
1)) |
168 | | nnm1nn0 12029 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
169 | | hashfz0 13897 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
ℕ0 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1)) |
170 | 150, 168,
169 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) +
1)) |
171 | 164, 167,
170 | 3eqtr4rd 2785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘(0...(𝑁 − 1))) =
((♯‘(0...𝑁))
− 1)) |
172 | | hashdifsn 13879 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((0...𝑁) ∈ Fin
∧ 𝑡 ∈ (0...𝑁)) →
(♯‘((0...𝑁)
∖ {𝑡})) =
((♯‘(0...𝑁))
− 1)) |
173 | 8, 172 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (0...𝑁) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1)) |
174 | 173 | eqcomd 2745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (0...𝑁) → ((♯‘(0...𝑁)) − 1) =
(♯‘((0...𝑁)
∖ {𝑡}))) |
175 | 171, 174 | sylan9eq 2794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (♯‘(0...(𝑁 − 1))) =
(♯‘((0...𝑁)
∖ {𝑡}))) |
176 | | diffi 8839 |
. . . . . . . . . . . . . . . . . 18
⊢
((0...𝑁) ∈ Fin
→ ((0...𝑁) ∖
{𝑡}) ∈
Fin) |
177 | 8, 176 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((0...𝑁) ∖
{𝑡}) ∈
Fin |
178 | | hashen 13811 |
. . . . . . . . . . . . . . . . 17
⊢
(((0...(𝑁 −
1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) →
((♯‘(0...(𝑁
− 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))) |
179 | 161, 177,
178 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) |
180 | 175, 179 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) |
181 | | phpreu 35416 |
. . . . . . . . . . . . . . 15
⊢
(((0...(𝑁 −
1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
182 | 161, 180,
181 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
183 | 182 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
184 | 183 | impr 458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
185 | | nfv 1921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧 𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
186 | | nfcsb1v 3824 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
187 | 186 | nfeq2 2917 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
188 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑧 → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
189 | 188 | eqeq2d 2750 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
190 | 185, 187,
189 | cbvreuw 3343 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑗 ∈
((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
191 | | eqeq1 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
192 | 191 | reubidv 3293 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
193 | 190, 192 | syl5bb 286 |
. . . . . . . . . . . . 13
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
194 | 193 | rspcv 3524 |
. . . . . . . . . . . 12
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
195 | 160, 184,
194 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
196 | | an32 646 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
197 | 196 | biimpi 219 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
198 | 197 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
199 | | eqeq2 2751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
200 | | rexsns 4570 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑗 ∈
{𝑡}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ [𝑡 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
201 | 29 | nfeq2 2917 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑗 𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
202 | 31 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑡 → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
203 | 201, 202 | sbciegf 3724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
204 | 7, 203 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
([𝑡 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
205 | 200, 204 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑗 ∈
{𝑡}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
206 | | rexsns 4570 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑗 ∈
{𝑧}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ [𝑧 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
207 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑧 ∈ V |
208 | 187, 189 | sbciegf 3724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
209 | 207, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
([𝑧 / 𝑗]𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
210 | 206, 209 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑗 ∈
{𝑧}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ 𝑖 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
211 | 199, 205,
210 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
212 | 211 | orbi1d 916 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
213 | | rexun 4090 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑗 ∈
({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
214 | | rexun 4090 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑗 ∈
({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
215 | 212, 213,
214 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
216 | 215 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
217 | | eldifsni 4688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ≠ 𝑡) |
218 | 217 | necomd 2990 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡 ≠ 𝑧) |
219 | | dif32 4193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((0...𝑁) ∖
{𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) |
220 | 219 | uneq2i 4060 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) |
221 | | snssi 4706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧})) |
222 | | eldifsn 4685 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡 ≠ 𝑧)) |
223 | | undif 4381 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧})) |
224 | 221, 222,
223 | 3imtr3i 294 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑡 ≠ 𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧})) |
225 | 220, 224 | syl5eq 2786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑡 ≠ 𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧})) |
226 | 218, 225 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧})) |
227 | 226 | rexeqdv 3318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
228 | 227 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
229 | | snssi 4706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡})) |
230 | | undif 4381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡})) |
231 | 229, 230 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡})) |
232 | 231 | rexeqdv 3318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
233 | 232 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
234 | 216, 228,
233 | 3bitr3d 312 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
235 | 234 | ralbidv 3110 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
236 | 235 | biimpar 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
237 | 236 | an32s 652 |
. . . . . . . . . . . . . 14
⊢ ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
238 | 198, 237 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
239 | | simpl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑡 ∈ (0...𝑁)) |
240 | 239 | anim2i 620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → (𝜑 ∧ 𝑡 ∈ (0...𝑁))) |
241 | | necom 2988 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ≠ 𝑡 ↔ 𝑡 ≠ 𝑧) |
242 | 241 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ≠ 𝑡 → 𝑡 ≠ 𝑧) |
243 | 242 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡) → 𝑡 ≠ 𝑧) |
244 | 243 | anim2i 620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡 ≠ 𝑧)) |
245 | | eldifsn 4685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡)) |
246 | 245 | anbi2i 626 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡))) |
247 | 244, 246,
222 | 3imtr4i 295 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧})) |
248 | 247 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧})) |
249 | 248 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧})) |
250 | 29 | nfel1 2916 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑗⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) |
251 | 37, 250 | nfim 1903 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑗((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
252 | 31 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = 𝑡 → (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)))) |
253 | 41, 252 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑡 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))))) |
254 | 26 | necomd 2990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ≠ 𝑁) |
255 | 254 | neneqd 2940 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁) |
256 | | fzm1 13090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈
(ℤ≥‘0) → (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
257 | 153, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 →
(⦋〈𝑇,
𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
258 | 257 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...𝑁) ↔ (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁))) |
259 | 148, 258 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∨ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = 𝑁)) |
260 | 259 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (¬ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) →
⦋〈𝑇,
𝑈〉 / 𝑠⦌𝐶 = 𝑁)) |
261 | 255, 260 | mt3d 150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
262 | 251, 253,
261 | chvarfv 2242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
263 | 262 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1))) |
264 | | eldifi 4027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁)) |
265 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁))) |
266 | 265 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑧 → ((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑧 ∈ (0...𝑁)))) |
267 | | sneq 4536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧}) |
268 | 267 | difeq2d 4023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧})) |
269 | 268 | breq2d 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))) |
270 | 266, 269 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑧 → (((𝜑 ∧ 𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑 ∧ 𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))) |
271 | 270, 180 | chvarvv 2010 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) |
272 | 264, 271 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) |
273 | 272 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) |
274 | | phpreu 35416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((0...(𝑁 −
1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
275 | 161, 274 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((0...(𝑁 − 1))
≈ ((0...𝑁) ∖
{𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
276 | 275 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((0...(𝑁 −
1)) ≈ ((0...𝑁)
∖ {𝑧}) ∧
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
277 | 273, 276 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
278 | | eqeq1 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
279 | 278 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ 𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
280 | 201, 279 | reubida 3291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
281 | 280 | rspcv 3524 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
282 | 263, 277,
281 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
283 | | reurmo 3332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃!𝑗 ∈
((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
284 | 282, 283 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
285 | | nfv 1921 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑖⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
286 | 285 | rmo3 3790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃*𝑗 ∈
((0...𝑁) ∖ {𝑧})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑗 = 𝑖)) |
287 | 284, 286 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑗 = 𝑖)) |
288 | | equcomi 2029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = 𝑡 → 𝑡 = 𝑖) |
289 | 288 | csbeq1d 3804 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = 𝑡 → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
290 | | sbsbc 3689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ([𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
291 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑖 ∈ V |
292 | | sbceqg 4309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ V → ([𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑖 / 𝑗⦌⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
293 | 29 | csbconstgf 3818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ V →
⦋𝑖 / 𝑗⦌⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
294 | 293 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ V →
(⦋𝑖 / 𝑗⦌⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
295 | 292, 294 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ V → ([𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
296 | 291, 295 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
([𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
297 | 290, 296 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑖 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
298 | 289, 297 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑡 → [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
299 | 298 | biantrud 535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑡 → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
300 | 299 | bicomd 226 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑡 → ((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
301 | | eqeq2 2751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑡 → (𝑗 = 𝑖 ↔ 𝑗 = 𝑡)) |
302 | 300, 301 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑡 → (((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑗 = 𝑖) ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡))) |
303 | 302 | rspcv 3524 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑗 = 𝑖) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡))) |
304 | 303 | ralimdv 3093 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ [𝑖 / 𝑗]⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡))) |
305 | 249, 287,
304 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡)) |
306 | | dif32 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((0...𝑁) ∖
{𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) |
307 | 306 | eleq2i 2825 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) |
308 | | eldifsn 4685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗 ≠ 𝑡)) |
309 | | eldifsn 4685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗 ≠ 𝑧)) |
310 | 307, 308,
309 | 3bitr3ri 305 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗 ≠ 𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗 ≠ 𝑡)) |
311 | 310 | imbi1i 353 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗 ≠ 𝑧) → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗 ≠ 𝑡) → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
312 | | impexp 454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗 ≠ 𝑧) → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
313 | | impexp 454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗 ≠ 𝑡) → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
314 | 311, 312,
313 | 3bitr3ri 305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
315 | 314 | albii 1826 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
316 | | con34b 319 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
317 | | df-ne 2936 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ≠ 𝑡 ↔ ¬ 𝑗 = 𝑡) |
318 | 317 | imbi1i 353 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
319 | 316, 318 | bitr4i 281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡) ↔ (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
320 | 319 | ralbii 3081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑧})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
321 | | df-ral 3059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑧})(𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
322 | 320, 321 | bitri 278 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑧})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗 ≠ 𝑡 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
323 | | df-ral 3059 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑡})(𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
324 | 315, 322,
323 | 3bitr4i 306 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑧})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
325 | 305, 324 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
326 | | df-ne 2936 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ≠ 𝑧 ↔ ¬ 𝑗 = 𝑧) |
327 | 326 | imbi1i 353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
328 | | con34b 319 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
329 | 327, 328 | bitr4i 281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑧)) |
330 | | ancr 550 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → 𝑗 = 𝑧) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
331 | 329, 330 | sylbi 220 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
332 | 331 | ralimi 3076 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑡})(𝑗 ≠ 𝑧 → ¬ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
333 | 325, 332 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
334 | 240, 333 | sylanl1 680 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
335 | 201, 278 | rexbid 3231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
336 | 335 | rspcva 3527 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⦋𝑡 /
𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
337 | 262, 336 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
338 | 337 | anasss 470 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
339 | 338 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
340 | | rexim 3155 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑗 ∈
((0...𝑁) ∖ {𝑡})(⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → (𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶))) |
341 | 334, 339,
340 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
342 | | rexex 3154 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑗 ∈
((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
343 | 341, 342 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ∃𝑗(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
344 | 29, 186 | nfeq 2913 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 |
345 | 188 | eqeq2d 2750 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
346 | 344, 345 | equsexv 2269 |
. . . . . . . . . . . . . 14
⊢
(∃𝑗(𝑗 = 𝑧 ∧ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
347 | 343, 346 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) → ⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
348 | 238, 347 | impbida 801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
349 | 348 | reubidva 3292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})⦋𝑡 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 = ⦋𝑧 / 𝑗⦌⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
350 | 195, 349 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) |
351 | | an32 646 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ 𝑧 ≠ 𝑡)) |
352 | 245 | anbi1i 627 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧 ≠ 𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
353 | | sneq 4536 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
354 | 353 | difeq2d 4023 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧})) |
355 | 354 | rexeqdv 3318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
356 | 355 | ralbidv 3110 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
357 | 356 | elrab 3593 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
358 | 357 | anbi1i 627 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∧ 𝑧 ≠ 𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ∧ 𝑧 ≠ 𝑡)) |
359 | 351, 352,
358 | 3bitr4i 306 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∧ 𝑧 ≠ 𝑡)) |
360 | | eldifsn 4685 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∧ 𝑧 ≠ 𝑡)) |
361 | 359, 360 | bitr4i 281 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) |
362 | 361 | eubii 2587 |
. . . . . . . . . . 11
⊢
(∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) |
363 | | df-reu 3061 |
. . . . . . . . . . 11
⊢
(∃!𝑧 ∈
((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) |
364 | | euhash1 13885 |
. . . . . . . . . . . 12
⊢ (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}) ∈ Fin → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡}))) |
365 | 12, 364 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((♯‘({𝑦
∈ (0...𝑁) ∣
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) |
366 | 362, 363,
365 | 3bitr4i 306 |
. . . . . . . . . 10
⊢
(∃!𝑧 ∈
((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ↔ (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) = 1) |
367 | 350, 366 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶)) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) = 1) |
368 | 25, 367 | sylan2b 597 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) = 1) |
369 | 368 | oveq1d 7197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} ∖ {𝑡})) + 1) = (1 + 1)) |
370 | 20, 369 | eqtr3d 2776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) = (1 + 1)) |
371 | 6, 370 | breqtrrid 5078 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |
372 | 371 | ex 416 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}))) |
373 | 372 | exlimdv 1940 |
. . 3
⊢ (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}))) |
374 | 1, 373 | syl5bi 245 |
. 2
⊢ (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} = ∅ → 2 ∥
(♯‘{𝑦 ∈
(0...𝑁) ∣
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}))) |
375 | | dvds0 15729 |
. . . . 5
⊢ (2 ∈
ℤ → 2 ∥ 0) |
376 | 2, 375 | ax-mp 5 |
. . . 4
⊢ 2 ∥
0 |
377 | | hash0 13832 |
. . . 4
⊢
(♯‘∅) = 0 |
378 | 376, 377 | breqtrri 5067 |
. . 3
⊢ 2 ∥
(♯‘∅) |
379 | | fveq2 6686 |
. . 3
⊢ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} = ∅ → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶}) =
(♯‘∅)) |
380 | 378, 379 | breqtrrid 5078 |
. 2
⊢ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶} = ∅ → 2 ∥
(♯‘{𝑦 ∈
(0...𝑁) ∣
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |
381 | 374, 380 | pm2.61d2 184 |
1
⊢ (𝜑 → 2 ∥
(♯‘{𝑦 ∈
(0...𝑁) ∣
∀𝑖 ∈
(0...(𝑁 −
1))∃𝑗 ∈
((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) |