Step | Hyp | Ref
| Expression |
1 | | vdw 16874 |
. . 3
โข ((๐
โ Fin โง ๐พ โ โ0)
โ โ๐ โ
โ โ๐ โ
(๐
โm
(1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐})) |
2 | 1 | 3adant2 1132 |
. 2
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
โ๐ โ โ
โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐})) |
3 | | simpl2 1193 |
. . . . . . 7
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ๐น:โโถ๐
) |
4 | | fz1ssnn 13481 |
. . . . . . 7
โข
(1...๐) โ
โ |
5 | | fssres 6712 |
. . . . . . 7
โข ((๐น:โโถ๐
โง (1...๐) โ โ) โ (๐น โพ (1...๐)):(1...๐)โถ๐
) |
6 | 3, 4, 5 | sylancl 587 |
. . . . . 6
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ (๐น โพ (1...๐)):(1...๐)โถ๐
) |
7 | | simpl1 1192 |
. . . . . . 7
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ๐
โ Fin) |
8 | | ovex 7394 |
. . . . . . 7
โข
(1...๐) โ
V |
9 | | elmapg 8784 |
. . . . . . 7
โข ((๐
โ Fin โง (1...๐) โ V) โ ((๐น โพ (1...๐)) โ (๐
โm (1...๐)) โ (๐น โพ (1...๐)):(1...๐)โถ๐
)) |
10 | 7, 8, 9 | sylancl 587 |
. . . . . 6
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ((๐น โพ (1...๐)) โ (๐
โm (1...๐)) โ (๐น โพ (1...๐)):(1...๐)โถ๐
)) |
11 | 6, 10 | mpbird 257 |
. . . . 5
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ (๐น โพ (1...๐)) โ (๐
โm (1...๐))) |
12 | | cnveq 5833 |
. . . . . . . . . . 11
โข (๐ = (๐น โพ (1...๐)) โ โก๐ = โก(๐น โพ (1...๐))) |
13 | 12 | imaeq1d 6016 |
. . . . . . . . . 10
โข (๐ = (๐น โพ (1...๐)) โ (โก๐ โ {๐}) = (โก(๐น โพ (1...๐)) โ {๐})) |
14 | 13 | eleq2d 2820 |
. . . . . . . . 9
โข (๐ = (๐น โพ (1...๐)) โ ((๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ (๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
15 | 14 | ralbidv 3171 |
. . . . . . . 8
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
16 | 15 | 2rexbidv 3210 |
. . . . . . 7
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
17 | 16 | rexbidv 3172 |
. . . . . 6
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
18 | 17 | rspcv 3579 |
. . . . 5
โข ((๐น โพ (1...๐)) โ (๐
โm (1...๐)) โ (โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
19 | 11, 18 | syl 17 |
. . . 4
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ
(โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
20 | | resss 5966 |
. . . . . . . . . 10
โข (๐น โพ (1...๐)) โ ๐น |
21 | | cnvss 5832 |
. . . . . . . . . 10
โข ((๐น โพ (1...๐)) โ ๐น โ โก(๐น โพ (1...๐)) โ โก๐น) |
22 | | imass1 6057 |
. . . . . . . . . 10
โข (โก(๐น โพ (1...๐)) โ โก๐น โ (โก(๐น โพ (1...๐)) โ {๐}) โ (โก๐น โ {๐})) |
23 | 20, 21, 22 | mp2b 10 |
. . . . . . . . 9
โข (โก(๐น โพ (1...๐)) โ {๐}) โ (โก๐น โ {๐}) |
24 | 23 | sseli 3944 |
. . . . . . . 8
โข ((๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}) โ (๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
25 | 24 | ralimi 3083 |
. . . . . . 7
โข
(โ๐ โ
(0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}) โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
26 | 25 | reximi 3084 |
. . . . . 6
โข
(โ๐ โ
โ โ๐ โ
(0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}) โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
27 | 26 | reximi 3084 |
. . . . 5
โข
(โ๐ โ
โ โ๐ โ
โ โ๐ โ
(0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
28 | 27 | reximi 3084 |
. . . 4
โข
(โ๐ โ
๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
29 | 19, 28 | syl6 35 |
. . 3
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ
(โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
30 | 29 | rexlimdva 3149 |
. 2
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
(โ๐ โ โ
โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
31 | 2, 30 | mpd 15 |
1
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |