Step | Hyp | Ref
| Expression |
1 | | xrge0tsmsd.s |
. . . . 5
β’ (π β π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
2 | | iccssxr 13276 |
. . . . . . . . 9
β’
(0[,]+β) β β* |
3 | | xrge0tsmsd.g |
. . . . . . . . . . . 12
β’ πΊ =
(β*π βΎs
(0[,]+β)) |
4 | | xrsbas 20736 |
. . . . . . . . . . . 12
β’
β* =
(Baseββ*π ) |
5 | 3, 4 | ressbas2 17055 |
. . . . . . . . . . 11
β’
((0[,]+β) β β* β (0[,]+β) =
(BaseβπΊ)) |
6 | 2, 5 | ax-mp 5 |
. . . . . . . . . 10
β’
(0[,]+β) = (BaseβπΊ) |
7 | | eqid 2738 |
. . . . . . . . . 10
β’
(0gβπΊ) = (0gβπΊ) |
8 | | xrge0cmn 20762 |
. . . . . . . . . . . 12
β’
(β*π βΎs
(0[,]+β)) β CMnd |
9 | 3, 8 | eqeltri 2835 |
. . . . . . . . . . 11
β’ πΊ β CMnd |
10 | 9 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (π« π΄ β© Fin)) β πΊ β CMnd) |
11 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (π« π΄ β© Fin)) β π β (π« π΄ β© Fin)) |
12 | | xrge0tsmsd.f |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆ(0[,]+β)) |
13 | | elfpw 9232 |
. . . . . . . . . . . 12
β’ (π β (π« π΄ β© Fin) β (π β π΄ β§ π β Fin)) |
14 | 13 | simplbi 499 |
. . . . . . . . . . 11
β’ (π β (π« π΄ β© Fin) β π β π΄) |
15 | | fssres 6704 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆ(0[,]+β) β§ π β π΄) β (πΉ βΎ π ):π βΆ(0[,]+β)) |
16 | 12, 14, 15 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΉ βΎ π ):π βΆ(0[,]+β)) |
17 | | elinel2 4155 |
. . . . . . . . . . . 12
β’ (π β (π« π΄ β© Fin) β π β Fin) |
18 | 17 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (π« π΄ β© Fin)) β π β Fin) |
19 | | fvexd 6853 |
. . . . . . . . . . 11
β’ ((π β§ π β (π« π΄ β© Fin)) β
(0gβπΊ)
β V) |
20 | 16, 18, 19 | fdmfifsupp 9249 |
. . . . . . . . . 10
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΉ βΎ π ) finSupp (0gβπΊ)) |
21 | 6, 7, 10, 11, 16, 20 | gsumcl 19621 |
. . . . . . . . 9
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π )) β (0[,]+β)) |
22 | 2, 21 | sselid 3941 |
. . . . . . . 8
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π )) β
β*) |
23 | 22 | fmpttd 7058 |
. . . . . . 7
β’ (π β (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))):(π« π΄ β©
Fin)βΆβ*) |
24 | 23 | frnd 6672 |
. . . . . 6
β’ (π β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) β
β*) |
25 | | supxrcl 13163 |
. . . . . 6
β’ (ran
(π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) β β*
β sup(ran (π β
(π« π΄ β© Fin)
β¦ (πΊ
Ξ£g (πΉ βΎ π ))), β*, < ) β
β*) |
26 | 24, 25 | syl 17 |
. . . . 5
β’ (π β sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))), β*, < )
β β*) |
27 | 1, 26 | eqeltrd 2839 |
. . . 4
β’ (π β π β
β*) |
28 | | 0ss 4355 |
. . . . . . . 8
β’ β
β π΄ |
29 | | 0fin 9049 |
. . . . . . . 8
β’ β
β Fin |
30 | | elfpw 9232 |
. . . . . . . 8
β’ (β
β (π« π΄ β©
Fin) β (β
β π΄ β§ β
β Fin)) |
31 | 28, 29, 30 | mpbir2an 710 |
. . . . . . 7
β’ β
β (π« π΄ β©
Fin) |
32 | | 0cn 11081 |
. . . . . . 7
β’ 0 β
β |
33 | | eqid 2738 |
. . . . . . . 8
β’ (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) = (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) |
34 | | reseq2 5929 |
. . . . . . . . . . 11
β’ (π = β
β (πΉ βΎ π ) = (πΉ βΎ β
)) |
35 | | res0 5938 |
. . . . . . . . . . 11
β’ (πΉ βΎ β
) =
β
|
36 | 34, 35 | eqtrdi 2794 |
. . . . . . . . . 10
β’ (π = β
β (πΉ βΎ π ) = β
) |
37 | 36 | oveq2d 7366 |
. . . . . . . . 9
β’ (π = β
β (πΊ Ξ£g
(πΉ βΎ π )) = (πΊ Ξ£g
β
)) |
38 | | eqid 2738 |
. . . . . . . . . . . 12
β’
(β*π βΎs
(β* β {-β})) =
(β*π βΎs
(β* β {-β})) |
39 | 38 | xrge0subm 20761 |
. . . . . . . . . . 11
β’
(0[,]+β) β
(SubMndβ(β*π βΎs
(β* β {-β}))) |
40 | | xrex 12841 |
. . . . . . . . . . . . . . 15
β’
β* β V |
41 | | difexg 5283 |
. . . . . . . . . . . . . . 15
β’
(β* β V β (β* β
{-β}) β V) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
(β* β {-β}) β V |
43 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β*
β§ 0 β€ π₯) β
π₯ β
β*) |
44 | | ge0nemnf 13021 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β*
β§ 0 β€ π₯) β
π₯ β
-β) |
45 | 43, 44 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β*
β§ 0 β€ π₯) β
(π₯ β
β* β§ π₯
β -β)) |
46 | | elxrge0 13303 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (0[,]+β) β
(π₯ β
β* β§ 0 β€ π₯)) |
47 | | eldifsn 4746 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (β*
β {-β}) β (π₯ β β* β§ π₯ β
-β)) |
48 | 45, 46, 47 | 3imtr4i 292 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (0[,]+β) β
π₯ β
(β* β {-β})) |
49 | 48 | ssriv 3947 |
. . . . . . . . . . . . . 14
β’
(0[,]+β) β (β* β
{-β}) |
50 | | ressabs 17065 |
. . . . . . . . . . . . . 14
β’
(((β* β {-β}) β V β§ (0[,]+β)
β (β* β {-β})) β
((β*π βΎs
(β* β {-β})) βΎs (0[,]+β)) =
(β*π βΎs
(0[,]+β))) |
51 | 42, 49, 50 | mp2an 691 |
. . . . . . . . . . . . 13
β’
((β*π βΎs
(β* β {-β})) βΎs (0[,]+β)) =
(β*π βΎs
(0[,]+β)) |
52 | 3, 51 | eqtr4i 2769 |
. . . . . . . . . . . 12
β’ πΊ =
((β*π βΎs
(β* β {-β})) βΎs
(0[,]+β)) |
53 | 38 | xrs10 20759 |
. . . . . . . . . . . 12
β’ 0 =
(0gβ(β*π
βΎs (β* β {-β}))) |
54 | 52, 53 | subm0 18561 |
. . . . . . . . . . 11
β’
((0[,]+β) β
(SubMndβ(β*π βΎs
(β* β {-β}))) β 0 =
(0gβπΊ)) |
55 | 39, 54 | ax-mp 5 |
. . . . . . . . . 10
β’ 0 =
(0gβπΊ) |
56 | 55 | gsum0 18474 |
. . . . . . . . 9
β’ (πΊ Ξ£g
β
) = 0 |
57 | 37, 56 | eqtrdi 2794 |
. . . . . . . 8
β’ (π = β
β (πΊ Ξ£g
(πΉ βΎ π )) = 0) |
58 | 33, 57 | elrnmpt1s 5909 |
. . . . . . 7
β’ ((β
β (π« π΄ β©
Fin) β§ 0 β β) β 0 β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))) |
59 | 31, 32, 58 | mp2an 691 |
. . . . . 6
β’ 0 β
ran (π β (π«
π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) |
60 | | supxrub 13172 |
. . . . . 6
β’ ((ran
(π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) β β*
β§ 0 β ran (π
β (π« π΄ β©
Fin) β¦ (πΊ
Ξ£g (πΉ βΎ π )))) β 0 β€ sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))), β*, <
)) |
61 | 24, 59, 60 | sylancl 587 |
. . . . 5
β’ (π β 0 β€ sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))), β*, <
)) |
62 | 61, 1 | breqtrrd 5132 |
. . . 4
β’ (π β 0 β€ π) |
63 | | elxrge0 13303 |
. . . 4
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
64 | 27, 62, 63 | sylanbrc 584 |
. . 3
β’ (π β π β (0[,]+β)) |
65 | | letop 22479 |
. . . . . 6
β’
(ordTopβ β€ ) β Top |
66 | | ovex 7383 |
. . . . . 6
β’
(0[,]+β) β V |
67 | | elrest 17244 |
. . . . . 6
β’
(((ordTopβ β€ ) β Top β§ (0[,]+β) β V) β
(π’ β ((ordTopβ
β€ ) βΎt (0[,]+β)) β βπ£ β (ordTopβ β€ )π’ = (π£ β© (0[,]+β)))) |
68 | 65, 66, 67 | mp2an 691 |
. . . . 5
β’ (π’ β ((ordTopβ β€ )
βΎt (0[,]+β)) β βπ£ β (ordTopβ β€ )π’ = (π£ β© (0[,]+β))) |
69 | | elinel1 4154 |
. . . . . . . 8
β’ (π β (π£ β© (0[,]+β)) β π β π£) |
70 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β π£ β (ordTopβ β€
)) |
71 | | reex 11076 |
. . . . . . . . . . . . . . 15
β’ β
β V |
72 | | elrestr 17245 |
. . . . . . . . . . . . . . 15
β’
(((ordTopβ β€ ) β Top β§ β β V β§ π£ β (ordTopβ β€ ))
β (π£ β© β)
β ((ordTopβ β€ ) βΎt β)) |
73 | 65, 71, 72 | mp3an12 1452 |
. . . . . . . . . . . . . 14
β’ (π£ β (ordTopβ β€ )
β (π£ β© β)
β ((ordTopβ β€ ) βΎt β)) |
74 | 70, 73 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β (π£ β© β) β ((ordTopβ β€ )
βΎt β)) |
75 | | eqid 2738 |
. . . . . . . . . . . . . 14
β’
((ordTopβ β€ ) βΎt β) = ((ordTopβ
β€ ) βΎt β) |
76 | 75 | xrtgioo 24091 |
. . . . . . . . . . . . 13
β’
(topGenβran (,)) = ((ordTopβ β€ ) βΎt
β) |
77 | 74, 76 | eleqtrrdi 2850 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β (π£ β© β) β (topGenβran
(,))) |
78 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β π β π£) |
79 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β π β β) |
80 | 78, 79 | elind 4153 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β π β (π£ β© β)) |
81 | | tg2 22237 |
. . . . . . . . . . . 12
β’ (((π£ β© β) β
(topGenβran (,)) β§ π β (π£ β© β)) β βπ’ β ran (,)(π β π’ β§ π’ β (π£ β© β))) |
82 | 77, 80, 81 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β βπ’ β ran (,)(π β π’ β§ π’ β (π£ β© β))) |
83 | | ioof 13293 |
. . . . . . . . . . . . . 14
β’
(,):(β* Γ β*)βΆπ«
β |
84 | | ffn 6664 |
. . . . . . . . . . . . . 14
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
85 | | ovelrn 7523 |
. . . . . . . . . . . . . 14
β’ ((,) Fn
(β* Γ β*) β (π’ β ran (,) β βπ β β*
βπ€ β
β* π’ =
(π(,)π€))) |
86 | 83, 84, 85 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (π’ β ran (,) β
βπ β
β* βπ€ β β* π’ = (π(,)π€)) |
87 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β (π(,)π€) β (π£ β© β)) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (π(,)π€) β (π£ β© β)) |
89 | | inss1 4187 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π£ β© β) β π£ |
90 | 88, 89 | sstrdi 3955 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (π(,)π€) β π£) |
91 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β πΊ β CMnd) |
92 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π¦ β (π« π΄ β© Fin)) |
93 | | elinel2 4155 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β (π« π΄ β© Fin) β π¦ β Fin) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π¦ β Fin) |
95 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π) |
96 | 95, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β πΉ:π΄βΆ(0[,]+β)) |
97 | | elfpw 9232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β (π« π΄ β© Fin) β (π¦ β π΄ β§ π¦ β Fin)) |
98 | 97 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β (π« π΄ β© Fin) β π¦ β π΄) |
99 | 92, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π¦ β π΄) |
100 | 96, 99 | fssresd 6705 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΉ βΎ π¦):π¦βΆ(0[,]+β)) |
101 | 12 | ffund 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β Fun πΉ) |
102 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β Fun πΉ) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β Fun πΉ) |
104 | | c0ex 11083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
V |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β 0 β V) |
106 | 103, 94, 105 | resfifsupp 9267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΉ βΎ π¦) finSupp 0) |
107 | 6, 55, 91, 94, 100, 106 | gsumcl 19621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β (0[,]+β)) |
108 | 2, 107 | sselid 3941 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β
β*) |
109 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π β β*) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π β β*) |
111 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π§ β (π« π΄ β© Fin)) |
112 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π§ β π¦) |
113 | 112, 99 | sstrd 3953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π§ β π΄) |
114 | 96, 113 | fssresd 6705 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΉ βΎ π§):π§βΆ(0[,]+β)) |
115 | | ssfi 9051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π¦ β Fin β§ π§ β π¦) β π§ β Fin) |
116 | 94, 112, 115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π§ β Fin) |
117 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (0gβπΊ) β V) |
118 | 114, 116,
117 | fdmfifsupp 9249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΉ βΎ π§) finSupp (0gβπΊ)) |
119 | 6, 7, 91, 111, 114, 118 | gsumcl 19621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π§)) β (0[,]+β)) |
120 | 2, 119 | sselid 3941 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π§)) β
β*) |
121 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π < (πΊ Ξ£g (πΉ βΎ π§))) |
122 | | xrge0tsmsd.a |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π΄ β π) |
123 | 95, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π΄ β π) |
124 | 3, 123, 96, 92, 112 | xrge0gsumle 24118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π§)) β€ (πΊ Ξ£g (πΉ βΎ π¦))) |
125 | 110, 120,
108, 121, 124 | xrltletrd 13009 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π < (πΊ Ξ£g (πΉ βΎ π¦))) |
126 | 95, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π β
β*) |
127 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π€ β β*) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π€ β β*) |
129 | 95, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) β
β*) |
130 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΊ Ξ£g
(πΉ βΎ π¦)) β V |
131 | | reseq2 5929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π¦ β (πΉ βΎ π ) = (πΉ βΎ π¦)) |
132 | 131 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π¦ β (πΊ Ξ£g (πΉ βΎ π )) = (πΊ Ξ£g (πΉ βΎ π¦))) |
133 | 33, 132 | elrnmpt1s 5909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β (π« π΄ β© Fin) β§ (πΊ Ξ£g
(πΉ βΎ π¦)) β V) β (πΊ Ξ£g
(πΉ βΎ π¦)) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))) |
134 | 92, 130, 133 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))) |
135 | | supxrub 13172 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((ran
(π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) β β*
β§ (πΊ
Ξ£g (πΉ βΎ π¦)) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))) β (πΊ Ξ£g (πΉ βΎ π¦)) β€ sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
136 | 129, 134,
135 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β€ sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
137 | 95, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
138 | 136, 137 | breqtrrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β€ π) |
139 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π β (π(,)π€)) |
140 | | eliooord 13252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π(,)π€) β (π < π β§ π < π€)) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β (π < π β§ π < π€)) |
142 | 141 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π < π€) |
143 | 142 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β π < π€) |
144 | 108, 126,
128, 138, 143 | xrlelttrd 13008 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) < π€) |
145 | | elioo1 13233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β*
β§ π€ β
β*) β ((πΊ Ξ£g (πΉ βΎ π¦)) β (π(,)π€) β ((πΊ Ξ£g (πΉ βΎ π¦)) β β* β§ π < (πΊ Ξ£g (πΉ βΎ π¦)) β§ (πΊ Ξ£g (πΉ βΎ π¦)) < π€))) |
146 | 110, 128,
145 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β ((πΊ Ξ£g (πΉ βΎ π¦)) β (π(,)π€) β ((πΊ Ξ£g (πΉ βΎ π¦)) β β* β§ π < (πΊ Ξ£g (πΉ βΎ π¦)) β§ (πΊ Ξ£g (πΉ βΎ π¦)) < π€))) |
147 | 108, 125,
144, 146 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β (π(,)π€)) |
148 | 90, 147 | sseldd 3944 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β π£) |
149 | 148, 107 | elind 4153 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ ((π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦))) β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))) |
150 | 149 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))) |
151 | 150 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ π¦ β (π« π΄ β© Fin)) β (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
152 | 151 | ralrimiva 3142 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
153 | 141 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π < π) |
154 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
155 | 153, 154 | breqtrd 5130 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β π < sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
156 | 24 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) β
β*) |
157 | | supxrlub 13173 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((ran
(π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) β β*
β§ π β
β*) β (π < sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, < ) β
βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))π < π€)) |
158 | 156, 109,
157 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β (π < sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, < ) β
βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))π < π€)) |
159 | 155, 158 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))π < π€) |
160 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΊ Ξ£g
(πΉ βΎ π§)) β V |
161 | 160 | rgenw 3067 |
. . . . . . . . . . . . . . . . . . 19
β’
βπ§ β
(π« π΄ β©
Fin)(πΊ
Ξ£g (πΉ βΎ π§)) β V |
162 | | reseq2 5929 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π§ β (πΉ βΎ π ) = (πΉ βΎ π§)) |
163 | 162 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π§ β (πΊ Ξ£g (πΉ βΎ π )) = (πΊ Ξ£g (πΉ βΎ π§))) |
164 | 163 | cbvmptv 5217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) = (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))) |
165 | | breq2 5108 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = (πΊ Ξ£g (πΉ βΎ π§)) β (π < π€ β π < (πΊ Ξ£g (πΉ βΎ π§)))) |
166 | 164, 165 | rexrnmptw 7040 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ§ β
(π« π΄ β©
Fin)(πΊ
Ξ£g (πΉ βΎ π§)) β V β (βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))π < π€ β βπ§ β (π« π΄ β© Fin)π < (πΊ Ξ£g (πΉ βΎ π§)))) |
167 | 161, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ€ β ran
(π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))π < π€ β βπ§ β (π« π΄ β© Fin)π < (πΊ Ξ£g (πΉ βΎ π§))) |
168 | 159, 167 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β βπ§ β (π« π΄ β© Fin)π < (πΊ Ξ£g (πΉ βΎ π§))) |
169 | 152, 168 | reximddv 3167 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ ((π β β* β§ π€ β β*)
β§ (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
170 | 169 | expr 458 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ (π β β* β§ π€ β β*))
β ((π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
171 | | eleq2 2827 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = (π(,)π€) β (π β π’ β π β (π(,)π€))) |
172 | | sseq1 3968 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = (π(,)π€) β (π’ β (π£ β© β) β (π(,)π€) β (π£ β© β))) |
173 | 171, 172 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π’ = (π(,)π€) β ((π β π’ β§ π’ β (π£ β© β)) β (π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)))) |
174 | 173 | imbi1d 342 |
. . . . . . . . . . . . . . 15
β’ (π’ = (π(,)π€) β (((π β π’ β§ π’ β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) β ((π β (π(,)π€) β§ (π(,)π€) β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))))) |
175 | 170, 174 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β§ (π β β* β§ π€ β β*))
β (π’ = (π(,)π€) β ((π β π’ β§ π’ β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))))) |
176 | 175 | rexlimdvva 3204 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β (βπ β β*
βπ€ β
β* π’ =
(π(,)π€) β ((π β π’ β§ π’ β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))))) |
177 | 86, 176 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β (π’ β ran (,) β ((π β π’ β§ π’ β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))))) |
178 | 177 | rexlimdv 3149 |
. . . . . . . . . . 11
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β (βπ’ β ran (,)(π β π’ β§ π’ β (π£ β© β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
179 | 82, 178 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π β β) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
180 | | simplrl 776 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β π£ β (ordTopβ β€
)) |
181 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β π = +β) |
182 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β π β π£) |
183 | 181, 182 | eqeltrrd 2840 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β +β β π£) |
184 | | pnfnei 22493 |
. . . . . . . . . . . 12
β’ ((π£ β (ordTopβ β€ )
β§ +β β π£)
β βπ β
β (π(,]+β)
β π£) |
185 | 180, 183,
184 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β βπ β β (π(,]+β) β π£) |
186 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β (π(,]+β) β π£) |
187 | 186 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (π(,]+β) β π£) |
188 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β πΊ β CMnd) |
189 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π¦ β (π« π΄ β© Fin)) |
190 | | simp-5l 784 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π) |
191 | 190, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β πΉ:π΄βΆ(0[,]+β)) |
192 | 98 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π¦ β π΄) |
193 | 191, 192 | fssresd 6705 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΉ βΎ π¦):π¦βΆ(0[,]+β)) |
194 | 93 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π¦ β Fin) |
195 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (0gβπΊ) β V) |
196 | 193, 194,
195 | fdmfifsupp 9249 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΉ βΎ π¦) finSupp (0gβπΊ)) |
197 | 6, 7, 188, 189, 193, 196 | gsumcl 19621 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β (0[,]+β)) |
198 | 2, 197 | sselid 3941 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β
β*) |
199 | | rexr 11135 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β*) |
200 | 199 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π β β*) |
201 | 200 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π β β*) |
202 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π§ β (π« π΄ β© Fin)) |
203 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π§ β π¦) |
204 | 203, 192 | sstrd 3953 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π§ β π΄) |
205 | 191, 204 | fssresd 6705 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΉ βΎ π§):π§βΆ(0[,]+β)) |
206 | 194, 203,
115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π§ β Fin) |
207 | 205, 206,
195 | fdmfifsupp 9249 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΉ βΎ π§) finSupp (0gβπΊ)) |
208 | 6, 7, 188, 202, 205, 207 | gsumcl 19621 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π§)) β (0[,]+β)) |
209 | 2, 208 | sselid 3941 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π§)) β
β*) |
210 | | simplrr 777 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π < (πΊ Ξ£g (πΉ βΎ π§))) |
211 | 190, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π΄ β π) |
212 | 3, 211, 191, 189, 203 | xrge0gsumle 24118 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π§)) β€ (πΊ Ξ£g (πΉ βΎ π¦))) |
213 | 201, 209,
198, 210, 212 | xrltletrd 13009 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β π < (πΊ Ξ£g (πΉ βΎ π¦))) |
214 | | pnfge 12980 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ Ξ£g
(πΉ βΎ π¦)) β β*
β (πΊ
Ξ£g (πΉ βΎ π¦)) β€ +β) |
215 | 198, 214 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β€ +β) |
216 | | pnfxr 11143 |
. . . . . . . . . . . . . . . . . 18
β’ +β
β β* |
217 | | elioc1 13235 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β*
β§ +β β β*) β ((πΊ Ξ£g (πΉ βΎ π¦)) β (π(,]+β) β ((πΊ Ξ£g (πΉ βΎ π¦)) β β* β§ π < (πΊ Ξ£g (πΉ βΎ π¦)) β§ (πΊ Ξ£g (πΉ βΎ π¦)) β€ +β))) |
218 | 201, 216,
217 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β ((πΊ Ξ£g (πΉ βΎ π¦)) β (π(,]+β) β ((πΊ Ξ£g (πΉ βΎ π¦)) β β* β§ π < (πΊ Ξ£g (πΉ βΎ π¦)) β§ (πΊ Ξ£g (πΉ βΎ π¦)) β€ +β))) |
219 | 198, 213,
215, 218 | mpbir3and 1343 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β (π(,]+β)) |
220 | 187, 219 | sseldd 3944 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β π£) |
221 | 220, 197 | elind 4153 |
. . . . . . . . . . . . . 14
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ (π¦ β (π« π΄ β© Fin) β§ π§ β π¦)) β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))) |
222 | 221 | expr 458 |
. . . . . . . . . . . . 13
β’
((((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β§ π¦ β (π« π΄ β© Fin)) β (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
223 | 222 | ralrimiva 3142 |
. . . . . . . . . . . 12
β’
(((((π β§ (π£ β (ordTopβ β€ )
β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β§ (π§ β (π« π΄ β© Fin) β§ π < (πΊ Ξ£g (πΉ βΎ π§)))) β βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
224 | | ltpnf 12970 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π < +β) |
225 | 224 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π < +β) |
226 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π = +β) |
227 | 225, 226 | breqtrrd 5132 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π < π) |
228 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
229 | 227, 228 | breqtrd 5130 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β π < sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, <
)) |
230 | 24 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) β
β*) |
231 | 230, 200,
157 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β (π < sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, < ) β
βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))π < π€)) |
232 | 229, 231 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β βπ€ β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))π < π€) |
233 | 232, 167 | sylib 217 |
. . . . . . . . . . . 12
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β βπ§ β (π« π΄ β© Fin)π < (πΊ Ξ£g (πΉ βΎ π§))) |
234 | 223, 233 | reximddv 3167 |
. . . . . . . . . . 11
β’ ((((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β§ (π β β β§ (π(,]+β) β π£)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
235 | 185, 234 | rexlimddv 3157 |
. . . . . . . . . 10
β’ (((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β§ π = +β) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
236 | | ge0nemnf 13021 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ 0 β€ π) β
π β
-β) |
237 | 27, 62, 236 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β π β -β) |
238 | 27, 237 | jca 513 |
. . . . . . . . . . . 12
β’ (π β (π β β* β§ π β
-β)) |
239 | 238 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β (π β β* β§ π β
-β)) |
240 | | xrnemnf 12967 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β -β)
β (π β β
β¨ π =
+β)) |
241 | 239, 240 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β (π β β β¨ π = +β)) |
242 | 179, 235,
241 | mpjaodan 958 |
. . . . . . . . 9
β’ ((π β§ (π£ β (ordTopβ β€ ) β§ π β π£)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
243 | 242 | expr 458 |
. . . . . . . 8
β’ ((π β§ π£ β (ordTopβ β€ )) β (π β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
244 | 69, 243 | syl5 34 |
. . . . . . 7
β’ ((π β§ π£ β (ordTopβ β€ )) β (π β (π£ β© (0[,]+β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
245 | | eleq2 2827 |
. . . . . . . 8
β’ (π’ = (π£ β© (0[,]+β)) β (π β π’ β π β (π£ β© (0[,]+β)))) |
246 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π’ = (π£ β© (0[,]+β)) β ((πΊ Ξ£g
(πΉ βΎ π¦)) β π’ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))) |
247 | 246 | imbi2d 341 |
. . . . . . . . 9
β’ (π’ = (π£ β© (0[,]+β)) β ((π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’) β (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
248 | 247 | rexralbidv 3213 |
. . . . . . . 8
β’ (π’ = (π£ β© (0[,]+β)) β (βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β))))) |
249 | 245, 248 | imbi12d 345 |
. . . . . . 7
β’ (π’ = (π£ β© (0[,]+β)) β ((π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) β (π β (π£ β© (0[,]+β)) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β (π£ β© (0[,]+β)))))) |
250 | 244, 249 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β§ π£ β (ordTopβ β€ )) β (π’ = (π£ β© (0[,]+β)) β (π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
251 | 250 | rexlimdva 3151 |
. . . . 5
β’ (π β (βπ£ β (ordTopβ β€ )π’ = (π£ β© (0[,]+β)) β (π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
252 | 68, 251 | biimtrid 241 |
. . . 4
β’ (π β (π’ β ((ordTopβ β€ )
βΎt (0[,]+β)) β (π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
253 | 252 | ralrimiv 3141 |
. . 3
β’ (π β βπ’ β ((ordTopβ β€ )
βΎt (0[,]+β))(π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))) |
254 | | xrstset 20739 |
. . . . . . 7
β’
(ordTopβ β€ ) =
(TopSetββ*π ) |
255 | 3, 254 | resstset 17181 |
. . . . . 6
β’
((0[,]+β) β V β (ordTopβ β€ ) =
(TopSetβπΊ)) |
256 | 66, 255 | ax-mp 5 |
. . . . 5
β’
(ordTopβ β€ ) = (TopSetβπΊ) |
257 | 6, 256 | topnval 17251 |
. . . 4
β’
((ordTopβ β€ ) βΎt (0[,]+β)) =
(TopOpenβπΊ) |
258 | | eqid 2738 |
. . . 4
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
259 | 9 | a1i 11 |
. . . 4
β’ (π β πΊ β CMnd) |
260 | | xrstps 22482 |
. . . . . . 7
β’
β*π β TopSp |
261 | | resstps 22460 |
. . . . . . 7
β’
((β*π β TopSp β§
(0[,]+β) β V) β (β*π
βΎs (0[,]+β)) β TopSp) |
262 | 260, 66, 261 | mp2an 691 |
. . . . . 6
β’
(β*π βΎs
(0[,]+β)) β TopSp |
263 | 3, 262 | eqeltri 2835 |
. . . . 5
β’ πΊ β TopSp |
264 | 263 | a1i 11 |
. . . 4
β’ (π β πΊ β TopSp) |
265 | 6, 257, 258, 259, 264, 122, 12 | eltsms 23406 |
. . 3
β’ (π β (π β (πΊ tsums πΉ) β (π β (0[,]+β) β§ βπ’ β ((ordTopβ β€ )
βΎt (0[,]+β))(π β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))))) |
266 | 64, 253, 265 | mpbir2and 712 |
. 2
β’ (π β π β (πΊ tsums πΉ)) |
267 | | letsr 18417 |
. . . . 5
β’ β€
β TosetRel |
268 | | ordthaus 22657 |
. . . . 5
β’ ( β€
β TosetRel β (ordTopβ β€ ) β Haus) |
269 | 267, 268 | mp1i 13 |
. . . 4
β’ (π β (ordTopβ β€ )
β Haus) |
270 | | resthaus 22641 |
. . . 4
β’
(((ordTopβ β€ ) β Haus β§ (0[,]+β) β V)
β ((ordTopβ β€ ) βΎt (0[,]+β)) β
Haus) |
271 | 269, 66, 270 | sylancl 587 |
. . 3
β’ (π β ((ordTopβ β€ )
βΎt (0[,]+β)) β Haus) |
272 | 6, 259, 264, 122, 12, 257, 271 | haustsms2 23410 |
. 2
β’ (π β (π β (πΊ tsums πΉ) β (πΊ tsums πΉ) = {π})) |
273 | 266, 272 | mpd 15 |
1
β’ (π β (πΊ tsums πΉ) = {π}) |