Step | Hyp | Ref
| Expression |
1 | | icopnfhmeo.f |
. . . . 5
β’ πΉ = (π₯ β (0[,)1) β¦ (π₯ / (1 β π₯))) |
2 | 1 | icopnfcnv 24328 |
. . . 4
β’ (πΉ:(0[,)1)β1-1-ontoβ(0[,)+β) β§ β‘πΉ = (π¦ β (0[,)+β) β¦ (π¦ / (1 + π¦)))) |
3 | 2 | simpli 485 |
. . 3
β’ πΉ:(0[,)1)β1-1-ontoβ(0[,)+β) |
4 | | 0re 11165 |
. . . . . . . . . . 11
β’ 0 β
β |
5 | | 1xr 11222 |
. . . . . . . . . . 11
β’ 1 β
β* |
6 | | elico2 13337 |
. . . . . . . . . . 11
β’ ((0
β β β§ 1 β β*) β (π₯ β (0[,)1) β (π₯ β β β§ 0 β€ π₯ β§ π₯ < 1))) |
7 | 4, 5, 6 | mp2an 691 |
. . . . . . . . . 10
β’ (π₯ β (0[,)1) β (π₯ β β β§ 0 β€
π₯ β§ π₯ < 1)) |
8 | 7 | simp1bi 1146 |
. . . . . . . . 9
β’ (π₯ β (0[,)1) β π₯ β
β) |
9 | 8 | ssriv 3952 |
. . . . . . . 8
β’ (0[,)1)
β β |
10 | 9 | sseli 3944 |
. . . . . . 7
β’ (π§ β (0[,)1) β π§ β
β) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β π§ β
β) |
12 | | elico2 13337 |
. . . . . . . . . . 11
β’ ((0
β β β§ 1 β β*) β (π€ β (0[,)1) β (π€ β β β§ 0 β€ π€ β§ π€ < 1))) |
13 | 4, 5, 12 | mp2an 691 |
. . . . . . . . . 10
β’ (π€ β (0[,)1) β (π€ β β β§ 0 β€
π€ β§ π€ < 1)) |
14 | 13 | simp3bi 1148 |
. . . . . . . . 9
β’ (π€ β (0[,)1) β π€ < 1) |
15 | 9 | sseli 3944 |
. . . . . . . . . 10
β’ (π€ β (0[,)1) β π€ β
β) |
16 | | 1re 11163 |
. . . . . . . . . 10
β’ 1 β
β |
17 | | difrp 12961 |
. . . . . . . . . 10
β’ ((π€ β β β§ 1 β
β) β (π€ < 1
β (1 β π€) β
β+)) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . . . 9
β’ (π€ β (0[,)1) β (π€ < 1 β (1 β π€) β
β+)) |
19 | 14, 18 | mpbid 231 |
. . . . . . . 8
β’ (π€ β (0[,)1) β (1
β π€) β
β+) |
20 | 19 | rpregt0d 12971 |
. . . . . . 7
β’ (π€ β (0[,)1) β ((1
β π€) β β
β§ 0 < (1 β π€))) |
21 | 20 | adantl 483 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((1
β π€) β β
β§ 0 < (1 β π€))) |
22 | 15 | adantl 483 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β π€ β
β) |
23 | | elico2 13337 |
. . . . . . . . . . 11
β’ ((0
β β β§ 1 β β*) β (π§ β (0[,)1) β (π§ β β β§ 0 β€ π§ β§ π§ < 1))) |
24 | 4, 5, 23 | mp2an 691 |
. . . . . . . . . 10
β’ (π§ β (0[,)1) β (π§ β β β§ 0 β€
π§ β§ π§ < 1)) |
25 | 24 | simp3bi 1148 |
. . . . . . . . 9
β’ (π§ β (0[,)1) β π§ < 1) |
26 | | difrp 12961 |
. . . . . . . . . 10
β’ ((π§ β β β§ 1 β
β) β (π§ < 1
β (1 β π§) β
β+)) |
27 | 10, 16, 26 | sylancl 587 |
. . . . . . . . 9
β’ (π§ β (0[,)1) β (π§ < 1 β (1 β π§) β
β+)) |
28 | 25, 27 | mpbid 231 |
. . . . . . . 8
β’ (π§ β (0[,)1) β (1
β π§) β
β+) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (1
β π§) β
β+) |
30 | 29 | rpregt0d 12971 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((1
β π§) β β
β§ 0 < (1 β π§))) |
31 | | lt2mul2div 12041 |
. . . . . 6
β’ (((π§ β β β§ ((1
β π€) β β
β§ 0 < (1 β π€))) β§ (π€ β β β§ ((1 β π§) β β β§ 0 < (1
β π§)))) β
((π§ Β· (1 β
π€)) < (π€ Β· (1 β π§)) β (π§ / (1 β π§)) < (π€ / (1 β π€)))) |
32 | 11, 21, 22, 30, 31 | syl22anc 838 |
. . . . 5
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((π§ Β· (1 β π€)) < (π€ Β· (1 β π§)) β (π§ / (1 β π§)) < (π€ / (1 β π€)))) |
33 | 11, 22 | remulcld 11193 |
. . . . . . 7
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ Β· π€) β β) |
34 | 11, 22, 33 | ltsub1d 11772 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ < π€ β (π§ β (π§ Β· π€)) < (π€ β (π§ Β· π€)))) |
35 | 11 | recnd 11191 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β π§ β
β) |
36 | | 1cnd 11158 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β 1 β
β) |
37 | 22 | recnd 11191 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β π€ β
β) |
38 | 35, 36, 37 | subdid 11619 |
. . . . . . . 8
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ Β· (1 β π€)) = ((π§ Β· 1) β (π§ Β· π€))) |
39 | 35 | mulridd 11180 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ Β· 1) = π§) |
40 | 39 | oveq1d 7376 |
. . . . . . . 8
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((π§ Β· 1) β (π§ Β· π€)) = (π§ β (π§ Β· π€))) |
41 | 38, 40 | eqtrd 2773 |
. . . . . . 7
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ Β· (1 β π€)) = (π§ β (π§ Β· π€))) |
42 | 37, 36, 35 | subdid 11619 |
. . . . . . . 8
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π€ Β· (1 β π§)) = ((π€ Β· 1) β (π€ Β· π§))) |
43 | 37 | mulridd 11180 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π€ Β· 1) = π€) |
44 | 37, 35 | mulcomd 11184 |
. . . . . . . . 9
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π€ Β· π§) = (π§ Β· π€)) |
45 | 43, 44 | oveq12d 7379 |
. . . . . . . 8
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((π€ Β· 1) β (π€ Β· π§)) = (π€ β (π§ Β· π€))) |
46 | 42, 45 | eqtrd 2773 |
. . . . . . 7
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π€ Β· (1 β π§)) = (π€ β (π§ Β· π€))) |
47 | 41, 46 | breq12d 5122 |
. . . . . 6
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((π§ Β· (1 β π€)) < (π€ Β· (1 β π§)) β (π§ β (π§ Β· π€)) < (π€ β (π§ Β· π€)))) |
48 | 34, 47 | bitr4d 282 |
. . . . 5
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ < π€ β (π§ Β· (1 β π€)) < (π€ Β· (1 β π§)))) |
49 | | id 22 |
. . . . . . . 8
β’ (π₯ = π§ β π₯ = π§) |
50 | | oveq2 7369 |
. . . . . . . 8
β’ (π₯ = π§ β (1 β π₯) = (1 β π§)) |
51 | 49, 50 | oveq12d 7379 |
. . . . . . 7
β’ (π₯ = π§ β (π₯ / (1 β π₯)) = (π§ / (1 β π§))) |
52 | | ovex 7394 |
. . . . . . 7
β’ (π§ / (1 β π§)) β V |
53 | 51, 1, 52 | fvmpt 6952 |
. . . . . 6
β’ (π§ β (0[,)1) β (πΉβπ§) = (π§ / (1 β π§))) |
54 | | id 22 |
. . . . . . . 8
β’ (π₯ = π€ β π₯ = π€) |
55 | | oveq2 7369 |
. . . . . . . 8
β’ (π₯ = π€ β (1 β π₯) = (1 β π€)) |
56 | 54, 55 | oveq12d 7379 |
. . . . . . 7
β’ (π₯ = π€ β (π₯ / (1 β π₯)) = (π€ / (1 β π€))) |
57 | | ovex 7394 |
. . . . . . 7
β’ (π€ / (1 β π€)) β V |
58 | 56, 1, 57 | fvmpt 6952 |
. . . . . 6
β’ (π€ β (0[,)1) β (πΉβπ€) = (π€ / (1 β π€))) |
59 | 53, 58 | breqan12d 5125 |
. . . . 5
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β ((πΉβπ§) < (πΉβπ€) β (π§ / (1 β π§)) < (π€ / (1 β π€)))) |
60 | 32, 48, 59 | 3bitr4d 311 |
. . . 4
β’ ((π§ β (0[,)1) β§ π€ β (0[,)1)) β (π§ < π€ β (πΉβπ§) < (πΉβπ€))) |
61 | 60 | rgen2 3191 |
. . 3
β’
βπ§ β
(0[,)1)βπ€ β
(0[,)1)(π§ < π€ β (πΉβπ§) < (πΉβπ€)) |
62 | | df-isom 6509 |
. . 3
β’ (πΉ Isom < , < ((0[,)1),
(0[,)+β)) β (πΉ:(0[,)1)β1-1-ontoβ(0[,)+β) β§ βπ§ β (0[,)1)βπ€ β (0[,)1)(π§ < π€ β (πΉβπ§) < (πΉβπ€)))) |
63 | 3, 61, 62 | mpbir2an 710 |
. 2
β’ πΉ Isom < , < ((0[,)1),
(0[,)+β)) |
64 | | letsr 18490 |
. . . . . 6
β’ β€
β TosetRel |
65 | 64 | elexi 3466 |
. . . . 5
β’ β€
β V |
66 | 65 | inex1 5278 |
. . . 4
β’ ( β€
β© ((0[,)1) Γ (0[,)1))) β V |
67 | 65 | inex1 5278 |
. . . 4
β’ ( β€
β© ((0[,)+β) Γ (0[,)+β))) β V |
68 | | icossxr 13358 |
. . . . . . . 8
β’ (0[,)1)
β β* |
69 | | icossxr 13358 |
. . . . . . . 8
β’
(0[,)+β) β β* |
70 | | leiso 14367 |
. . . . . . . 8
β’ (((0[,)1)
β β* β§ (0[,)+β) β β*)
β (πΉ Isom < , <
((0[,)1), (0[,)+β)) β πΉ Isom β€ , β€ ((0[,)1),
(0[,)+β)))) |
71 | 68, 69, 70 | mp2an 691 |
. . . . . . 7
β’ (πΉ Isom < , < ((0[,)1),
(0[,)+β)) β πΉ
Isom β€ , β€ ((0[,)1), (0[,)+β))) |
72 | 63, 71 | mpbi 229 |
. . . . . 6
β’ πΉ Isom β€ , β€ ((0[,)1),
(0[,)+β)) |
73 | | isores1 7283 |
. . . . . 6
β’ (πΉ Isom β€ , β€ ((0[,)1),
(0[,)+β)) β πΉ
Isom ( β€ β© ((0[,)1) Γ (0[,)1))), β€ ((0[,)1),
(0[,)+β))) |
74 | 72, 73 | mpbi 229 |
. . . . 5
β’ πΉ Isom ( β€ β© ((0[,)1)
Γ (0[,)1))), β€ ((0[,)1), (0[,)+β)) |
75 | | isores2 7282 |
. . . . 5
β’ (πΉ Isom ( β€ β© ((0[,)1)
Γ (0[,)1))), β€ ((0[,)1), (0[,)+β)) β πΉ Isom ( β€ β© ((0[,)1) Γ
(0[,)1))), ( β€ β© ((0[,)+β) Γ (0[,)+β)))((0[,)1),
(0[,)+β))) |
76 | 74, 75 | mpbi 229 |
. . . 4
β’ πΉ Isom ( β€ β© ((0[,)1)
Γ (0[,)1))), ( β€ β© ((0[,)+β) Γ
(0[,)+β)))((0[,)1), (0[,)+β)) |
77 | | tsrps 18484 |
. . . . . . . 8
β’ ( β€
β TosetRel β β€ β PosetRel) |
78 | 64, 77 | ax-mp 5 |
. . . . . . 7
β’ β€
β PosetRel |
79 | | ledm 18487 |
. . . . . . . 8
β’
β* = dom β€ |
80 | 79 | psssdm 18479 |
. . . . . . 7
β’ (( β€
β PosetRel β§ (0[,)1) β β*) β dom ( β€
β© ((0[,)1) Γ (0[,)1))) = (0[,)1)) |
81 | 78, 68, 80 | mp2an 691 |
. . . . . 6
β’ dom (
β€ β© ((0[,)1) Γ (0[,)1))) = (0[,)1) |
82 | 81 | eqcomi 2742 |
. . . . 5
β’ (0[,)1) =
dom ( β€ β© ((0[,)1) Γ (0[,)1))) |
83 | 79 | psssdm 18479 |
. . . . . . 7
β’ (( β€
β PosetRel β§ (0[,)+β) β β*) β dom (
β€ β© ((0[,)+β) Γ (0[,)+β))) =
(0[,)+β)) |
84 | 78, 69, 83 | mp2an 691 |
. . . . . 6
β’ dom (
β€ β© ((0[,)+β) Γ (0[,)+β))) =
(0[,)+β) |
85 | 84 | eqcomi 2742 |
. . . . 5
β’
(0[,)+β) = dom ( β€ β© ((0[,)+β) Γ
(0[,)+β))) |
86 | 82, 85 | ordthmeo 23176 |
. . . 4
β’ ((( β€
β© ((0[,)1) Γ (0[,)1))) β V β§ ( β€ β© ((0[,)+β)
Γ (0[,)+β))) β V β§ πΉ Isom ( β€ β© ((0[,)1) Γ
(0[,)1))), ( β€ β© ((0[,)+β) Γ (0[,)+β)))((0[,)1),
(0[,)+β))) β πΉ
β ((ordTopβ( β€ β© ((0[,)1) Γ
(0[,)1))))Homeo(ordTopβ( β€ β© ((0[,)+β) Γ
(0[,)+β)))))) |
87 | 66, 67, 76, 86 | mp3an 1462 |
. . 3
β’ πΉ β ((ordTopβ( β€
β© ((0[,)1) Γ (0[,)1))))Homeo(ordTopβ( β€ β©
((0[,)+β) Γ (0[,)+β))))) |
88 | | icopnfhmeo.j |
. . . . . . 7
β’ π½ =
(TopOpenββfld) |
89 | | eqid 2733 |
. . . . . . 7
β’
(ordTopβ β€ ) = (ordTopβ β€ ) |
90 | 88, 89 | xrrest2 24194 |
. . . . . 6
β’ ((0[,)1)
β β β (π½
βΎt (0[,)1)) = ((ordTopβ β€ ) βΎt
(0[,)1))) |
91 | 9, 90 | ax-mp 5 |
. . . . 5
β’ (π½ βΎt (0[,)1)) =
((ordTopβ β€ ) βΎt (0[,)1)) |
92 | | iccssico2 13347 |
. . . . . 6
β’ ((π₯ β (0[,)1) β§ π¦ β (0[,)1)) β (π₯[,]π¦) β (0[,)1)) |
93 | 68, 92 | ordtrestixx 22596 |
. . . . 5
β’
((ordTopβ β€ ) βΎt (0[,)1)) = (ordTopβ(
β€ β© ((0[,)1) Γ (0[,)1)))) |
94 | 91, 93 | eqtri 2761 |
. . . 4
β’ (π½ βΎt (0[,)1)) =
(ordTopβ( β€ β© ((0[,)1) Γ (0[,)1)))) |
95 | | rge0ssre 13382 |
. . . . . 6
β’
(0[,)+β) β β |
96 | 88, 89 | xrrest2 24194 |
. . . . . 6
β’
((0[,)+β) β β β (π½ βΎt (0[,)+β)) =
((ordTopβ β€ ) βΎt (0[,)+β))) |
97 | 95, 96 | ax-mp 5 |
. . . . 5
β’ (π½ βΎt
(0[,)+β)) = ((ordTopβ β€ ) βΎt
(0[,)+β)) |
98 | | iccssico2 13347 |
. . . . . 6
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯[,]π¦) β
(0[,)+β)) |
99 | 69, 98 | ordtrestixx 22596 |
. . . . 5
β’
((ordTopβ β€ ) βΎt (0[,)+β)) =
(ordTopβ( β€ β© ((0[,)+β) Γ
(0[,)+β)))) |
100 | 97, 99 | eqtri 2761 |
. . . 4
β’ (π½ βΎt
(0[,)+β)) = (ordTopβ( β€ β© ((0[,)+β) Γ
(0[,)+β)))) |
101 | 94, 100 | oveq12i 7373 |
. . 3
β’ ((π½ βΎt
(0[,)1))Homeo(π½
βΎt (0[,)+β))) = ((ordTopβ( β€ β© ((0[,)1)
Γ (0[,)1))))Homeo(ordTopβ( β€ β© ((0[,)+β) Γ
(0[,)+β))))) |
102 | 87, 101 | eleqtrri 2833 |
. 2
β’ πΉ β ((π½ βΎt (0[,)1))Homeo(π½ βΎt
(0[,)+β))) |
103 | 63, 102 | pm3.2i 472 |
1
β’ (πΉ Isom < , < ((0[,)1),
(0[,)+β)) β§ πΉ
β ((π½
βΎt (0[,)1))Homeo(π½ βΎt
(0[,)+β)))) |