ordtrestNEW

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) (Revised by Thierry Arnoux, 11-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	$⊢ B = {Base}_{K}$
	ordtNEW.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
Assertion	ordtrestNEW	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq} \cap (A \times A)) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	$⊢ B = {Base}_{K}$
2		ordtNEW.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
3		fvex	$⊢ \leq_{K} \in V$
4	3	inex1	$⊢ \leq_{K} \cap (B \times B) \in V$
5	2 4	eqeltri	$⊢ \underset{˙}{\leq} \in V$
6	5	inex1	$⊢ \underset{˙}{\leq} \cap (A \times A) \in V$
7		eqid	$⊢ dom (\underset{˙}{\leq} \cap (A \times A)) = dom (\underset{˙}{\leq} \cap (A \times A))$
8		eqid	$⊢ ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) = ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\})$
9		eqid	$⊢ ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) = ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})$
10	7 8 9	ordtval	$⊢ \underset{˙}{\leq} \cap (A \times A) \in V \to ordTop (\underset{˙}{\leq} \cap (A \times A)) = topGen (fi (\{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}))))$
11	6 10	mp1i	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq} \cap (A \times A)) = topGen (fi (\{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}))))$
12		ordttop	$⊢ \underset{˙}{\leq} \in V \to ordTop (\underset{˙}{\leq}) \in Top$
13	5 12	ax-mp	$⊢ ordTop (\underset{˙}{\leq}) \in Top$
14		fvex	$⊢ {Base}_{K} \in V$
15	1 14	eqeltri	$⊢ B \in V$
16	15	ssex	$⊢ A \subseteq B \to A \in V$
17		resttop	$⊢ (ordTop (\underset{˙}{\leq}) \in Top \land A \in V) \to ordTop (\underset{˙}{\leq}) ↾_{𝑡} A \in Top$
18	13 16 17	sylancr	$⊢ A \subseteq B \to ordTop (\underset{˙}{\leq}) ↾_{𝑡} A \in Top$
19	18	adantl	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq}) ↾_{𝑡} A \in Top$
20	1	ressprs	$⊢ (K \in Proset \land A \subseteq B) \to K ↾_{𝑠} A \in Proset$
21		eqid	$⊢ {Base}_{(K ↾_{𝑠} A)} = {Base}_{(K ↾_{𝑠} A)}$
22		eqid	$⊢ \leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)}) = \leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})$
23	21 22	prsdm	$⊢ K ↾_{𝑠} A \in Proset \to dom (\leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})) = {Base}_{(K ↾_{𝑠} A)}$
24	20 23	syl	$⊢ (K \in Proset \land A \subseteq B) \to dom (\leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})) = {Base}_{(K ↾_{𝑠} A)}$
25		eqid	$⊢ K ↾_{𝑠} A = K ↾_{𝑠} A$
26	25 1	ressbas2	$⊢ A \subseteq B \to A = {Base}_{(K ↾_{𝑠} A)}$
27		fvex	$⊢ {Base}_{(K ↾_{𝑠} A)} \in V$
28	26 27	eqeltrdi	$⊢ A \subseteq B \to A \in V$
29		eqid	$⊢ \leq_{K} = \leq_{K}$
30	25 29	ressle	$⊢ A \in V \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
31	28 30	syl	$⊢ A \subseteq B \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
32	31	adantl	$⊢ (K \in Proset \land A \subseteq B) \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
33	26	adantl	$⊢ (K \in Proset \land A \subseteq B) \to A = {Base}_{(K ↾_{𝑠} A)}$
34	33	sqxpeqd	$⊢ (K \in Proset \land A \subseteq B) \to A \times A = {Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)}$
35	32 34	ineq12d	$⊢ (K \in Proset \land A \subseteq B) \to \leq_{K} \cap (A \times A) = \leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})$
36	35	dmeqd	$⊢ (K \in Proset \land A \subseteq B) \to dom (\leq_{K} \cap (A \times A)) = dom (\leq_{(K ↾_{𝑠} A)} \cap ({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)}))$
37	24 36 33	3eqtr4d	$⊢ (K \in Proset \land A \subseteq B) \to dom (\leq_{K} \cap (A \times A)) = A$
38	1 2	prsss	$⊢ (K \in Proset \land A \subseteq B) \to \underset{˙}{\leq} \cap (A \times A) = \leq_{K} \cap (A \times A)$
39	38	dmeqd	$⊢ (K \in Proset \land A \subseteq B) \to dom (\underset{˙}{\leq} \cap (A \times A)) = dom (\leq_{K} \cap (A \times A))$
40	1 2	prsdm	$⊢ K \in Proset \to dom \underset{˙}{\leq} = B$
41	40	sseq2d	$⊢ K \in Proset \to (A \subseteq dom \underset{˙}{\leq} \leftrightarrow A \subseteq B)$
42	41	biimpar	$⊢ (K \in Proset \land A \subseteq B) \to A \subseteq dom \underset{˙}{\leq}$
43		sseqin2	$⊢ A \subseteq dom \underset{˙}{\leq} \leftrightarrow dom \underset{˙}{\leq} \cap A = A$
44	42 43	sylib	$⊢ (K \in Proset \land A \subseteq B) \to dom \underset{˙}{\leq} \cap A = A$
45	37 39 44	3eqtr4d	$⊢ (K \in Proset \land A \subseteq B) \to dom (\underset{˙}{\leq} \cap (A \times A)) = dom \underset{˙}{\leq} \cap A$
46	5 12	mp1i	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq}) \in Top$
47	16	adantl	$⊢ (K \in Proset \land A \subseteq B) \to A \in V$
48		eqid	$⊢ dom \underset{˙}{\leq} = dom \underset{˙}{\leq}$
49	48	ordttopon	$⊢ \underset{˙}{\leq} \in V \to ordTop (\underset{˙}{\leq}) \in TopOn (dom \underset{˙}{\leq})$
50	5 49	mp1i	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq}) \in TopOn (dom \underset{˙}{\leq})$
51		toponmax	$⊢ ordTop (\underset{˙}{\leq}) \in TopOn (dom \underset{˙}{\leq}) \to dom \underset{˙}{\leq} \in ordTop (\underset{˙}{\leq})$
52	50 51	syl	$⊢ (K \in Proset \land A \subseteq B) \to dom \underset{˙}{\leq} \in ordTop (\underset{˙}{\leq})$
53		elrestr	$⊢ (ordTop (\underset{˙}{\leq}) \in Top \land A \in V \land dom \underset{˙}{\leq} \in ordTop (\underset{˙}{\leq})) \to dom \underset{˙}{\leq} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
54	46 47 52 53	syl3anc	$⊢ (K \in Proset \land A \subseteq B) \to dom \underset{˙}{\leq} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
55	45 54	eqeltrd	$⊢ (K \in Proset \land A \subseteq B) \to dom (\underset{˙}{\leq} \cap (A \times A)) \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
56	55	snssd	$⊢ (K \in Proset \land A \subseteq B) \to \{dom (\underset{˙}{\leq} \cap (A \times A))\} \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
57		rabeq	$⊢ dom (\underset{˙}{\leq} \cap (A \times A)) = dom \underset{˙}{\leq} \cap A \to \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}$
58	45 57	syl	$⊢ (K \in Proset \land A \subseteq B) \to \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}$
59	45 58	mpteq12dv	$⊢ (K \in Proset \land A \subseteq B) \to (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) = (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\})$
60	59	rneqd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) = ran (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\})$
61		inrab2	$⊢ \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \cap A = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y \underset{˙}{\leq} x\}$
62		inss2	$⊢ dom \underset{˙}{\leq} \cap A \subseteq A$
63		simpr	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to y \in (dom \underset{˙}{\leq} \cap A)$
64	62 63	sseldi	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to y \in A$
65		simpr	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to x \in (dom \underset{˙}{\leq} \cap A)$
66	62 65	sseldi	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to x \in A$
67	66	adantr	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to x \in A$
68		brinxp	$⊢ (y \in A \land x \in A) \to (y \underset{˙}{\leq} x \leftrightarrow y (\underset{˙}{\leq} \cap (A \times A)) x)$
69	64 67 68	syl2anc	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to (y \underset{˙}{\leq} x \leftrightarrow y (\underset{˙}{\leq} \cap (A \times A)) x)$
70	69	notbid	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to (\neg y \underset{˙}{\leq} x \leftrightarrow \neg y (\underset{˙}{\leq} \cap (A \times A)) x)$
71	70	rabbidva	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y \underset{˙}{\leq} x\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}$
72	61 71	syl5eq	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \cap A = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}$
73	5 12	mp1i	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to ordTop (\underset{˙}{\leq}) \in Top$
74	47	adantr	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to A \in V$
75		simpl	$⊢ (K \in Proset \land A \subseteq B) \to K \in Proset$
76		inss1	$⊢ dom \underset{˙}{\leq} \cap A \subseteq dom \underset{˙}{\leq}$
77	76	sseli	$⊢ x \in (dom \underset{˙}{\leq} \cap A) \to x \in dom \underset{˙}{\leq}$
78	48	ordtopn1	$⊢ (\underset{˙}{\leq} \in V \land x \in dom \underset{˙}{\leq}) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \in ordTop (\underset{˙}{\leq})$
79	5 78	mpan	$⊢ x \in dom \underset{˙}{\leq} \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \in ordTop (\underset{˙}{\leq})$
80	79	adantl	$⊢ (K \in Proset \land x \in dom \underset{˙}{\leq}) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \in ordTop (\underset{˙}{\leq})$
81	75 77 80	syl2an	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \in ordTop (\underset{˙}{\leq})$
82		elrestr	$⊢ (ordTop (\underset{˙}{\leq}) \in Top \land A \in V \land \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \in ordTop (\underset{˙}{\leq})) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
83	73 74 81 82	syl3anc	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg y \underset{˙}{\leq} x\} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
84	72 83	eqeltrrd	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\} \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
85	84	fmpttd	$⊢ (K \in Proset \land A \subseteq B) \to (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) : dom \underset{˙}{\leq} \cap A ⟶ ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
86	85	frnd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
87	60 86	eqsstrd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
88		rabeq	$⊢ dom (\underset{˙}{\leq} \cap (A \times A)) = dom \underset{˙}{\leq} \cap A \to \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}$
89	45 88	syl	$⊢ (K \in Proset \land A \subseteq B) \to \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}$
90	45 89	mpteq12dv	$⊢ (K \in Proset \land A \subseteq B) \to (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) = (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})$
91	90	rneqd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) = ran (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})$
92		inrab2	$⊢ \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \cap A = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x \underset{˙}{\leq} y\}$
93		brinxp	$⊢ (x \in A \land y \in A) \to (x \underset{˙}{\leq} y \leftrightarrow x (\underset{˙}{\leq} \cap (A \times A)) y)$
94	67 64 93	syl2anc	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to (x \underset{˙}{\leq} y \leftrightarrow x (\underset{˙}{\leq} \cap (A \times A)) y)$
95	94	notbid	$⊢ (((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \land y \in (dom \underset{˙}{\leq} \cap A)) \to (\neg x \underset{˙}{\leq} y \leftrightarrow \neg x (\underset{˙}{\leq} \cap (A \times A)) y)$
96	95	rabbidva	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x \underset{˙}{\leq} y\} = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}$
97	92 96	syl5eq	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \cap A = \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}$
98	48	ordtopn2	$⊢ (\underset{˙}{\leq} \in V \land x \in dom \underset{˙}{\leq}) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \in ordTop (\underset{˙}{\leq})$
99	5 98	mpan	$⊢ x \in dom \underset{˙}{\leq} \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \in ordTop (\underset{˙}{\leq})$
100	99	adantl	$⊢ (K \in Proset \land x \in dom \underset{˙}{\leq}) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \in ordTop (\underset{˙}{\leq})$
101	75 77 100	syl2an	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \in ordTop (\underset{˙}{\leq})$
102		elrestr	$⊢ (ordTop (\underset{˙}{\leq}) \in Top \land A \in V \land \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \in ordTop (\underset{˙}{\leq})) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
103	73 74 101 102	syl3anc	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in dom \underset{˙}{\leq} \| \neg x \underset{˙}{\leq} y\} \cap A \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
104	97 103	eqeltrrd	$⊢ ((K \in Proset \land A \subseteq B) \land x \in (dom \underset{˙}{\leq} \cap A)) \to \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\} \in (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A)$
105	104	fmpttd	$⊢ (K \in Proset \land A \subseteq B) \to (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) : dom \underset{˙}{\leq} \cap A ⟶ ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
106	105	frnd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in (dom \underset{˙}{\leq} \cap A) ⟼ \{y \in (dom \underset{˙}{\leq} \cap A) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
107	91 106	eqsstrd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
108	87 107	unssd	$⊢ (K \in Proset \land A \subseteq B) \to ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\}) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
109	56 108	unssd	$⊢ (K \in Proset \land A \subseteq B) \to \{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
110		tgfiss	$⊢ (ordTop (\underset{˙}{\leq}) ↾_{𝑡} A \in Top \land \{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A) \to topGen (fi (\{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})))) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
111	19 109 110	syl2anc	$⊢ (K \in Proset \land A \subseteq B) \to topGen (fi (\{dom (\underset{˙}{\leq} \cap (A \times A))\} \cup (ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg y (\underset{˙}{\leq} \cap (A \times A)) x\}) \cup ran (x \in dom (\underset{˙}{\leq} \cap (A \times A)) ⟼ \{y \in dom (\underset{˙}{\leq} \cap (A \times A)) \| \neg x (\underset{˙}{\leq} \cap (A \times A)) y\})))) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$
112	11 111	eqsstrd	$⊢ (K \in Proset \land A \subseteq B) \to ordTop (\underset{˙}{\leq} \cap (A \times A)) \subseteq ordTop (\underset{˙}{\leq}) ↾_{𝑡} A$

Metamath Proof Explorer

Theorem ordtrestNEW

Proof