Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . 3
โข (((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ ๐
โ Fin) |
2 | | simplr 768 |
. . 3
โข (((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ ๐น:โโถ๐
) |
3 | | oveq1 7416 |
. . . . . . . . . . 11
โข (๐ = ๐ค โ (๐ ยท ๐) = (๐ค ยท ๐)) |
4 | 3 | oveq2d 7425 |
. . . . . . . . . 10
โข (๐ = ๐ค โ (๐ + (๐ ยท ๐)) = (๐ + (๐ค ยท ๐))) |
5 | 4 | eleq1d 2819 |
. . . . . . . . 9
โข (๐ = ๐ค โ ((๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ (๐ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}))) |
6 | 5 | cbvralvw 3235 |
. . . . . . . 8
โข
(โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ค โ (0...(๐ โ 1))(๐ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข})) |
7 | | oveq1 7416 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ + (๐ค ยท ๐)) = (๐ฆ + (๐ค ยท ๐))) |
8 | 7 | eleq1d 2819 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ ((๐ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}) โ (๐ฆ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}))) |
9 | 8 | ralbidv 3178 |
. . . . . . . 8
โข (๐ = ๐ฆ โ (โ๐ค โ (0...(๐ โ 1))(๐ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}))) |
10 | 6, 9 | bitrid 283 |
. . . . . . 7
โข (๐ = ๐ฆ โ (โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}))) |
11 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ค ยท ๐) = (๐ค ยท ๐ง)) |
12 | 11 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ = ๐ง โ (๐ฆ + (๐ค ยท ๐)) = (๐ฆ + (๐ค ยท ๐ง))) |
13 | 12 | eleq1d 2819 |
. . . . . . . 8
โข (๐ = ๐ง โ ((๐ฆ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}) โ (๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
14 | 13 | ralbidv 3178 |
. . . . . . 7
โข (๐ = ๐ง โ (โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
15 | 10, 14 | cbvrex2vw 3240 |
. . . . . 6
โข
(โ๐ โ
โ โ๐ โ
โ โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข})) |
16 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (๐ โ 1) = (๐ฅ โ 1)) |
17 | 16 | oveq2d 7425 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (0...(๐ โ 1)) = (0...(๐ฅ โ 1))) |
18 | 17 | raleqdv 3326 |
. . . . . . 7
โข (๐ = ๐ฅ โ (โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}) โ โ๐ค โ (0...(๐ฅ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
19 | 18 | 2rexbidv 3220 |
. . . . . 6
โข (๐ = ๐ฅ โ (โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}) โ โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ฅ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
20 | 15, 19 | bitrid 283 |
. . . . 5
โข (๐ = ๐ฅ โ (โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ฅ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
21 | 20 | notbid 318 |
. . . 4
โข (๐ = ๐ฅ โ (ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ ยฌ โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ฅ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข}))) |
22 | 21 | cbvrabv 3443 |
. . 3
โข {๐ โ โ โฃ ยฌ
โ๐ โ โ
โ๐ โ โ
โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} = {๐ฅ โ โ โฃ ยฌ โ๐ฆ โ โ โ๐ง โ โ โ๐ค โ (0...(๐ฅ โ 1))(๐ฆ + (๐ค ยท ๐ง)) โ (โก๐น โ {๐ข})} |
23 | | simpr 486 |
. . . . 5
โข (((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
24 | | sneq 4639 |
. . . . . . . . . . 11
โข (๐ = ๐ข โ {๐} = {๐ข}) |
25 | 24 | imaeq2d 6060 |
. . . . . . . . . 10
โข (๐ = ๐ข โ (โก๐น โ {๐}) = (โก๐น โ {๐ข})) |
26 | 25 | eleq2d 2820 |
. . . . . . . . 9
โข (๐ = ๐ข โ ((๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ (๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}))) |
27 | 26 | ralbidv 3178 |
. . . . . . . 8
โข (๐ = ๐ข โ (โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}))) |
28 | 27 | 2rexbidv 3220 |
. . . . . . 7
โข (๐ = ๐ข โ (โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}))) |
29 | 28 | ralbidv 3178 |
. . . . . 6
โข (๐ = ๐ข โ (โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}))) |
30 | 29 | cbvrexvw 3236 |
. . . . 5
โข
(โ๐ โ
๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ โ๐ข โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
31 | 23, 30 | sylnib 328 |
. . . 4
โข (((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ ยฌ โ๐ข โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
32 | | rabn0 4386 |
. . . . . . 7
โข ({๐ โ โ โฃ ยฌ
โ๐ โ โ
โ๐ โ โ
โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} โ โ
โ โ๐ โ โ ยฌ
โ๐ โ โ
โ๐ โ โ
โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
33 | | rexnal 3101 |
. . . . . . 7
โข
(โ๐ โ
โ ยฌ โ๐
โ โ โ๐
โ โ โ๐
โ (0...(๐ โ
1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
34 | 32, 33 | bitri 275 |
. . . . . 6
โข ({๐ โ โ โฃ ยฌ
โ๐ โ โ
โ๐ โ โ
โ๐ โ
(0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} โ โ
โ ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
35 | 34 | ralbii 3094 |
. . . . 5
โข
(โ๐ข โ
๐
{๐ โ โ โฃ ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} โ โ
โ โ๐ข โ ๐
ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
36 | | ralnex 3073 |
. . . . 5
โข
(โ๐ข โ
๐
ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข}) โ ยฌ โ๐ข โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
37 | 35, 36 | bitri 275 |
. . . 4
โข
(โ๐ข โ
๐
{๐ โ โ โฃ ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} โ โ
โ ยฌ โ๐ข โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})) |
38 | 31, 37 | sylibr 233 |
. . 3
โข (((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ โ๐ข โ ๐
{๐ โ โ โฃ ยฌ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐ข})} โ โ
) |
39 | 1, 2, 22, 38 | vdwnnlem3 16930 |
. 2
โข ยฌ
((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
40 | | iman 403 |
. 2
โข (((๐
โ Fin โง ๐น:โโถ๐
) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) โ ยฌ ((๐
โ Fin โง ๐น:โโถ๐
) โง ยฌ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
41 | 39, 40 | mpbir 230 |
1
โข ((๐
โ Fin โง ๐น:โโถ๐
) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |