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	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R \cap (A \times A)) \subseteq ordTop (R) ↾_{𝑡} A$

Proof

Step	Hyp	Ref	Expression
1		inex1g	$⊢ R \in PosetRel \to R \cap (A \times A) \in V$
2	1	adantr	$⊢ (R \in PosetRel \land A \in V) \to R \cap (A \times A) \in V$
3		eqid	$⊢ dom (R \cap (A \times A)) = dom (R \cap (A \times A))$
4		eqid	$⊢ ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) = ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\})$
5		eqid	$⊢ ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}) = ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\})$
6	3 4 5	ordtval	$⊢ R \cap (A \times A) \in V \to ordTop (R \cap (A \times A)) = topGen (fi (\{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}))))$
7	2 6	syl	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R \cap (A \times A)) = topGen (fi (\{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}))))$
8		ordttop	$⊢ R \in PosetRel \to ordTop (R) \in Top$
9		resttop	$⊢ (ordTop (R) \in Top \land A \in V) \to ordTop (R) ↾_{𝑡} A \in Top$
10	8 9	sylan	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R) ↾_{𝑡} A \in Top$
11		eqid	$⊢ dom R = dom R$
12	11	psssdm2	$⊢ R \in PosetRel \to dom (R \cap (A \times A)) = dom R \cap A$
13	12	adantr	$⊢ (R \in PosetRel \land A \in V) \to dom (R \cap (A \times A)) = dom R \cap A$
14	8	adantr	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R) \in Top$
15		simpr	$⊢ (R \in PosetRel \land A \in V) \to A \in V$
16	11	ordttopon	$⊢ R \in PosetRel \to ordTop (R) \in TopOn (dom R)$
17	16	adantr	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R) \in TopOn (dom R)$
18		toponmax	$⊢ ordTop (R) \in TopOn (dom R) \to dom R \in ordTop (R)$
19	17 18	syl	$⊢ (R \in PosetRel \land A \in V) \to dom R \in ordTop (R)$
20		elrestr	$⊢ (ordTop (R) \in Top \land A \in V \land dom R \in ordTop (R)) \to dom R \cap A \in (ordTop (R) ↾_{𝑡} A)$
21	14 15 19 20	syl3anc	$⊢ (R \in PosetRel \land A \in V) \to dom R \cap A \in (ordTop (R) ↾_{𝑡} A)$
22	13 21	eqeltrd	$⊢ (R \in PosetRel \land A \in V) \to dom (R \cap (A \times A)) \in (ordTop (R) ↾_{𝑡} A)$
23	22	snssd	$⊢ (R \in PosetRel \land A \in V) \to \{dom (R \cap (A \times A))\} \subseteq ordTop (R) ↾_{𝑡} A$
24	13	rabeqdv	$⊢ (R \in PosetRel \land A \in V) \to \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\} = \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\}$
25	13 24	mpteq12dv	$⊢ (R \in PosetRel \land A \in V) \to (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) = (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\})$
26	25	rneqd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) = ran (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\})$
27		inrab2	$⊢ \{y \in dom R \| \neg y R x\} \cap A = \{y \in (dom R \cap A) \| \neg y R x\}$
28		simpr	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to y \in (dom R \cap A)$
29	28	elin2d	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to y \in A$
30		simpr	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to x \in (dom R \cap A)$
31	30	elin2d	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to x \in A$
32	31	adantr	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to x \in A$
33		brinxp	$⊢ (y \in A \land x \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
34	29 32 33	syl2anc	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
35	34	notbid	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to (\neg y R x \leftrightarrow \neg y (R \cap (A \times A)) x)$
36	35	rabbidva	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in (dom R \cap A) \| \neg y R x\} = \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\}$
37	27 36	syl5eq	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg y R x\} \cap A = \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\}$
38	14	adantr	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to ordTop (R) \in Top$
39	15	adantr	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to A \in V$
40		simpl	$⊢ (R \in PosetRel \land A \in V) \to R \in PosetRel$
41		elinel1	$⊢ x \in (dom R \cap A) \to x \in dom R$
42	11	ordtopn1	$⊢ (R \in PosetRel \land x \in dom R) \to \{y \in dom R \| \neg y R x\} \in ordTop (R)$
43	40 41 42	syl2an	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg y R x\} \in ordTop (R)$
44		elrestr	$⊢ (ordTop (R) \in Top \land A \in V \land \{y \in dom R \| \neg y R x\} \in ordTop (R)) \to \{y \in dom R \| \neg y R x\} \cap A \in (ordTop (R) ↾_{𝑡} A)$
45	38 39 43 44	syl3anc	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg y R x\} \cap A \in (ordTop (R) ↾_{𝑡} A)$
46	37 45	eqeltrrd	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\} \in (ordTop (R) ↾_{𝑡} A)$
47	46	fmpttd	$⊢ (R \in PosetRel \land A \in V) \to (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\}) : dom R \cap A ⟶ ordTop (R) ↾_{𝑡} A$
48	47	frnd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg y (R \cap (A \times A)) x\}) \subseteq ordTop (R) ↾_{𝑡} A$
49	26 48	eqsstrd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \subseteq ordTop (R) ↾_{𝑡} A$
50	13	rabeqdv	$⊢ (R \in PosetRel \land A \in V) \to \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\} = \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\}$
51	13 50	mpteq12dv	$⊢ (R \in PosetRel \land A \in V) \to (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}) = (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\})$
52	51	rneqd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}) = ran (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\})$
53		inrab2	$⊢ \{y \in dom R \| \neg x R y\} \cap A = \{y \in (dom R \cap A) \| \neg x R y\}$
54		brinxp	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
55	32 29 54	syl2anc	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
56	55	notbid	$⊢ (((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \land y \in (dom R \cap A)) \to (\neg x R y \leftrightarrow \neg x (R \cap (A \times A)) y)$
57	56	rabbidva	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in (dom R \cap A) \| \neg x R y\} = \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\}$
58	53 57	syl5eq	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg x R y\} \cap A = \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\}$
59	11	ordtopn2	$⊢ (R \in PosetRel \land x \in dom R) \to \{y \in dom R \| \neg x R y\} \in ordTop (R)$
60	40 41 59	syl2an	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg x R y\} \in ordTop (R)$
61		elrestr	$⊢ (ordTop (R) \in Top \land A \in V \land \{y \in dom R \| \neg x R y\} \in ordTop (R)) \to \{y \in dom R \| \neg x R y\} \cap A \in (ordTop (R) ↾_{𝑡} A)$
62	38 39 60 61	syl3anc	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in dom R \| \neg x R y\} \cap A \in (ordTop (R) ↾_{𝑡} A)$
63	58 62	eqeltrrd	$⊢ ((R \in PosetRel \land A \in V) \land x \in (dom R \cap A)) \to \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\} \in (ordTop (R) ↾_{𝑡} A)$
64	63	fmpttd	$⊢ (R \in PosetRel \land A \in V) \to (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\}) : dom R \cap A ⟶ ordTop (R) ↾_{𝑡} A$
65	64	frnd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in (dom R \cap A) ⟼ \{y \in (dom R \cap A) \| \neg x (R \cap (A \times A)) y\}) \subseteq ordTop (R) ↾_{𝑡} A$
66	52 65	eqsstrd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}) \subseteq ordTop (R) ↾_{𝑡} A$
67	49 66	unssd	$⊢ (R \in PosetRel \land A \in V) \to ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\}) \subseteq ordTop (R) ↾_{𝑡} A$
68	23 67	unssd	$⊢ (R \in PosetRel \land A \in V) \to \{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\})) \subseteq ordTop (R) ↾_{𝑡} A$
69		tgfiss	$⊢ (ordTop (R) ↾_{𝑡} A \in Top \land \{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\})) \subseteq ordTop (R) ↾_{𝑡} A) \to topGen (fi (\{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\})))) \subseteq ordTop (R) ↾_{𝑡} A$
70	10 68 69	syl2anc	$⊢ (R \in PosetRel \land A \in V) \to topGen (fi (\{dom (R \cap (A \times A))\} \cup (ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg y (R \cap (A \times A)) x\}) \cup ran (x \in dom (R \cap (A \times A)) ⟼ \{y \in dom (R \cap (A \times A)) \| \neg x (R \cap (A \times A)) y\})))) \subseteq ordTop (R) ↾_{𝑡} A$
71	7 70	eqsstrd	$⊢ (R \in PosetRel \land A \in V) \to ordTop (R \cap (A \times A)) \subseteq ordTop (R) ↾_{𝑡} A$

Metamath Proof Explorer

Theorem ordtrest

Proof