Metamath Proof Explorer


Theorem icchmeo

Description: The natural bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses icchmeo.j J = TopOpen fld
icchmeo.f F = x 0 1 x B + 1 x A
Assertion icchmeo A B A < B F II Homeo J 𝑡 A B

Proof

Step Hyp Ref Expression
1 icchmeo.j J = TopOpen fld
2 icchmeo.f F = x 0 1 x B + 1 x A
3 iitopon II TopOn 0 1
4 3 a1i A B A < B II TopOn 0 1
5 1 dfii3 II = J 𝑡 0 1
6 5 eqcomi J 𝑡 0 1 = II
7 6 oveq2i II Cn J 𝑡 0 1 = II Cn II
8 1 cnfldtop J Top
9 cnrest2r J Top II Cn J 𝑡 0 1 II Cn J
10 8 9 ax-mp II Cn J 𝑡 0 1 II Cn J
11 7 10 eqsstrri II Cn II II Cn J
12 4 cnmptid A B A < B x 0 1 x II Cn II
13 11 12 sselid A B A < B x 0 1 x II Cn J
14 1 cnfldtopon J TopOn
15 14 a1i A B A < B J TopOn
16 simp2 A B A < B B
17 16 recnd A B A < B B
18 4 15 17 cnmptc A B A < B x 0 1 B II Cn J
19 1 mpomulcn u , v u v J × t J Cn J
20 19 a1i A B A < B u , v u v J × t J Cn J
21 oveq12 u = x v = B u v = x B
22 4 13 18 15 15 20 21 cnmpt12 A B A < B x 0 1 x B II Cn J
23 1cnd A B A < B 1
24 4 15 23 cnmptc A B A < B x 0 1 1 II Cn J
25 1 subcn J × t J Cn J
26 25 a1i A B A < B J × t J Cn J
27 4 24 13 26 cnmpt12f A B A < B x 0 1 1 x II Cn J
28 simp1 A B A < B A
29 28 recnd A B A < B A
30 4 15 29 cnmptc A B A < B x 0 1 A II Cn J
31 oveq12 u = 1 x v = A u v = 1 x A
32 4 27 30 15 15 20 31 cnmpt12 A B A < B x 0 1 1 x A II Cn J
33 1 addcn + J × t J Cn J
34 33 a1i A B A < B + J × t J Cn J
35 4 22 32 34 cnmpt12f A B A < B x 0 1 x B + 1 x A II Cn J
36 2 35 eqeltrid A B A < B F II Cn J
37 2 iccf1o A B A < B F : 0 1 1-1 onto A B F -1 = y A B y A B A
38 37 simpld A B A < B F : 0 1 1-1 onto A B
39 f1of F : 0 1 1-1 onto A B F : 0 1 A B
40 frn F : 0 1 A B ran F A B
41 38 39 40 3syl A B A < B ran F A B
42 iccssre A B A B
43 42 3adant3 A B A < B A B
44 ax-resscn
45 43 44 sstrdi A B A < B A B
46 cnrest2 J TopOn ran F A B A B F II Cn J F II Cn J 𝑡 A B
47 14 41 45 46 mp3an2i A B A < B F II Cn J F II Cn J 𝑡 A B
48 36 47 mpbid A B A < B F II Cn J 𝑡 A B
49 37 simprd A B A < B F -1 = y A B y A B A
50 resttopon J TopOn A B J 𝑡 A B TopOn A B
51 14 45 50 sylancr A B A < B J 𝑡 A B TopOn A B
52 cnrest2r J Top J 𝑡 A B Cn J 𝑡 A B J 𝑡 A B Cn J
53 8 52 ax-mp J 𝑡 A B Cn J 𝑡 A B J 𝑡 A B Cn J
54 51 cnmptid A B A < B y A B y J 𝑡 A B Cn J 𝑡 A B
55 53 54 sselid A B A < B y A B y J 𝑡 A B Cn J
56 51 15 29 cnmptc A B A < B y A B A J 𝑡 A B Cn J
57 51 55 56 26 cnmpt12f A B A < B y A B y A J 𝑡 A B Cn J
58 difrp A B A < B B A +
59 58 biimp3a A B A < B B A +
60 rpcnne0 B A + B A B A 0
61 1 divccn B A B A 0 x x B A J Cn J
62 59 60 61 3syl A B A < B x x B A J Cn J
63 oveq1 x = y A x B A = y A B A
64 51 57 15 62 63 cnmpt11 A B A < B y A B y A B A J 𝑡 A B Cn J
65 49 64 eqeltrd A B A < B F -1 J 𝑡 A B Cn J
66 dfdm4 dom F = ran F -1
67 66 eqimss2i ran F -1 dom F
68 f1odm F : 0 1 1-1 onto A B dom F = 0 1
69 38 68 syl A B A < B dom F = 0 1
70 67 69 sseqtrid A B A < B ran F -1 0 1
71 unitsscn 0 1
72 71 a1i A B A < B 0 1
73 cnrest2 J TopOn ran F -1 0 1 0 1 F -1 J 𝑡 A B Cn J F -1 J 𝑡 A B Cn J 𝑡 0 1
74 14 70 72 73 mp3an2i A B A < B F -1 J 𝑡 A B Cn J F -1 J 𝑡 A B Cn J 𝑡 0 1
75 65 74 mpbid A B A < B F -1 J 𝑡 A B Cn J 𝑡 0 1
76 5 oveq2i J 𝑡 A B Cn II = J 𝑡 A B Cn J 𝑡 0 1
77 75 76 eleqtrrdi A B A < B F -1 J 𝑡 A B Cn II
78 ishmeo F II Homeo J 𝑡 A B F II Cn J 𝑡 A B F -1 J 𝑡 A B Cn II
79 48 77 78 sylanbrc A B A < B F II Homeo J 𝑡 A B