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