Step | Hyp | Ref
| Expression |
1 | | vdw 16926 |
. . 3
โข ((๐
โ Fin โง ๐พ โ โ0)
โ โ๐ โ
โ โ๐ โ
(๐
โm
(1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐})) |
2 | 1 | 3adant2 1131 |
. 2
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
โ๐ โ โ
โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐})) |
3 | | simpl2 1192 |
. . . . . . 7
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ๐น:โโถ๐
) |
4 | | fz1ssnn 13531 |
. . . . . . 7
โข
(1...๐) โ
โ |
5 | | fssres 6757 |
. . . . . . 7
โข ((๐น:โโถ๐
โง (1...๐) โ โ) โ (๐น โพ (1...๐)):(1...๐)โถ๐
) |
6 | 3, 4, 5 | sylancl 586 |
. . . . . 6
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ (๐น โพ (1...๐)):(1...๐)โถ๐
) |
7 | | simpl1 1191 |
. . . . . . 7
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ๐
โ Fin) |
8 | | ovex 7441 |
. . . . . . 7
โข
(1...๐) โ
V |
9 | | elmapg 8832 |
. . . . . . 7
โข ((๐
โ Fin โง (1...๐) โ V) โ ((๐น โพ (1...๐)) โ (๐
โm (1...๐)) โ (๐น โพ (1...๐)):(1...๐)โถ๐
)) |
10 | 7, 8, 9 | sylancl 586 |
. . . . . 6
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ ((๐น โพ (1...๐)) โ (๐
โm (1...๐)) โ (๐น โพ (1...๐)):(1...๐)โถ๐
)) |
11 | 6, 10 | mpbird 256 |
. . . . 5
โข (((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โง ๐ โ โ) โ (๐น โพ (1...๐)) โ (๐
โm (1...๐))) |
12 | | cnveq 5873 |
. . . . . . . . . . 11
โข (๐ = (๐น โพ (1...๐)) โ โก๐ = โก(๐น โพ (1...๐))) |
13 | 12 | imaeq1d 6058 |
. . . . . . . . . 10
โข (๐ = (๐น โพ (1...๐)) โ (โก๐ โ {๐}) = (โก(๐น โพ (1...๐)) โ {๐})) |
14 | 13 | eleq2d 2819 |
. . . . . . . . 9
โข (๐ = (๐น โพ (1...๐)) โ ((๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ (๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
15 | 14 | ralbidv 3177 |
. . . . . . . 8
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
16 | 15 | 2rexbidv 3219 |
. . . . . . 7
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
17 | 16 | rexbidv 3178 |
. . . . . 6
โข (๐ = (๐น โพ (1...๐)) โ (โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก(๐น โพ (1...๐)) โ {๐}))) |
18 | 17 | rspcv 3608 |
. . . . 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 6006 |
. . . . . . . . . 10
โข (๐น โพ (1...๐)) โ ๐น |
21 | | cnvss 5872 |
. . . . . . . . . 10
โข ((๐น โพ (1...๐)) โ ๐น โ โก(๐น โพ (1...๐)) โ โก๐น) |
22 | | imass1 6100 |
. . . . . . . . . 10
โข (โก(๐น โพ (1...๐)) โ โก๐น โ (โก(๐น โพ (1...๐)) โ {๐}) โ (โก๐น โ {๐})) |
23 | 20, 21, 22 | mp2b 10 |
. . . . . . . . 9
โข (โก(๐น โพ (1...๐)) โ {๐}) โ (โก๐น โ {๐}) |
24 | 23 | sseli 3978 |
. . . . . . . 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 3155 |
. 2
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
(โ๐ โ โ
โ๐ โ (๐
โm (1...๐))โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐ โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
31 | 2, 30 | mpd 15 |
1
โข ((๐
โ Fin โง ๐น:โโถ๐
โง ๐พ โ โ0) โ
โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |