Step | Hyp | Ref
| Expression |
1 | | lern 18574 |
. . . . 5
β’
β* = ran β€ |
2 | | df-rn 5683 |
. . . . 5
β’ ran β€
= dom β‘ β€ |
3 | 1, 2 | eqtri 2755 |
. . . 4
β’
β* = dom β‘
β€ |
4 | | letsr 18576 |
. . . . . 6
β’ β€
β TosetRel |
5 | | cnvtsr 18571 |
. . . . . 6
β’ ( β€
β TosetRel β β‘ β€ β
TosetRel ) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
β’ β‘ β€ β TosetRel |
7 | 6 | a1i 11 |
. . . 4
β’ (β€
β β‘ β€ β TosetRel
) |
8 | | cnvordtrestixx.1 |
. . . . 5
β’ π΄ β
β* |
9 | 8 | a1i 11 |
. . . 4
β’ (β€
β π΄ β
β*) |
10 | | brcnvg 5876 |
. . . . . . . . . 10
β’ ((π¦ β π΄ β§ π§ β β*) β (π¦β‘ β€ π§ β π§ β€ π¦)) |
11 | 10 | adantlr 714 |
. . . . . . . . 9
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β (π¦β‘ β€ π§ β π§ β€ π¦)) |
12 | | simpr 484 |
. . . . . . . . . 10
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β π§ β
β*) |
13 | | simplr 768 |
. . . . . . . . . 10
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β π₯ β π΄) |
14 | | brcnvg 5876 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ π₯ β π΄) β (π§β‘
β€ π₯ β π₯ β€ π§)) |
15 | 12, 13, 14 | syl2anc 583 |
. . . . . . . . 9
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β (π§β‘ β€ π₯ β π₯ β€ π§)) |
16 | 11, 15 | anbi12d 630 |
. . . . . . . 8
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β ((π¦β‘ β€ π§ β§ π§β‘
β€ π₯) β (π§ β€ π¦ β§ π₯ β€ π§))) |
17 | | ancom 460 |
. . . . . . . 8
β’ ((π§ β€ π¦ β§ π₯ β€ π§) β (π₯ β€ π§ β§ π§ β€ π¦)) |
18 | 16, 17 | bitrdi 287 |
. . . . . . 7
β’ (((π¦ β π΄ β§ π₯ β π΄) β§ π§ β β*) β ((π¦β‘ β€ π§ β§ π§β‘
β€ π₯) β (π₯ β€ π§ β§ π§ β€ π¦))) |
19 | 18 | rabbidva 3434 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ β π΄) β {π§ β β* β£ (π¦β‘ β€ π§ β§ π§β‘
β€ π₯)} = {π§ β β*
β£ (π₯ β€ π§ β§ π§ β€ π¦)}) |
20 | | simpr 484 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ π₯ β π΄) β π₯ β π΄) |
21 | 8, 20 | sselid 3976 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π₯ β π΄) β π₯ β β*) |
22 | | simpl 482 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ π₯ β π΄) β π¦ β π΄) |
23 | 8, 22 | sselid 3976 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π₯ β π΄) β π¦ β β*) |
24 | | iccval 13387 |
. . . . . . . 8
β’ ((π₯ β β*
β§ π¦ β
β*) β (π₯[,]π¦) = {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) |
25 | 21, 23, 24 | syl2anc 583 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π₯ β π΄) β (π₯[,]π¦) = {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) |
26 | | cnvordtrestixx.2 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯[,]π¦) β π΄) |
27 | 26 | ancoms 458 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π₯ β π΄) β (π₯[,]π¦) β π΄) |
28 | 25, 27 | eqsstrrd 4017 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ β π΄) β {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)} β π΄) |
29 | 19, 28 | eqsstrd 4016 |
. . . . 5
β’ ((π¦ β π΄ β§ π₯ β π΄) β {π§ β β* β£ (π¦β‘ β€ π§ β§ π§β‘
β€ π₯)} β π΄) |
30 | 29 | adantl 481 |
. . . 4
β’
((β€ β§ (π¦
β π΄ β§ π₯ β π΄)) β {π§ β β* β£ (π¦β‘ β€ π§ β§ π§β‘
β€ π₯)} β π΄) |
31 | 3, 7, 9, 30 | ordtrest2 23095 |
. . 3
β’ (β€
β (ordTopβ(β‘ β€ β©
(π΄ Γ π΄))) = ((ordTopββ‘ β€ ) βΎt π΄)) |
32 | 31 | mptru 1541 |
. 2
β’
(ordTopβ(β‘ β€ β©
(π΄ Γ π΄))) = ((ordTopββ‘ β€ ) βΎt π΄) |
33 | | tsrps 18570 |
. . . . 5
β’ ( β€
β TosetRel β β€ β PosetRel) |
34 | 4, 33 | ax-mp 5 |
. . . 4
β’ β€
β PosetRel |
35 | | ordtcnv 23092 |
. . . 4
β’ ( β€
β PosetRel β (ordTopββ‘
β€ ) = (ordTopβ β€ )) |
36 | 34, 35 | ax-mp 5 |
. . 3
β’
(ordTopββ‘ β€ ) =
(ordTopβ β€ ) |
37 | 36 | oveq1i 7424 |
. 2
β’
((ordTopββ‘ β€ )
βΎt π΄) =
((ordTopβ β€ ) βΎt π΄) |
38 | 32, 37 | eqtr2i 2756 |
1
β’
((ordTopβ β€ ) βΎt π΄) = (ordTopβ(β‘ β€ β© (π΄ Γ π΄))) |