Step | Hyp | Ref
| Expression |
1 | | erdsze.n |
. . . 4
⢠(š ā š ā ā) |
2 | | erdsze.f |
. . . 4
⢠(š ā š¹:(1...š)ā1-1āā) |
3 | | erdszelem.k |
. . . 4
⢠š¾ = (š„ ā (1...š) ⦠sup((⯠ā {š¦ ā š« (1...š„) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š„ ā š¦)}), ā, < )) |
4 | 1, 2, 3 | erdszelem3 34712 |
. . 3
⢠(š“ ā (1...š) ā (š¾āš“) = sup((⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < )) |
5 | 4 | adantl 481 |
. 2
⢠((š ā§ š“ ā (1...š)) ā (š¾āš“) = sup((⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < )) |
6 | | snex 5424 |
. . . . . 6
⢠{š“} ā V |
7 | | hashf 14303 |
. . . . . . 7
ā¢
āÆ:Vā¶(ā0 āŖ {+ā}) |
8 | 7 | fdmi 6723 |
. . . . . 6
⢠dom
⯠= V |
9 | 6, 8 | eleqtrri 2826 |
. . . . 5
⢠{š“} ā dom
⯠|
10 | | erdszelem.o |
. . . . . 6
⢠š Or ā |
11 | 1, 2, 3, 10 | erdszelem4 34713 |
. . . . 5
⢠((š ā§ š“ ā (1...š)) ā {š“} ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) |
12 | | inelcm 4459 |
. . . . 5
⢠(({š“} ā dom ⯠ā§
{š“} ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā (dom ⯠⩠{š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
) |
13 | 9, 11, 12 | sylancr 586 |
. . . 4
⢠((š ā§ š“ ā (1...š)) ā (dom ⯠⩠{š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
) |
14 | | imadisj 6073 |
. . . . 5
⢠((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) = ā
ā (dom ⯠ā©
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) = ā
) |
15 | 14 | necon3bii 2987 |
. . . 4
⢠((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
ā (dom ⯠ā©
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
) |
16 | 13, 15 | sylibr 233 |
. . 3
⢠((š ā§ š“ ā (1...š)) ā (⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
) |
17 | | eqid 2726 |
. . . . . 6
⢠{š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)} = {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)} |
18 | 17 | erdszelem2 34711 |
. . . . 5
⢠((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā Fin ā§ (⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā) |
19 | 18 | simpli 483 |
. . . 4
⢠(āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā Fin |
20 | 18 | simpri 485 |
. . . . 5
⢠(āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā |
21 | | nnssre 12220 |
. . . . 5
⢠ā
ā ā |
22 | 20, 21 | sstri 3986 |
. . . 4
⢠(āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā |
23 | | ltso 11298 |
. . . . 5
⢠< Or
ā |
24 | | fisupcl 9466 |
. . . . 5
⢠(( <
Or ā ā§ ((⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā Fin ā§ (⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
ā§ (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā)) ā sup((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < ) ā (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)})) |
25 | 23, 24 | mpan 687 |
. . . 4
ā¢
(((⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā Fin ā§ (⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
ā§ (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā) ā sup((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < ) ā (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)})) |
26 | 19, 22, 25 | mp3an13 1448 |
. . 3
⢠((āÆ
ā {š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}) ā ā
ā sup((⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < ) ā (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)})) |
27 | 16, 26 | syl 17 |
. 2
⢠((š ā§ š“ ā (1...š)) ā sup((⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)}), ā, < ) ā (⯠ā
{š¦ ā š«
(1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)})) |
28 | 5, 27 | eqeltrd 2827 |
1
⢠((š ā§ š“ ā (1...š)) ā (š¾āš“) ā (⯠ā {š¦ ā š« (1...š“) ⣠((š¹ ā¾ š¦) Isom < , š (š¦, (š¹ ā š¦)) ā§ š“ ā š¦)})) |