Description: The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ordtrest | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inex1g | |
|
2 | 1 | adantr | |
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 3 4 5 | ordtval | |
7 | 2 6 | syl | |
8 | ordttop | |
|
9 | resttop | |
|
10 | 8 9 | sylan | |
11 | eqid | |
|
12 | 11 | psssdm2 | |
13 | 12 | adantr | |
14 | 8 | adantr | |
15 | simpr | |
|
16 | 11 | ordttopon | |
17 | 16 | adantr | |
18 | toponmax | |
|
19 | 17 18 | syl | |
20 | elrestr | |
|
21 | 14 15 19 20 | syl3anc | |
22 | 13 21 | eqeltrd | |
23 | 22 | snssd | |
24 | 13 | rabeqdv | |
25 | 13 24 | mpteq12dv | |
26 | 25 | rneqd | |
27 | inrab2 | |
|
28 | simpr | |
|
29 | 28 | elin2d | |
30 | simpr | |
|
31 | 30 | elin2d | |
32 | 31 | adantr | |
33 | brinxp | |
|
34 | 29 32 33 | syl2anc | |
35 | 34 | notbid | |
36 | 35 | rabbidva | |
37 | 27 36 | eqtrid | |
38 | 14 | adantr | |
39 | 15 | adantr | |
40 | simpl | |
|
41 | elinel1 | |
|
42 | 11 | ordtopn1 | |
43 | 40 41 42 | syl2an | |
44 | elrestr | |
|
45 | 38 39 43 44 | syl3anc | |
46 | 37 45 | eqeltrrd | |
47 | 46 | fmpttd | |
48 | 47 | frnd | |
49 | 26 48 | eqsstrd | |
50 | 13 | rabeqdv | |
51 | 13 50 | mpteq12dv | |
52 | 51 | rneqd | |
53 | inrab2 | |
|
54 | brinxp | |
|
55 | 32 29 54 | syl2anc | |
56 | 55 | notbid | |
57 | 56 | rabbidva | |
58 | 53 57 | eqtrid | |
59 | 11 | ordtopn2 | |
60 | 40 41 59 | syl2an | |
61 | elrestr | |
|
62 | 38 39 60 61 | syl3anc | |
63 | 58 62 | eqeltrrd | |
64 | 63 | fmpttd | |
65 | 64 | frnd | |
66 | 52 65 | eqsstrd | |
67 | 49 66 | unssd | |
68 | 23 67 | unssd | |
69 | tgfiss | |
|
70 | 10 68 69 | syl2anc | |
71 | 7 70 | eqsstrd | |