Step | Hyp | Ref
| Expression |
1 | | icomnfordt 23094 |
. . . . . 6
β’
(-β[,)π)
β (ordTopβ β€ ) |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β (-β[,)π) β (ordTopβ β€
)) |
3 | | xlimmnfvlem1.c |
. . . . . . . 8
β’ (π β πΉ~~>*-β) |
4 | | df-xlim 45120 |
. . . . . . . . 9
β’ ~~>* =
(βπ‘β(ordTopβ β€ )) |
5 | 4 | breqi 5148 |
. . . . . . . 8
β’ (πΉ~~>*-β β πΉ(βπ‘β(ordTopβ
β€ ))-β) |
6 | 3, 5 | sylib 217 |
. . . . . . 7
β’ (π β πΉ(βπ‘β(ordTopβ
β€ ))-β) |
7 | | nfcv 2898 |
. . . . . . . 8
β’
β²ππΉ |
8 | | letopon 23083 |
. . . . . . . . 9
β’
(ordTopβ β€ ) β
(TopOnββ*) |
9 | 8 | a1i 11 |
. . . . . . . 8
β’ (π β (ordTopβ β€ )
β (TopOnββ*)) |
10 | 7, 9 | lmbr3 45048 |
. . . . . . 7
β’ (π β (πΉ(βπ‘β(ordTopβ
β€ ))-β β (πΉ β
(β* βpm β) β§ -β β
β* β§ βπ’ β (ordTopβ β€ )(-β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
11 | 6, 10 | mpbid 231 |
. . . . . 6
β’ (π β (πΉ β (β*
βpm β) β§ -β β β* β§
βπ’ β
(ordTopβ β€ )(-β β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
12 | 11 | simp3d 1142 |
. . . . 5
β’ (π β βπ’ β (ordTopβ β€ )(-β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
13 | 2, 12 | jca 511 |
. . . 4
β’ (π β ((-β[,)π) β (ordTopβ β€ )
β§ βπ’ β
(ordTopβ β€ )(-β β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
14 | 11 | simp2d 1141 |
. . . . 5
β’ (π β -β β
β*) |
15 | | xlimmnfvlem1.x |
. . . . . 6
β’ (π β π β β) |
16 | 15 | rexrd 11280 |
. . . . 5
β’ (π β π β
β*) |
17 | 15 | mnfltd 13122 |
. . . . 5
β’ (π β -β < π) |
18 | | lbico1 13396 |
. . . . 5
β’
((-β β β* β§ π β β* β§ -β
< π) β -β
β (-β[,)π)) |
19 | 14, 16, 17, 18 | syl3anc 1369 |
. . . 4
β’ (π β -β β
(-β[,)π)) |
20 | | eleq2 2817 |
. . . . . 6
β’ (π’ = (-β[,)π) β (-β β π’ β -β β (-β[,)π))) |
21 | | eleq2 2817 |
. . . . . . . . 9
β’ (π’ = (-β[,)π) β ((πΉβπ) β π’ β (πΉβπ) β (-β[,)π))) |
22 | 21 | anbi2d 628 |
. . . . . . . 8
β’ (π’ = (-β[,)π) β ((π β dom πΉ β§ (πΉβπ) β π’) β (π β dom πΉ β§ (πΉβπ) β (-β[,)π)))) |
23 | 22 | ralbidv 3172 |
. . . . . . 7
β’ (π’ = (-β[,)π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)))) |
24 | 23 | rexbidv 3173 |
. . . . . 6
β’ (π’ = (-β[,)π) β (βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)))) |
25 | 20, 24 | imbi12d 344 |
. . . . 5
β’ (π’ = (-β[,)π) β ((-β β π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (-β β (-β[,)π) β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π))))) |
26 | 25 | rspcva 3605 |
. . . 4
β’
(((-β[,)π)
β (ordTopβ β€ ) β§ βπ’ β (ordTopβ β€ )(-β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (-β β (-β[,)π) β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)))) |
27 | 13, 19, 26 | sylc 65 |
. . 3
β’ (π β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π))) |
28 | | nfv 1910 |
. . . 4
β’
β²ππ |
29 | | nfv 1910 |
. . . . . 6
β’
β²ππ |
30 | | xlimmnfvlem1.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ*) |
31 | 30 | ffdmd 6748 |
. . . . . . . . . . 11
β’ (π β πΉ:dom πΉβΆβ*) |
32 | 31 | ffvelcdmda 7088 |
. . . . . . . . . 10
β’ ((π β§ π β dom πΉ) β (πΉβπ) β
β*) |
33 | 32 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β (πΉβπ) β
β*) |
34 | 16 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β π β
β*) |
35 | 14 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β -β β
β*) |
36 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β (πΉβπ) β (-β[,)π)) |
37 | 35, 34, 36 | icoltubd 44843 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β (πΉβπ) < π) |
38 | 33, 34, 37 | xrltled 13147 |
. . . . . . . 8
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (-β[,)π))) β (πΉβπ) β€ π) |
39 | 38 | ex 412 |
. . . . . . 7
β’ (π β ((π β dom πΉ β§ (πΉβπ) β (-β[,)π)) β (πΉβπ) β€ π)) |
40 | 39 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β (-β[,)π)) β (πΉβπ) β€ π)) |
41 | 29, 40 | ralimdaa 3252 |
. . . . 5
β’ (π β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)) β βπ β (β€β₯βπ)(πΉβπ) β€ π)) |
42 | 41 | a1d 25 |
. . . 4
β’ (π β (π β β€ β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)) β βπ β (β€β₯βπ)(πΉβπ) β€ π))) |
43 | 28, 42 | reximdai 3253 |
. . 3
β’ (π β (βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (-β[,)π)) β βπ β β€ βπ β (β€β₯βπ)(πΉβπ) β€ π)) |
44 | 27, 43 | mpd 15 |
. 2
β’ (π β βπ β β€ βπ β (β€β₯βπ)(πΉβπ) β€ π) |
45 | | xlimmnfvlem1.m |
. . 3
β’ (π β π β β€) |
46 | | xlimmnfvlem1.z |
. . . 4
β’ π =
(β€β₯βπ) |
47 | 46 | rexuz3 15313 |
. . 3
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π β βπ β β€ βπ β (β€β₯βπ)(πΉβπ) β€ π)) |
48 | 45, 47 | syl 17 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π β βπ β β€ βπ β (β€β₯βπ)(πΉβπ) β€ π)) |
49 | 44, 48 | mpbird 257 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π) |