Step | Hyp | Ref
| Expression |
1 | | iocpnfordt 22582 |
. . . . . 6
β’ (π(,]+β) β
(ordTopβ β€ ) |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β (π(,]+β) β (ordTopβ β€
)) |
3 | | xlimpnfvlem1.c |
. . . . . . . 8
β’ (π β πΉ~~>*+β) |
4 | | df-xlim 44146 |
. . . . . . . . 9
β’ ~~>* =
(βπ‘β(ordTopβ β€ )) |
5 | 4 | breqi 5112 |
. . . . . . . 8
β’ (πΉ~~>*+β β πΉ(βπ‘β(ordTopβ
β€ ))+β) |
6 | 3, 5 | sylib 217 |
. . . . . . 7
β’ (π β πΉ(βπ‘β(ordTopβ
β€ ))+β) |
7 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππΉ |
8 | | letopon 22572 |
. . . . . . . . 9
β’
(ordTopβ β€ ) β
(TopOnββ*) |
9 | 8 | a1i 11 |
. . . . . . . 8
β’ (π β (ordTopβ β€ )
β (TopOnββ*)) |
10 | 7, 9 | lmbr3 44074 |
. . . . . . 7
β’ (π β (πΉ(βπ‘β(ordTopβ
β€ ))+β β (πΉ β
(β* βpm β) β§ +β β
β* β§ βπ’ β (ordTopβ β€ )(+β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
11 | 6, 10 | mpbid 231 |
. . . . . 6
β’ (π β (πΉ β (β*
βpm β) β§ +β β β* β§
βπ’ β
(ordTopβ β€ )(+β β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
12 | 11 | simp3d 1145 |
. . . . 5
β’ (π β βπ’ β (ordTopβ β€ )(+β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
13 | 2, 12 | jca 513 |
. . . 4
β’ (π β ((π(,]+β) β (ordTopβ β€ )
β§ βπ’ β
(ordTopβ β€ )(+β β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
14 | | xlimpnfvlem1.x |
. . . . . 6
β’ (π β π β β) |
15 | 14 | rexrd 11210 |
. . . . 5
β’ (π β π β
β*) |
16 | 11 | simp2d 1144 |
. . . . 5
β’ (π β +β β
β*) |
17 | 14 | ltpnfd 13047 |
. . . . 5
β’ (π β π < +β) |
18 | | ubioc1 13323 |
. . . . 5
β’ ((π β β*
β§ +β β β* β§ π < +β) β +β β
(π(,]+β)) |
19 | 15, 16, 17, 18 | syl3anc 1372 |
. . . 4
β’ (π β +β β (π(,]+β)) |
20 | | eleq2 2823 |
. . . . . 6
β’ (π’ = (π(,]+β) β (+β β π’ β +β β (π(,]+β))) |
21 | | eleq2 2823 |
. . . . . . . . 9
β’ (π’ = (π(,]+β) β ((πΉβπ) β π’ β (πΉβπ) β (π(,]+β))) |
22 | 21 | anbi2d 630 |
. . . . . . . 8
β’ (π’ = (π(,]+β) β ((π β dom πΉ β§ (πΉβπ) β π’) β (π β dom πΉ β§ (πΉβπ) β (π(,]+β)))) |
23 | 22 | ralbidv 3171 |
. . . . . . 7
β’ (π’ = (π(,]+β) β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)))) |
24 | 23 | rexbidv 3172 |
. . . . . 6
β’ (π’ = (π(,]+β) β (βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)))) |
25 | 20, 24 | imbi12d 345 |
. . . . 5
β’ (π’ = (π(,]+β) β ((+β β π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (+β β (π(,]+β) β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β))))) |
26 | 25 | rspcva 3578 |
. . . 4
β’ (((π(,]+β) β
(ordTopβ β€ ) β§ βπ’ β (ordTopβ β€ )(+β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (+β β (π(,]+β) β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)))) |
27 | 13, 19, 26 | sylc 65 |
. . 3
β’ (π β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β))) |
28 | | nfv 1918 |
. . . 4
β’
β²ππ |
29 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
30 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β π β
β*) |
31 | | xlimpnfvlem1.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ*) |
32 | 31 | ffdmd 6700 |
. . . . . . . . . . 11
β’ (π β πΉ:dom πΉβΆβ*) |
33 | 32 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β dom πΉ) β (πΉβπ) β
β*) |
34 | 33 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β (πΉβπ) β
β*) |
35 | 16 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β +β β
β*) |
36 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β (πΉβπ) β (π(,]+β)) |
37 | 30, 35, 36 | iocgtlbd 43895 |
. . . . . . . . 9
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β π < (πΉβπ)) |
38 | 30, 34, 37 | xrltled 13075 |
. . . . . . . 8
β’ ((π β§ (π β dom πΉ β§ (πΉβπ) β (π(,]+β))) β π β€ (πΉβπ)) |
39 | 38 | ex 414 |
. . . . . . 7
β’ (π β ((π β dom πΉ β§ (πΉβπ) β (π(,]+β)) β π β€ (πΉβπ))) |
40 | 39 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β (π(,]+β)) β π β€ (πΉβπ))) |
41 | 29, 40 | ralimdaa 3242 |
. . . . 5
β’ (π β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)) β βπ β
(β€β₯βπ)π β€ (πΉβπ))) |
42 | 41 | a1d 25 |
. . . 4
β’ (π β (π β β€ β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)) β βπ β
(β€β₯βπ)π β€ (πΉβπ)))) |
43 | 28, 42 | reximdai 3243 |
. . 3
β’ (π β (βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(,]+β)) β βπ β β€ βπ β
(β€β₯βπ)π β€ (πΉβπ))) |
44 | 27, 43 | mpd 15 |
. 2
β’ (π β βπ β β€ βπ β (β€β₯βπ)π β€ (πΉβπ)) |
45 | | xlimpnfvlem1.m |
. . 3
β’ (π β π β β€) |
46 | | xlimpnfvlem1.z |
. . . 4
β’ π =
(β€β₯βπ) |
47 | 46 | rexuz3 15239 |
. . 3
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ) β βπ β β€ βπ β (β€β₯βπ)π β€ (πΉβπ))) |
48 | 45, 47 | syl 17 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ) β βπ β β€ βπ β (β€β₯βπ)π β€ (πΉβπ))) |
49 | 44, 48 | mpbird 257 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ)) |