Step | Hyp | Ref
| Expression |
1 | | smfsupxr.g |
. . . 4
β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, <
)) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, <
))) |
3 | | smfsupxr.d |
. . . . . 6
β’ π· = {π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π· = {π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
5 | | nfv 1918 |
. . . . . . . 8
β’
β²ππ |
6 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ₯ |
7 | | nfii1 4990 |
. . . . . . . . 9
β’
β²πβ© π β π dom (πΉβπ) |
8 | 6, 7 | nfel 2918 |
. . . . . . . 8
β’
β²π π₯ β β© π β π dom (πΉβπ) |
9 | 5, 8 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π₯ β β©
π β π dom (πΉβπ)) |
10 | | smfsupxr.m |
. . . . . . . . 9
β’ (π β π β β€) |
11 | | smfsupxr.z |
. . . . . . . . 9
β’ π =
(β€β₯βπ) |
12 | 10, 11 | uzn0d 43746 |
. . . . . . . 8
β’ (π β π β β
) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β π β β
) |
14 | | smfsupxr.s |
. . . . . . . . . . 11
β’ (π β π β SAlg) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β SAlg) |
16 | | smfsupxr.f |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
17 | 16 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’ dom
(πΉβπ) = dom (πΉβπ) |
19 | 15, 17, 18 | smff 45059 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
20 | 19 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
21 | | eliinid 43409 |
. . . . . . . . 9
β’ ((π₯ β β© π β π dom (πΉβπ) β§ π β π) β π₯ β dom (πΉβπ)) |
22 | 21 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β π₯ β dom (πΉβπ)) |
23 | 20, 22 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β ((πΉβπ)βπ₯) β β) |
24 | 9, 13, 23 | supxrre3rnmpt 43750 |
. . . . . 6
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β β βπ¦
β β βπ
β π ((πΉβπ)βπ₯) β€ π¦)) |
25 | 24 | rabbidva 3413 |
. . . . 5
β’ (π β {π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} = {π₯ β
β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦}) |
26 | 4, 25 | eqtrd 2773 |
. . . 4
β’ (π β π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦}) |
27 | | nfmpt1 5214 |
. . . . . . . . . . . 12
β’
β²π(π β π β¦ ((πΉβπ)βπ₯)) |
28 | 27 | nfrn 5908 |
. . . . . . . . . . 11
β’
β²πran
(π β π β¦ ((πΉβπ)βπ₯)) |
29 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²πβ* |
30 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π
< |
31 | 28, 29, 30 | nfsup 9392 |
. . . . . . . . . 10
β’
β²πsup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, <
) |
32 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²πβ |
33 | 31, 32 | nfel 2918 |
. . . . . . . . 9
β’
β²πsup(ran
(π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β |
34 | 33, 7 | nfrabw 3439 |
. . . . . . . 8
β’
β²π{π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
35 | 3, 34 | nfcxfr 2902 |
. . . . . . 7
β’
β²ππ· |
36 | 6, 35 | nfel 2918 |
. . . . . 6
β’
β²π π₯ β π· |
37 | 5, 36 | nfan 1903 |
. . . . 5
β’
β²π(π β§ π₯ β π·) |
38 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β π β β
) |
39 | 19 | adantlr 714 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
40 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯π |
41 | | smfsupxr.x |
. . . . . . . . . . . . . 14
β’
β²π₯πΉ |
42 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
43 | 41, 42 | nffv 6853 |
. . . . . . . . . . . . 13
β’
β²π₯(πΉβπ) |
44 | 43 | nfdm 5907 |
. . . . . . . . . . . 12
β’
β²π₯dom
(πΉβπ) |
45 | 40, 44 | nfiin 4986 |
. . . . . . . . . . 11
β’
β²π₯β© π β π dom (πΉβπ) |
46 | 45 | ssrab2f 43415 |
. . . . . . . . . 10
β’ {π₯ β β© π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β β© π β π dom (πΉβπ) |
47 | 3, 46 | eqsstri 3979 |
. . . . . . . . 9
β’ π· β β© π β π dom (πΉβπ) |
48 | | id 22 |
. . . . . . . . 9
β’ (π₯ β π· β π₯ β π·) |
49 | 47, 48 | sselid 3943 |
. . . . . . . 8
β’ (π₯ β π· β π₯ β β©
π β π dom (πΉβπ)) |
50 | 49, 21 | sylan 581 |
. . . . . . 7
β’ ((π₯ β π· β§ π β π) β π₯ β dom (πΉβπ)) |
51 | 50 | adantll 713 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β π) β π₯ β dom (πΉβπ)) |
52 | 39, 51 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ π β π) β ((πΉβπ)βπ₯) β β) |
53 | 48, 3 | eleqtrdi 2844 |
. . . . . . . 8
β’ (π₯ β π· β π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
54 | | rabidim2 43400 |
. . . . . . . 8
β’ (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β sup(ran (π
β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β) |
55 | 53, 54 | syl 17 |
. . . . . . 7
β’ (π₯ β π· β sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β) |
56 | 55 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β π·) β sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β) |
57 | 49 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β π₯ β β©
π β π dom (πΉβπ)) |
58 | 57, 24 | syldan 592 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β
β β βπ¦
β β βπ
β π ((πΉβπ)βπ₯) β€ π¦)) |
59 | 56, 58 | mpbid 231 |
. . . . 5
β’ ((π β§ π₯ β π·) β βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦) |
60 | 37, 38, 52, 59 | supxrrernmpt 43742 |
. . . 4
β’ ((π β§ π₯ β π·) β sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) = sup(ran
(π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
61 | 26, 60 | mpteq12dva 5195 |
. . 3
β’ (π β (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < )) = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ))) |
62 | 2, 61 | eqtrd 2773 |
. 2
β’ (π β πΊ = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ))) |
63 | | smfsupxr.n |
. . 3
β’
β²ππΉ |
64 | | eqid 2733 |
. . 3
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} |
65 | | eqid 2733 |
. . 3
β’ (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
66 | 63, 41, 10, 11, 14, 16, 64, 65 | smfsup 45141 |
. 2
β’ (π β (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β
(SMblFnβπ)) |
67 | 62, 66 | eqeltrd 2834 |
1
β’ (π β πΊ β (SMblFnβπ)) |