Metamath Proof Explorer


Theorem ordtrest

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 RPosetRelAVordTopRA×AordTopR𝑡A

Proof

Step Hyp Ref Expression
1 inex1g RPosetRelRA×AV
2 1 adantr RPosetRelAVRA×AV
3 eqid domRA×A=domRA×A
4 eqid ranxdomRA×AydomRA×A|¬yRA×Ax=ranxdomRA×AydomRA×A|¬yRA×Ax
5 eqid ranxdomRA×AydomRA×A|¬xRA×Ay=ranxdomRA×AydomRA×A|¬xRA×Ay
6 3 4 5 ordtval RA×AVordTopRA×A=topGenfidomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×Ay
7 2 6 syl RPosetRelAVordTopRA×A=topGenfidomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×Ay
8 ordttop RPosetRelordTopRTop
9 resttop ordTopRTopAVordTopR𝑡ATop
10 8 9 sylan RPosetRelAVordTopR𝑡ATop
11 eqid domR=domR
12 11 psssdm2 RPosetReldomRA×A=domRA
13 12 adantr RPosetRelAVdomRA×A=domRA
14 8 adantr RPosetRelAVordTopRTop
15 simpr RPosetRelAVAV
16 11 ordttopon RPosetRelordTopRTopOndomR
17 16 adantr RPosetRelAVordTopRTopOndomR
18 toponmax ordTopRTopOndomRdomRordTopR
19 17 18 syl RPosetRelAVdomRordTopR
20 elrestr ordTopRTopAVdomRordTopRdomRAordTopR𝑡A
21 14 15 19 20 syl3anc RPosetRelAVdomRAordTopR𝑡A
22 13 21 eqeltrd RPosetRelAVdomRA×AordTopR𝑡A
23 22 snssd RPosetRelAVdomRA×AordTopR𝑡A
24 13 rabeqdv RPosetRelAVydomRA×A|¬yRA×Ax=ydomRA|¬yRA×Ax
25 13 24 mpteq12dv RPosetRelAVxdomRA×AydomRA×A|¬yRA×Ax=xdomRAydomRA|¬yRA×Ax
26 25 rneqd RPosetRelAVranxdomRA×AydomRA×A|¬yRA×Ax=ranxdomRAydomRA|¬yRA×Ax
27 inrab2 ydomR|¬yRxA=ydomRA|¬yRx
28 simpr RPosetRelAVxdomRAydomRAydomRA
29 28 elin2d RPosetRelAVxdomRAydomRAyA
30 simpr RPosetRelAVxdomRAxdomRA
31 30 elin2d RPosetRelAVxdomRAxA
32 31 adantr RPosetRelAVxdomRAydomRAxA
33 brinxp yAxAyRxyRA×Ax
34 29 32 33 syl2anc RPosetRelAVxdomRAydomRAyRxyRA×Ax
35 34 notbid RPosetRelAVxdomRAydomRA¬yRx¬yRA×Ax
36 35 rabbidva RPosetRelAVxdomRAydomRA|¬yRx=ydomRA|¬yRA×Ax
37 27 36 eqtrid RPosetRelAVxdomRAydomR|¬yRxA=ydomRA|¬yRA×Ax
38 14 adantr RPosetRelAVxdomRAordTopRTop
39 15 adantr RPosetRelAVxdomRAAV
40 simpl RPosetRelAVRPosetRel
41 elinel1 xdomRAxdomR
42 11 ordtopn1 RPosetRelxdomRydomR|¬yRxordTopR
43 40 41 42 syl2an RPosetRelAVxdomRAydomR|¬yRxordTopR
44 elrestr ordTopRTopAVydomR|¬yRxordTopRydomR|¬yRxAordTopR𝑡A
45 38 39 43 44 syl3anc RPosetRelAVxdomRAydomR|¬yRxAordTopR𝑡A
46 37 45 eqeltrrd RPosetRelAVxdomRAydomRA|¬yRA×AxordTopR𝑡A
47 46 fmpttd RPosetRelAVxdomRAydomRA|¬yRA×Ax:domRAordTopR𝑡A
48 47 frnd RPosetRelAVranxdomRAydomRA|¬yRA×AxordTopR𝑡A
49 26 48 eqsstrd RPosetRelAVranxdomRA×AydomRA×A|¬yRA×AxordTopR𝑡A
50 13 rabeqdv RPosetRelAVydomRA×A|¬xRA×Ay=ydomRA|¬xRA×Ay
51 13 50 mpteq12dv RPosetRelAVxdomRA×AydomRA×A|¬xRA×Ay=xdomRAydomRA|¬xRA×Ay
52 51 rneqd RPosetRelAVranxdomRA×AydomRA×A|¬xRA×Ay=ranxdomRAydomRA|¬xRA×Ay
53 inrab2 ydomR|¬xRyA=ydomRA|¬xRy
54 brinxp xAyAxRyxRA×Ay
55 32 29 54 syl2anc RPosetRelAVxdomRAydomRAxRyxRA×Ay
56 55 notbid RPosetRelAVxdomRAydomRA¬xRy¬xRA×Ay
57 56 rabbidva RPosetRelAVxdomRAydomRA|¬xRy=ydomRA|¬xRA×Ay
58 53 57 eqtrid RPosetRelAVxdomRAydomR|¬xRyA=ydomRA|¬xRA×Ay
59 11 ordtopn2 RPosetRelxdomRydomR|¬xRyordTopR
60 40 41 59 syl2an RPosetRelAVxdomRAydomR|¬xRyordTopR
61 elrestr ordTopRTopAVydomR|¬xRyordTopRydomR|¬xRyAordTopR𝑡A
62 38 39 60 61 syl3anc RPosetRelAVxdomRAydomR|¬xRyAordTopR𝑡A
63 58 62 eqeltrrd RPosetRelAVxdomRAydomRA|¬xRA×AyordTopR𝑡A
64 63 fmpttd RPosetRelAVxdomRAydomRA|¬xRA×Ay:domRAordTopR𝑡A
65 64 frnd RPosetRelAVranxdomRAydomRA|¬xRA×AyordTopR𝑡A
66 52 65 eqsstrd RPosetRelAVranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡A
67 49 66 unssd RPosetRelAVranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡A
68 23 67 unssd RPosetRelAVdomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡A
69 tgfiss ordTopR𝑡ATopdomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡AtopGenfidomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡A
70 10 68 69 syl2anc RPosetRelAVtopGenfidomRA×AranxdomRA×AydomRA×A|¬yRA×AxranxdomRA×AydomRA×A|¬xRA×AyordTopR𝑡A
71 7 70 eqsstrd RPosetRelAVordTopRA×AordTopR𝑡A