Step | Hyp | Ref
| Expression |
1 | | df-xlim 44146 |
. . . 4
β’ ~~>* =
(βπ‘β(ordTopβ β€ )) |
2 | 1 | breqi 5112 |
. . 3
β’ (πΉ~~>*π β πΉ(βπ‘β(ordTopβ
β€ ))π) |
3 | 2 | a1i 11 |
. 2
β’ (π β (πΉ~~>*π β πΉ(βπ‘β(ordTopβ
β€ ))π)) |
4 | | xlimbr.k |
. . 3
β’
β²ππΉ |
5 | | letopon 22572 |
. . . 4
β’
(ordTopβ β€ ) β
(TopOnββ*) |
6 | 5 | a1i 11 |
. . 3
β’ (π β (ordTopβ β€ )
β (TopOnββ*)) |
7 | 4, 6 | lmbr3 44074 |
. 2
β’ (π β (πΉ(βπ‘β(ordTopβ
β€ ))π β (πΉ β (β*
βpm β) β§ π β β* β§ βπ’ β (ordTopβ β€ )(π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
8 | | simpr2 1196 |
. . . 4
β’ ((π β§ (πΉ β (β*
βpm β) β§ π β β* β§
βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β π β
β*) |
9 | | xlimbr.j |
. . . . . . . 8
β’ π½ = (ordTopβ β€
) |
10 | 9 | eqcomi 2742 |
. . . . . . 7
β’
(ordTopβ β€ ) = π½ |
11 | 10 | raleqi 3310 |
. . . . . 6
β’
(βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
12 | | xlimbr.m |
. . . . . . . 8
β’ (π β π β β€) |
13 | | xlimbr.z |
. . . . . . . . . . . . 13
β’ π =
(β€β₯βπ) |
14 | 13 | rexuz3 15239 |
. . . . . . . . . . . 12
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
15 | 14 | bicomd 222 |
. . . . . . . . . . 11
β’ (π β β€ β
(βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
16 | 15 | imbi2d 341 |
. . . . . . . . . 10
β’ (π β β€ β ((π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
17 | 16 | biimpd 228 |
. . . . . . . . 9
β’ (π β β€ β ((π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
18 | 17 | ralimdv 3163 |
. . . . . . . 8
β’ (π β β€ β
(βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
19 | 12, 18 | syl 17 |
. . . . . . 7
β’ (π β (βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
20 | 19 | imp 408 |
. . . . . 6
β’ ((π β§ βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
21 | 11, 20 | sylan2b 595 |
. . . . 5
β’ ((π β§ βπ’ β (ordTopβ β€ )(π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
22 | 21 | 3ad2antr3 1191 |
. . . 4
β’ ((π β§ (πΉ β (β*
βpm β) β§ π β β* β§
βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
23 | 8, 22 | jca 513 |
. . 3
β’ ((π β§ (πΉ β (β*
βpm β) β§ π β β* β§
βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
24 | | cnex 11137 |
. . . . . . 7
β’ β
β V |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
26 | 6 | elfvexd 6882 |
. . . . . 6
β’ (π β β* β
V) |
27 | 13 | uzsscn2 43799 |
. . . . . . 7
β’ π β
β |
28 | 27 | a1i 11 |
. . . . . 6
β’ (π β π β β) |
29 | | xlimbr.f |
. . . . . 6
β’ (π β πΉ:πβΆβ*) |
30 | 25, 26, 28, 29 | fpmd 43579 |
. . . . 5
β’ (π β πΉ β (β*
βpm β)) |
31 | 30 | adantr 482 |
. . . 4
β’ ((π β§ (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β πΉ β (β*
βpm β)) |
32 | | simprl 770 |
. . . 4
β’ ((π β§ (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β π β
β*) |
33 | 16 | biimprd 248 |
. . . . . . . . 9
β’ (π β β€ β ((π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
34 | 33 | ralimdv 3163 |
. . . . . . . 8
β’ (π β β€ β
(βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
35 | 12, 34 | syl 17 |
. . . . . . 7
β’ (π β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
36 | 35 | imp 408 |
. . . . . 6
β’ ((π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
37 | 9 | raleqi 3310 |
. . . . . 6
β’
(βπ’ β
π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β (ordTopβ β€ )(π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
38 | 36, 37 | sylib 217 |
. . . . 5
β’ ((π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β βπ’ β (ordTopβ β€ )(π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
39 | 38 | adantrl 715 |
. . . 4
β’ ((π β§ (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β βπ’ β (ordTopβ β€ )(π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
40 | 31, 32, 39 | 3jca 1129 |
. . 3
β’ ((π β§ (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β (πΉ β (β*
βpm β) β§ π β β* β§
βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
41 | 23, 40 | impbida 800 |
. 2
β’ (π β ((πΉ β (β*
βpm β) β§ π β β* β§
βπ’ β
(ordTopβ β€ )(π
β π’ β
βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
42 | 3, 7, 41 | 3bitrd 305 |
1
β’ (π β (πΉ~~>*π β (π β β* β§
βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |