Step | Hyp | Ref
| Expression |
1 | | letopon 22572 |
. . . . . . 7
β’
(ordTopβ β€ ) β
(TopOnββ*) |
2 | 1 | a1i 11 |
. . . . . 6
β’ (π β (ordTopβ β€ )
β (TopOnββ*)) |
3 | 2 | elfvexd 6882 |
. . . . 5
β’ (π β β* β
V) |
4 | | cnex 11137 |
. . . . . 6
β’ β
β V |
5 | 4 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
6 | | xlimpnfvlem2.f |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
7 | | xlimpnfvlem2.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
8 | 7 | uzsscn2 43799 |
. . . . . 6
β’ π β
β |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β π β β) |
10 | | elpm2r 8786 |
. . . . 5
β’
(((β* β V β§ β β V) β§ (πΉ:πβΆβ* β§ π β β)) β πΉ β (β*
βpm β)) |
11 | 3, 5, 6, 9, 10 | syl22anc 838 |
. . . 4
β’ (π β πΉ β (β*
βpm β)) |
12 | | pnfxr 11214 |
. . . . 5
β’ +β
β β* |
13 | 12 | a1i 11 |
. . . 4
β’ (π β +β β
β*) |
14 | | pnfnei 22587 |
. . . . . . . 8
β’ ((π’ β (ordTopβ β€ )
β§ +β β π’)
β βπ₯ β
β (π₯(,]+β)
β π’) |
15 | 14 | adantll 713 |
. . . . . . 7
β’ (((π β§ π’ β (ordTopβ β€ )) β§ +β
β π’) β
βπ₯ β β
(π₯(,]+β) β
π’) |
16 | | xlimpnfvlem2.j |
. . . . . . . . . . . . 13
β’
β²ππ |
17 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π π₯ β β |
18 | 16, 17 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π(π β§ π₯ β β) |
19 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π(π₯(,]+β) β π’ |
20 | 18, 19 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π((π β§ π₯ β β) β§ (π₯(,]+β) β π’) |
21 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ (π β π β§ βπ β (β€β₯βπ)π₯ < (πΉβπ))) β βπ β (β€β₯βπ)π₯ < (πΉβπ)) |
22 | | xlimpnfvlem2.k |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ |
23 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π π₯ β β |
24 | 22, 23 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π β§ π₯ β β) |
25 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π₯(,]+β) β π’ |
26 | 24, 25 | nfan 1903 |
. . . . . . . . . . . . . . . 16
β’
β²π((π β§ π₯ β β) β§ (π₯(,]+β) β π’) |
27 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π π β π |
28 | 26, 27 | nfan 1903 |
. . . . . . . . . . . . . . 15
β’
β²π(((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) |
29 | 7 | uztrn2 12787 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
30 | 29 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β π) |
31 | 6 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom πΉ = π) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β dom πΉ = π) |
33 | 30, 32 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β dom πΉ) |
34 | 33 | ad5ant134 1368 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π β dom πΉ) |
35 | 34 | adantl4r 754 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π β dom πΉ) |
36 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (π₯(,]+β) β π’) |
37 | 36 | adantl4r 754 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (π₯(,]+β) β π’) |
38 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π₯ β β) |
39 | | rexr 11206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β π₯ β
β*) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π₯ β β*) |
41 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β +β β
β*) |
42 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π) |
43 | 29 | ad4ant23 752 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π β π) |
44 | 6 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
45 | 42, 43, 44 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (πΉβπ) β
β*) |
46 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β π₯ < (πΉβπ)) |
47 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β πΉ:πβΆβ*) |
48 | 47, 30 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
49 | 48 | pnfged 43795 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β€ +β) |
50 | 49 | ad5ant134 1368 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (πΉβπ) β€ +β) |
51 | 40, 41, 45, 46, 50 | eliocd 43831 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (πΉβπ) β (π₯(,]+β)) |
52 | 51 | adantl3r 749 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (πΉβπ) β (π₯(,]+β)) |
53 | 37, 52 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (πΉβπ) β π’) |
54 | 35, 53 | jca 513 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β π’)) |
55 | 54 | ex 414 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β§ π β (β€β₯βπ)) β (π₯ < (πΉβπ) β (π β dom πΉ β§ (πΉβπ) β π’))) |
56 | 28, 55 | ralimdaa 3242 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π) β (βπ β (β€β₯βπ)π₯ < (πΉβπ) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
57 | 56 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ (π β π β§ βπ β (β€β₯βπ)π₯ < (πΉβπ))) β (βπ β (β€β₯βπ)π₯ < (πΉβπ) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
58 | 21, 57 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ (π β π β§ βπ β (β€β₯βπ)π₯ < (πΉβπ))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
59 | 58 | 3impb 1116 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β§ π β π β§ βπ β (β€β₯βπ)π₯ < (πΉβπ)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
60 | | xlimpnfvlem2.g |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) |
61 | 60 | r19.21bi 3233 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) |
62 | 61 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) |
63 | 20, 59, 62 | reximdd 43450 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
64 | | xlimpnfvlem2.m |
. . . . . . . . . . . 12
β’ (π β π β β€) |
65 | 7 | rexuz3 15239 |
. . . . . . . . . . . 12
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
β’ (π β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
67 | 66 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
68 | 63, 67 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
69 | 68 | rexlimdva2 3151 |
. . . . . . . 8
β’ (π β (βπ₯ β β (π₯(,]+β) β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
70 | 69 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π’ β (ordTopβ β€ )) β§ +β
β π’) β
(βπ₯ β β
(π₯(,]+β) β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
71 | 15, 70 | mpd 15 |
. . . . . 6
β’ (((π β§ π’ β (ordTopβ β€ )) β§ +β
β π’) β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
72 | 71 | ex 414 |
. . . . 5
β’ ((π β§ π’ β (ordTopβ β€ )) β
(+β β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
73 | 72 | ralrimiva 3140 |
. . . 4
β’ (π β βπ’ β (ordTopβ β€ )(+β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
74 | 11, 13, 73 | 3jca 1129 |
. . 3
β’ (π β (πΉ β (β*
βpm β) β§ +β β β* β§
βπ’ β
(ordTopβ β€ )(+β β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
75 | | nfcv 2904 |
. . . 4
β’
β²ππΉ |
76 | 75, 2 | lmbr3 44074 |
. . 3
β’ (π β (πΉ(βπ‘β(ordTopβ
β€ ))+β β (πΉ β
(β* βpm β) β§ +β β
β* β§ βπ’ β (ordTopβ β€ )(+β β
π’ β βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
77 | 74, 76 | mpbird 257 |
. 2
β’ (π β πΉ(βπ‘β(ordTopβ
β€ ))+β) |
78 | | df-xlim 44146 |
. . . 4
β’ ~~>* =
(βπ‘β(ordTopβ β€ )) |
79 | 78 | breqi 5112 |
. . 3
β’ (πΉ~~>*+β β πΉ(βπ‘β(ordTopβ
β€ ))+β) |
80 | 79 | a1i 11 |
. 2
β’ (π β (πΉ~~>*+β β πΉ(βπ‘β(ordTopβ
β€ ))+β)) |
81 | 77, 80 | mpbird 257 |
1
β’ (π β πΉ~~>*+β) |