Metamath Proof Explorer


Theorem ordtrest2

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrest2.1 X = dom R
ordtrest2.2 φ R TosetRel
ordtrest2.3 φ A X
ordtrest2.4 φ x A y A z X | x R z z R y A
Assertion ordtrest2 φ ordTop R A × A = ordTop R 𝑡 A

Proof

Step Hyp Ref Expression
1 ordtrest2.1 X = dom R
2 ordtrest2.2 φ R TosetRel
3 ordtrest2.3 φ A X
4 ordtrest2.4 φ x A y A z X | x R z z R y A
5 tsrps R TosetRel R PosetRel
6 2 5 syl φ R PosetRel
7 2 dmexd φ dom R V
8 1 7 eqeltrid φ X V
9 8 3 ssexd φ A V
10 ordtrest R PosetRel A V ordTop R A × A ordTop R 𝑡 A
11 6 9 10 syl2anc φ ordTop R A × A ordTop R 𝑡 A
12 eqid ran z X w X | ¬ w R z = ran z X w X | ¬ w R z
13 eqid ran z X w X | ¬ z R w = ran z X w X | ¬ z R w
14 1 12 13 ordtval R TosetRel ordTop R = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w
15 2 14 syl φ ordTop R = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w
16 15 oveq1d φ ordTop R 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
17 fibas fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w TopBases
18 tgrest fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w TopBases A V topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
19 17 9 18 sylancr φ topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
20 16 19 eqtr4d φ ordTop R 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
21 firest fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
22 21 fveq2i topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
23 20 22 syl6eqr φ ordTop R 𝑡 A = topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A
24 inex1g R TosetRel R A × A V
25 2 24 syl φ R A × A V
26 ordttop R A × A V ordTop R A × A Top
27 25 26 syl φ ordTop R A × A Top
28 1 12 13 ordtuni R TosetRel X = X ran z X w X | ¬ w R z ran z X w X | ¬ z R w
29 2 28 syl φ X = X ran z X w X | ¬ w R z ran z X w X | ¬ z R w
30 29 8 eqeltrrd φ X ran z X w X | ¬ w R z ran z X w X | ¬ z R w V
31 uniexb X ran z X w X | ¬ w R z ran z X w X | ¬ z R w V X ran z X w X | ¬ w R z ran z X w X | ¬ z R w V
32 30 31 sylibr φ X ran z X w X | ¬ w R z ran z X w X | ¬ z R w V
33 restval X ran z X w X | ¬ w R z ran z X w X | ¬ z R w V A V X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = ran v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A
34 32 9 33 syl2anc φ X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A = ran v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A
35 sseqin2 A X X A = A
36 3 35 sylib φ X A = A
37 eqid dom R A × A = dom R A × A
38 37 ordttopon R A × A V ordTop R A × A TopOn dom R A × A
39 25 38 syl φ ordTop R A × A TopOn dom R A × A
40 1 psssdm R PosetRel A X dom R A × A = A
41 6 3 40 syl2anc φ dom R A × A = A
42 41 fveq2d φ TopOn dom R A × A = TopOn A
43 39 42 eleqtrd φ ordTop R A × A TopOn A
44 toponmax ordTop R A × A TopOn A A ordTop R A × A
45 43 44 syl φ A ordTop R A × A
46 36 45 eqeltrd φ X A ordTop R A × A
47 elsni v X v = X
48 47 ineq1d v X v A = X A
49 48 eleq1d v X v A ordTop R A × A X A ordTop R A × A
50 46 49 syl5ibrcom φ v X v A ordTop R A × A
51 50 ralrimiv φ v X v A ordTop R A × A
52 1 2 3 4 ordtrest2lem φ v ran z X w X | ¬ w R z v A ordTop R A × A
53 df-rn ran R = dom R -1
54 cnvtsr R TosetRel R -1 TosetRel
55 2 54 syl φ R -1 TosetRel
56 1 psrn R PosetRel X = ran R
57 6 56 syl φ X = ran R
58 3 57 sseqtrd φ A ran R
59 57 adantr φ x A y A X = ran R
60 59 rabeqdv φ x A y A z X | x R z z R y = z ran R | x R z z R y
61 vex y V
62 vex z V
63 61 62 brcnv y R -1 z z R y
64 vex x V
65 62 64 brcnv z R -1 x x R z
66 63 65 anbi12ci y R -1 z z R -1 x x R z z R y
67 66 rabbii z ran R | y R -1 z z R -1 x = z ran R | x R z z R y
68 60 67 syl6eqr φ x A y A z X | x R z z R y = z ran R | y R -1 z z R -1 x
69 68 4 eqsstrrd φ x A y A z ran R | y R -1 z z R -1 x A
70 69 ancom2s φ y A x A z ran R | y R -1 z z R -1 x A
71 53 55 58 70 ordtrest2lem φ v ran z ran R w ran R | ¬ w R -1 z v A ordTop R -1 A × A
72 vex w V
73 72 62 brcnv w R -1 z z R w
74 73 bicomi z R w w R -1 z
75 74 a1i φ z R w w R -1 z
76 75 notbid φ ¬ z R w ¬ w R -1 z
77 57 76 rabeqbidv φ w X | ¬ z R w = w ran R | ¬ w R -1 z
78 57 77 mpteq12dv φ z X w X | ¬ z R w = z ran R w ran R | ¬ w R -1 z
79 78 rneqd φ ran z X w X | ¬ z R w = ran z ran R w ran R | ¬ w R -1 z
80 cnvin R A × A -1 = R -1 A × A -1
81 cnvxp A × A -1 = A × A
82 81 ineq2i R -1 A × A -1 = R -1 A × A
83 80 82 eqtri R A × A -1 = R -1 A × A
84 83 fveq2i ordTop R A × A -1 = ordTop R -1 A × A
85 psss R PosetRel R A × A PosetRel
86 6 85 syl φ R A × A PosetRel
87 ordtcnv R A × A PosetRel ordTop R A × A -1 = ordTop R A × A
88 86 87 syl φ ordTop R A × A -1 = ordTop R A × A
89 84 88 syl5reqr φ ordTop R A × A = ordTop R -1 A × A
90 89 eleq2d φ v A ordTop R A × A v A ordTop R -1 A × A
91 79 90 raleqbidv φ v ran z X w X | ¬ z R w v A ordTop R A × A v ran z ran R w ran R | ¬ w R -1 z v A ordTop R -1 A × A
92 71 91 mpbird φ v ran z X w X | ¬ z R w v A ordTop R A × A
93 ralunb v ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A v ran z X w X | ¬ w R z v A ordTop R A × A v ran z X w X | ¬ z R w v A ordTop R A × A
94 52 92 93 sylanbrc φ v ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A
95 ralunb v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A v X v A ordTop R A × A v ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A
96 51 94 95 sylanbrc φ v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A
97 eqid v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A = v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A
98 97 fmpt v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A : X ran z X w X | ¬ w R z ran z X w X | ¬ z R w ordTop R A × A
99 96 98 sylib φ v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A : X ran z X w X | ¬ w R z ran z X w X | ¬ z R w ordTop R A × A
100 99 frnd φ ran v X ran z X w X | ¬ w R z ran z X w X | ¬ z R w v A ordTop R A × A
101 34 100 eqsstrd φ X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A ordTop R A × A
102 tgfiss ordTop R A × A Top X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A ordTop R A × A topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A ordTop R A × A
103 27 101 102 syl2anc φ topGen fi X ran z X w X | ¬ w R z ran z X w X | ¬ z R w 𝑡 A ordTop R A × A
104 23 103 eqsstrd φ ordTop R 𝑡 A ordTop R A × A
105 11 104 eqssd φ ordTop R A × A = ordTop R 𝑡 A