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	$⊢ φ \to R \in TosetRel$
	ordtrest2.3	$⊢ φ \to A \subseteq X$
	ordtrest2.4	$⊢ (φ \land (x \in A \land y \in A)) \to \{z \in X \| (x R z \land z R y)\} \subseteq A$
Assertion	ordtrest2	$⊢ φ \to ordTop (R \cap (A \times A)) = ordTop (R) ↾_{𝑡} A$

Proof

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

Metamath Proof Explorer

Theorem ordtrest2

Proof