Step | Hyp | Ref
| Expression |
1 | | letsr 18551 |
. . . 4
β’ β€
β TosetRel |
2 | 1 | a1i 11 |
. . 3
β’ (π β β€ β TosetRel
) |
3 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π₯ β β*) β π₯ β
β*) |
4 | | xrmulc1cn.c |
. . . . . . . . 9
β’ (π β πΆ β
β+) |
5 | 4 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π₯ β β*) β πΆ β
β+) |
6 | 5 | rpxrd 13022 |
. . . . . . 7
β’ ((π β§ π₯ β β*) β πΆ β
β*) |
7 | 3, 6 | xmulcld 13286 |
. . . . . 6
β’ ((π β§ π₯ β β*) β (π₯ Β·e πΆ) β
β*) |
8 | 7 | ralrimiva 3145 |
. . . . 5
β’ (π β βπ₯ β β* (π₯ Β·e πΆ) β
β*) |
9 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ π¦ β β*) β π¦ β
β*) |
10 | 4 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π¦ β β*) β πΆ β
β+) |
11 | 10 | rpred 13021 |
. . . . . . . 8
β’ ((π β§ π¦ β β*) β πΆ β
β) |
12 | 10 | rpne0d 13026 |
. . . . . . . 8
β’ ((π β§ π¦ β β*) β πΆ β 0) |
13 | | xreceu 32352 |
. . . . . . . 8
β’ ((π¦ β β*
β§ πΆ β β
β§ πΆ β 0) β
β!π₯ β
β* (πΆ
Β·e π₯) =
π¦) |
14 | 9, 11, 12, 13 | syl3anc 1370 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β
β!π₯ β
β* (πΆ
Β·e π₯) =
π¦) |
15 | | eqcom 2738 |
. . . . . . . . 9
β’ (π¦ = (π₯ Β·e πΆ) β (π₯ Β·e πΆ) = π¦) |
16 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π₯ β β*)
β π₯ β
β*) |
17 | 6 | adantlr 712 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π₯ β β*)
β πΆ β
β*) |
18 | | xmulcom 13250 |
. . . . . . . . . . 11
β’ ((π₯ β β*
β§ πΆ β
β*) β (π₯ Β·e πΆ) = (πΆ Β·e π₯)) |
19 | 16, 17, 18 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π₯ β β*)
β (π₯
Β·e πΆ) =
(πΆ Β·e
π₯)) |
20 | 19 | eqeq1d 2733 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π₯ β β*)
β ((π₯
Β·e πΆ) =
π¦ β (πΆ Β·e π₯) = π¦)) |
21 | 15, 20 | bitrid 282 |
. . . . . . . 8
β’ (((π β§ π¦ β β*) β§ π₯ β β*)
β (π¦ = (π₯ Β·e πΆ) β (πΆ Β·e π₯) = π¦)) |
22 | 21 | reubidva 3391 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β
(β!π₯ β
β* π¦ =
(π₯ Β·e
πΆ) β β!π₯ β β*
(πΆ Β·e
π₯) = π¦)) |
23 | 14, 22 | mpbird 256 |
. . . . . 6
β’ ((π β§ π¦ β β*) β
β!π₯ β
β* π¦ =
(π₯ Β·e
πΆ)) |
24 | 23 | ralrimiva 3145 |
. . . . 5
β’ (π β βπ¦ β β* β!π₯ β β*
π¦ = (π₯ Β·e πΆ)) |
25 | | xrmulc1cn.f |
. . . . . 6
β’ πΉ = (π₯ β β* β¦ (π₯ Β·e πΆ)) |
26 | 25 | f1ompt 7113 |
. . . . 5
β’ (πΉ:β*β1-1-ontoββ* β (βπ₯ β β*
(π₯ Β·e
πΆ) β
β* β§ βπ¦ β β* β!π₯ β β*
π¦ = (π₯ Β·e πΆ))) |
27 | 8, 24, 26 | sylanbrc 582 |
. . . 4
β’ (π β πΉ:β*β1-1-ontoββ*) |
28 | | simplr 766 |
. . . . . . . 8
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β π₯ β
β*) |
29 | | simpr 484 |
. . . . . . . 8
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β π¦ β
β*) |
30 | 4 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β πΆ β
β+) |
31 | | xlemul1 13274 |
. . . . . . . 8
β’ ((π₯ β β*
β§ π¦ β
β* β§ πΆ
β β+) β (π₯ β€ π¦ β (π₯ Β·e πΆ) β€ (π¦ Β·e πΆ))) |
32 | 28, 29, 30, 31 | syl3anc 1370 |
. . . . . . 7
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β (π₯ β€ π¦ β (π₯ Β·e πΆ) β€ (π¦ Β·e πΆ))) |
33 | | ovex 7445 |
. . . . . . . . 9
β’ (π₯ Β·e πΆ) β V |
34 | 25 | fvmpt2 7010 |
. . . . . . . . 9
β’ ((π₯ β β*
β§ (π₯
Β·e πΆ)
β V) β (πΉβπ₯) = (π₯ Β·e πΆ)) |
35 | 28, 33, 34 | sylancl 585 |
. . . . . . . 8
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β (πΉβπ₯) = (π₯ Β·e πΆ)) |
36 | | oveq1 7419 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ Β·e πΆ) = (π¦ Β·e πΆ)) |
37 | | ovex 7445 |
. . . . . . . . . 10
β’ (π¦ Β·e πΆ) β V |
38 | 36, 25, 37 | fvmpt 6999 |
. . . . . . . . 9
β’ (π¦ β β*
β (πΉβπ¦) = (π¦ Β·e πΆ)) |
39 | 38 | adantl 481 |
. . . . . . . 8
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β (πΉβπ¦) = (π¦ Β·e πΆ)) |
40 | 35, 39 | breq12d 5162 |
. . . . . . 7
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β ((πΉβπ₯) β€ (πΉβπ¦) β (π₯ Β·e πΆ) β€ (π¦ Β·e πΆ))) |
41 | 32, 40 | bitr4d 281 |
. . . . . 6
β’ (((π β§ π₯ β β*) β§ π¦ β β*)
β (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
42 | 41 | ralrimiva 3145 |
. . . . 5
β’ ((π β§ π₯ β β*) β
βπ¦ β
β* (π₯ β€
π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
43 | 42 | ralrimiva 3145 |
. . . 4
β’ (π β βπ₯ β β* βπ¦ β β*
(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
44 | | df-isom 6553 |
. . . 4
β’ (πΉ Isom β€ , β€
(β*, β*) β (πΉ:β*β1-1-ontoββ* β§ βπ₯ β β*
βπ¦ β
β* (π₯ β€
π¦ β (πΉβπ₯) β€ (πΉβπ¦)))) |
45 | 27, 43, 44 | sylanbrc 582 |
. . 3
β’ (π β πΉ Isom β€ , β€ (β*,
β*)) |
46 | | ledm 18548 |
. . . 4
β’
β* = dom β€ |
47 | 46, 46 | ordthmeolem 23526 |
. . 3
β’ (( β€
β TosetRel β§ β€ β TosetRel β§ πΉ Isom β€ , β€ (β*,
β*)) β πΉ β ((ordTopβ β€ ) Cn
(ordTopβ β€ ))) |
48 | 2, 2, 45, 47 | syl3anc 1370 |
. 2
β’ (π β πΉ β ((ordTopβ β€ ) Cn
(ordTopβ β€ ))) |
49 | | xrmulc1cn.k |
. . 3
β’ π½ = (ordTopβ β€
) |
50 | 49, 49 | oveq12i 7424 |
. 2
β’ (π½ Cn π½) = ((ordTopβ β€ ) Cn (ordTopβ
β€ )) |
51 | 48, 50 | eleqtrrdi 2843 |
1
β’ (π β πΉ β (π½ Cn π½)) |