ordtrest2lem

	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	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))$

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		inrab2	$⊢ \{w \in X \| \neg w R z\} \cap A = \{w \in (X \cap A) \| \neg w R z\}$
6		sseqin2	$⊢ A \subseteq X \leftrightarrow X \cap A = A$
7	3 6	sylib	$⊢ φ \to X \cap A = A$
8	7	adantr	$⊢ (φ \land z \in X) \to X \cap A = A$
9	8	rabeqdv	$⊢ (φ \land z \in X) \to \{w \in (X \cap A) \| \neg w R z\} = \{w \in A \| \neg w R z\}$
10	5 9	eqtrid	$⊢ (φ \land z \in X) \to \{w \in X \| \neg w R z\} \cap A = \{w \in A \| \neg w R z\}$
11		inex1g	$⊢ R \in TosetRel \to R \cap (A \times A) \in V$
12	2 11	syl	$⊢ φ \to R \cap (A \times A) \in V$
13		eqid	$⊢ dom (R \cap (A \times A)) = dom (R \cap (A \times A))$
14	13	ordttopon	$⊢ R \cap (A \times A) \in V \to ordTop (R \cap (A \times A)) \in TopOn (dom (R \cap (A \times A)))$
15	12 14	syl	$⊢ φ \to ordTop (R \cap (A \times A)) \in TopOn (dom (R \cap (A \times A)))$
16		tsrps	$⊢ R \in TosetRel \to R \in PosetRel$
17	2 16	syl	$⊢ φ \to R \in PosetRel$
18	1	psssdm	$⊢ (R \in PosetRel \land A \subseteq X) \to dom (R \cap (A \times A)) = A$
19	17 3 18	syl2anc	$⊢ φ \to dom (R \cap (A \times A)) = A$
20	19	fveq2d	$⊢ φ \to TopOn (dom (R \cap (A \times A))) = TopOn (A)$
21	15 20	eleqtrd	$⊢ φ \to ordTop (R \cap (A \times A)) \in TopOn (A)$
22		toponmax	$⊢ ordTop (R \cap (A \times A)) \in TopOn (A) \to A \in ordTop (R \cap (A \times A))$
23	21 22	syl	$⊢ φ \to A \in ordTop (R \cap (A \times A))$
24	23	adantr	$⊢ (φ \land z \in X) \to A \in ordTop (R \cap (A \times A))$
25		rabid2	$⊢ A = \{w \in A \| \neg w R z\} \leftrightarrow \forall w \in A \neg w R z$
26		eleq1	$⊢ A = \{w \in A \| \neg w R z\} \to (A \in ordTop (R \cap (A \times A)) \leftrightarrow \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
27	25 26	sylbir	$⊢ \forall w \in A \neg w R z \to (A \in ordTop (R \cap (A \times A)) \leftrightarrow \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
28	24 27	syl5ibcom	$⊢ (φ \land z \in X) \to (\forall w \in A \neg w R z \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
29		dfrex2	$⊢ \exists w \in A w R z \leftrightarrow \neg \forall w \in A \neg w R z$
30		breq1	$⊢ w = x \to (w R z \leftrightarrow x R z)$
31	30	cbvrexvw	$⊢ \exists w \in A w R z \leftrightarrow \exists x \in A x R z$
32	29 31	bitr3i	$⊢ \neg \forall w \in A \neg w R z \leftrightarrow \exists x \in A x R z$
33		ordttop	$⊢ R \cap (A \times A) \in V \to ordTop (R \cap (A \times A)) \in Top$
34	12 33	syl	$⊢ φ \to ordTop (R \cap (A \times A)) \in Top$
35	34	adantr	$⊢ (φ \land z \in X) \to ordTop (R \cap (A \times A)) \in Top$
36		0opn	$⊢ ordTop (R \cap (A \times A)) \in Top \to \emptyset \in ordTop (R \cap (A \times A))$
37	35 36	syl	$⊢ (φ \land z \in X) \to \emptyset \in ordTop (R \cap (A \times A))$
38	37	adantr	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to \emptyset \in ordTop (R \cap (A \times A))$
39		eleq1	$⊢ \{w \in A \| \neg w R z\} = \emptyset \to (\{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)) \leftrightarrow \emptyset \in ordTop (R \cap (A \times A)))$
40	38 39	syl5ibrcom	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to (\{w \in A \| \neg w R z\} = \emptyset \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
41		rabn0	$⊢ \{w \in A \| \neg w R z\} \neq \emptyset \leftrightarrow \exists w \in A \neg w R z$
42		breq1	$⊢ w = y \to (w R z \leftrightarrow y R z)$
43	42	notbid	$⊢ w = y \to (\neg w R z \leftrightarrow \neg y R z)$
44	43	cbvrexvw	$⊢ \exists w \in A \neg w R z \leftrightarrow \exists y \in A \neg y R z$
45	41 44	bitri	$⊢ \{w \in A \| \neg w R z\} \neq \emptyset \leftrightarrow \exists y \in A \neg y R z$
46	2	ad3antrrr	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to R \in TosetRel$
47	3	ad2antrr	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to A \subseteq X$
48	47	sselda	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to y \in X$
49		simpllr	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to z \in X$
50	1	tsrlin	$⊢ (R \in TosetRel \land y \in X \land z \in X) \to (y R z \lor z R y)$
51	46 48 49 50	syl3anc	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to (y R z \lor z R y)$
52	51	ord	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to (\neg y R z \to z R y)$
53		an4	$⊢ ((x \in A \land x R z) \land (y \in A \land z R y)) \leftrightarrow ((x \in A \land y \in A) \land (x R z \land z R y))$
54		rabss	$⊢ \{z \in X \| (x R z \land z R y)\} \subseteq A \leftrightarrow \forall z \in X ((x R z \land z R y) \to z \in A)$
55	4 54	sylib	$⊢ (φ \land (x \in A \land y \in A)) \to \forall z \in X ((x R z \land z R y) \to z \in A)$
56	55	r19.21bi	$⊢ ((φ \land (x \in A \land y \in A)) \land z \in X) \to ((x R z \land z R y) \to z \in A)$
57	56	an32s	$⊢ ((φ \land z \in X) \land (x \in A \land y \in A)) \to ((x R z \land z R y) \to z \in A)$
58	57	impr	$⊢ ((φ \land z \in X) \land ((x \in A \land y \in A) \land (x R z \land z R y))) \to z \in A$
59	53 58	sylan2b	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to z \in A$
60		brinxp	$⊢ (w \in A \land z \in A) \to (w R z \leftrightarrow w (R \cap (A \times A)) z)$
61	60	ancoms	$⊢ (z \in A \land w \in A) \to (w R z \leftrightarrow w (R \cap (A \times A)) z)$
62	61	notbid	$⊢ (z \in A \land w \in A) \to (\neg w R z \leftrightarrow \neg w (R \cap (A \times A)) z)$
63	62	rabbidva	$⊢ z \in A \to \{w \in A \| \neg w R z\} = \{w \in A \| \neg w (R \cap (A \times A)) z\}$
64	59 63	syl	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to \{w \in A \| \neg w R z\} = \{w \in A \| \neg w (R \cap (A \times A)) z\}$
65	19	ad2antrr	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to dom (R \cap (A \times A)) = A$
66	65	rabeqdv	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to \{w \in dom (R \cap (A \times A)) \| \neg w (R \cap (A \times A)) z\} = \{w \in A \| \neg w (R \cap (A \times A)) z\}$
67	64 66	eqtr4d	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to \{w \in A \| \neg w R z\} = \{w \in dom (R \cap (A \times A)) \| \neg w (R \cap (A \times A)) z\}$
68	12	ad2antrr	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to R \cap (A \times A) \in V$
69	59 65	eleqtrrd	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to z \in dom (R \cap (A \times A))$
70	13	ordtopn1	$⊢ (R \cap (A \times A) \in V \land z \in dom (R \cap (A \times A))) \to \{w \in dom (R \cap (A \times A)) \| \neg w (R \cap (A \times A)) z\} \in ordTop (R \cap (A \times A))$
71	68 69 70	syl2anc	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to \{w \in dom (R \cap (A \times A)) \| \neg w (R \cap (A \times A)) z\} \in ordTop (R \cap (A \times A))$
72	67 71	eqeltrd	$⊢ ((φ \land z \in X) \land ((x \in A \land x R z) \land (y \in A \land z R y))) \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A))$
73	72	anassrs	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land (y \in A \land z R y)) \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A))$
74	73	expr	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to (z R y \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
75	52 74	syld	$⊢ (((φ \land z \in X) \land (x \in A \land x R z)) \land y \in A) \to (\neg y R z \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
76	75	rexlimdva	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to (\exists y \in A \neg y R z \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
77	45 76	biimtrid	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to (\{w \in A \| \neg w R z\} \neq \emptyset \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
78	40 77	pm2.61dne	$⊢ ((φ \land z \in X) \land (x \in A \land x R z)) \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A))$
79	78	rexlimdvaa	$⊢ (φ \land z \in X) \to (\exists x \in A x R z \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
80	32 79	biimtrid	$⊢ (φ \land z \in X) \to (\neg \forall w \in A \neg w R z \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A)))$
81	28 80	pm2.61d	$⊢ (φ \land z \in X) \to \{w \in A \| \neg w R z\} \in ordTop (R \cap (A \times A))$
82	10 81	eqeltrd	$⊢ (φ \land z \in X) \to \{w \in X \| \neg w R z\} \cap A \in ordTop (R \cap (A \times A))$
83	82	ralrimiva	$⊢ φ \to \forall z \in X \{w \in X \| \neg w R z\} \cap A \in ordTop (R \cap (A \times A))$
84	2	dmexd	$⊢ φ \to dom R \in V$
85	1 84	eqeltrid	$⊢ φ \to X \in V$
86		rabexg	$⊢ X \in V \to \{w \in X \| \neg w R z\} \in V$
87	85 86	syl	$⊢ φ \to \{w \in X \| \neg w R z\} \in V$
88	87	ralrimivw	$⊢ φ \to \forall z \in X \{w \in X \| \neg w R z\} \in V$
89		eqid	$⊢ (z \in X ⟼ \{w \in X \| \neg w R z\}) = (z \in X ⟼ \{w \in X \| \neg w R z\})$
90		ineq1	$⊢ v = \{w \in X \| \neg w R z\} \to v \cap A = \{w \in X \| \neg w R z\} \cap A$
91	90	eleq1d	$⊢ v = \{w \in X \| \neg w R z\} \to (v \cap A \in ordTop (R \cap (A \times A)) \leftrightarrow \{w \in X \| \neg w R z\} \cap A \in ordTop (R \cap (A \times A)))$
92	89 91	ralrnmptw	$⊢ \forall z \in X \{w \in X \| \neg w R z\} \in V \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)) \leftrightarrow \forall z \in X \{w \in X \| \neg w R z\} \cap A \in ordTop (R \cap (A \times A)))$
93	88 92	syl	$⊢ φ \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)) \leftrightarrow \forall z \in X \{w \in X \| \neg w R z\} \cap A \in ordTop (R \cap (A \times A)))$
94	83 93	mpbird	$⊢ φ \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))$

Metamath Proof Explorer

Theorem ordtrest2lem

Proof