Step | Hyp | Ref
| Expression |
1 | | smfinfdmmbllem.1 |
. . 3
β’
β²ππ |
2 | | smfinfdmmbllem.2 |
. . 3
β’
β²π₯π |
3 | | smfinfdmmbllem.3 |
. . 3
β’
β²ππ |
4 | | smfinfdmmbllem.4 |
. . 3
β’
β²π₯πΉ |
5 | | smfinfdmmbllem.7 |
. . . . . 6
β’ (π β π β SAlg) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β SAlg) |
7 | | smfinfdmmbllem.8 |
. . . . . 6
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
8 | 7 | ffvelcdmda 7082 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
9 | | eqid 2733 |
. . . . 5
β’ dom
(πΉβπ) = dom (πΉβπ) |
10 | 6, 8, 9 | smff 45383 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
11 | 10 | frexr 44030 |
. . 3
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) |
12 | | smfinfdmmbllem.10 |
. . 3
β’ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} |
13 | | smfinfdmmbllem.11 |
. . 3
β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
14 | | smfinfdmmbllem.12 |
. . 3
β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) |
15 | 1, 2, 3, 4, 11, 12, 13, 14 | finfdm2 45498 |
. 2
β’ (π β dom πΊ = βͺ π β β β© π β π ((π»βπ)βπ)) |
16 | | nfcv 2904 |
. . 3
β’
β²ππ |
17 | | nfcv 2904 |
. . 3
β’
β²πβ |
18 | | nnct 13942 |
. . . 4
β’ β
βΌ Ο |
19 | 18 | a1i 11 |
. . 3
β’ (π β β βΌ
Ο) |
20 | | nfv 1918 |
. . . . 5
β’
β²π π β β |
21 | 1, 20 | nfan 1903 |
. . . 4
β’
β²π(π β§ π β β) |
22 | | nfcv 2904 |
. . . 4
β’
β²ππ |
23 | | nfcv 2904 |
. . . 4
β’
β²ππ |
24 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β π β SAlg) |
25 | | smfinfdmmbllem.6 |
. . . . . 6
β’ π =
(β€β₯βπ) |
26 | 25 | uzct 43683 |
. . . . 5
β’ π βΌ
Ο |
27 | 26 | a1i 11 |
. . . 4
β’ ((π β§ π β β) β π βΌ Ο) |
28 | | smfinfdmmbllem.5 |
. . . . . 6
β’ (π β π β β€) |
29 | 28, 25 | uzn0d 44070 |
. . . . 5
β’ (π β π β β
) |
30 | 29 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β π β β
) |
31 | 24 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β π β SAlg) |
32 | | smfinfdmmbllem.9 |
. . . . . . 7
β’ ((π β§ π β π) β dom (πΉβπ) β π) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β dom (πΉβπ) β π) |
34 | 31, 33 | salrestss 45012 |
. . . . 5
β’ (((π β§ π β β) β§ π β π) β (π βΎt dom (πΉβπ)) β π) |
35 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β π |
36 | 3, 35 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π β§ π β π) |
37 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯π |
38 | 4, 37 | nffv 6898 |
. . . . . . . . . . 11
β’
β²π₯(πΉβπ) |
39 | 8 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
40 | | nnre 12215 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
41 | 40 | renegcld 11637 |
. . . . . . . . . . . . 13
β’ (π β β β -π β
β) |
42 | 41 | rexrd 11260 |
. . . . . . . . . . . 12
β’ (π β β β -π β
β*) |
43 | 42 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β -π β β*) |
44 | 38, 31, 39, 9, 43 | smfpimgtxr 45431 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)} β (π βΎt dom (πΉβπ))) |
45 | 44 | an32s 651 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β) β {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)} β (π βΎt dom (πΉβπ))) |
46 | 36, 45 | fmptd2f 43871 |
. . . . . . . 8
β’ ((π β§ π β π) β (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)}):ββΆ(π βΎt dom (πΉβπ))) |
47 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
48 | | nnex 12214 |
. . . . . . . . . . 11
β’ β
β V |
49 | 48 | mptex 7220 |
. . . . . . . . . 10
β’ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)}) β V |
50 | 14 | fvmpt2 7005 |
. . . . . . . . . 10
β’ ((π β π β§ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)}) β V) β (π»βπ) = (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) |
51 | 47, 49, 50 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π»βπ) = (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) |
52 | 51 | feq1d 6699 |
. . . . . . . 8
β’ ((π β§ π β π) β ((π»βπ):ββΆ(π βΎt dom (πΉβπ)) β (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)}):ββΆ(π βΎt dom (πΉβπ)))) |
53 | 46, 52 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π β π) β (π»βπ):ββΆ(π βΎt dom (πΉβπ))) |
54 | 53 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β (π»βπ):ββΆ(π βΎt dom (πΉβπ))) |
55 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β π β β) |
56 | 54, 55 | ffvelcdmd 7083 |
. . . . 5
β’ (((π β§ π β β) β§ π β π) β ((π»βπ)βπ) β (π βΎt dom (πΉβπ))) |
57 | 34, 56 | sseldd 3982 |
. . . 4
β’ (((π β§ π β β) β§ π β π) β ((π»βπ)βπ) β π) |
58 | 21, 22, 23, 24, 27, 30, 57 | saliinclf 44977 |
. . 3
β’ ((π β§ π β β) β β© π β π ((π»βπ)βπ) β π) |
59 | 3, 16, 17, 5, 19, 58 | saliunclf 44973 |
. 2
β’ (π β βͺ π β β β© π β π ((π»βπ)βπ) β π) |
60 | 15, 59 | eqeltrd 2834 |
1
β’ (π β dom πΊ β π) |