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 eqtr4di ⊢ φ → 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 eqtr4di ⊢ φ ∧ 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 psss ⊢ R ∈ PosetRel → R ∩ A × A ∈ PosetRel
81 6 80 syl ⊢ φ → R ∩ A × A ∈ PosetRel
82 ordtcnv ⊢ R ∩ A × A ∈ PosetRel → ordTop ⁡ R ∩ A × A -1 = ordTop ⁡ R ∩ A × A
83 81 82 syl ⊢ φ → ordTop ⁡ R ∩ A × A -1 = ordTop ⁡ R ∩ A × A
84 cnvin ⊢ R ∩ A × A -1 = R -1 ∩ A × A -1
85 cnvxp ⊢ A × A -1 = A × A
86 85 ineq2i ⊢ R -1 ∩ A × A -1 = R -1 ∩ A × A
87 84 86 eqtri ⊢ R ∩ A × A -1 = R -1 ∩ A × A
88 87 fveq2i ⊢ ordTop ⁡ R ∩ A × A -1 = ordTop ⁡ R -1 ∩ A × A
89 83 88 eqtr3di ⊢ φ → 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