ordtcnv

Description: The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	ordtcnv	$⊢ R \in PosetRel \to ordTop (R^{-1}) = ordTop (R)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ dom R = dom R$
2	1	psrn	$⊢ R \in PosetRel \to dom R = ran R$
3	2	eqcomd	$⊢ R \in PosetRel \to ran R = dom R$
4	3	sneqd	$⊢ R \in PosetRel \to \{ran R\} = \{dom R\}$
5		vex	$⊢ y \in V$
6		vex	$⊢ x \in V$
7	5 6	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
8	7	a1i	$⊢ R \in PosetRel \to (y R^{-1} x \leftrightarrow x R y)$
9	8	notbid	$⊢ R \in PosetRel \to (\neg y R^{-1} x \leftrightarrow \neg x R y)$
10	3 9	rabeqbidv	$⊢ R \in PosetRel \to \{y \in ran R \| \neg y R^{-1} x\} = \{y \in dom R \| \neg x R y\}$
11	3 10	mpteq12dv	$⊢ R \in PosetRel \to (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) = (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})$
12	11	rneqd	$⊢ R \in PosetRel \to ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})$
13	6 5	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
14	13	a1i	$⊢ R \in PosetRel \to (x R^{-1} y \leftrightarrow y R x)$
15	14	notbid	$⊢ R \in PosetRel \to (\neg x R^{-1} y \leftrightarrow \neg y R x)$
16	3 15	rabeqbidv	$⊢ R \in PosetRel \to \{y \in ran R \| \neg x R^{-1} y\} = \{y \in dom R \| \neg y R x\}$
17	3 16	mpteq12dv	$⊢ R \in PosetRel \to (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}) = (x \in dom R ⟼ \{y \in dom R \| \neg y R x\})$
18	17	rneqd	$⊢ R \in PosetRel \to ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\})$
19	12 18	uneq12d	$⊢ R \in PosetRel \to ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\})$
20		uncom	$⊢ ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})$
21	19 20	syl6eq	$⊢ R \in PosetRel \to ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})$
22	4 21	uneq12d	$⊢ R \in PosetRel \to \{ran R\} \cup (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\})) = \{dom R\} \cup (ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}))$
23	22	fveq2d	$⊢ R \in PosetRel \to fi (\{ran R\} \cup (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}))) = fi (\{dom R\} \cup (ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})))$
24	23	fveq2d	$⊢ R \in PosetRel \to topGen (fi (\{ran R\} \cup (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\})))) = topGen (fi (\{dom R\} \cup (ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}))))$
25		cnvps	$⊢ R \in PosetRel \to R^{-1} \in PosetRel$
26		df-rn	$⊢ ran R = dom R^{-1}$
27		eqid	$⊢ ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
28		eqid	$⊢ ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}) = ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\})$
29	26 27 28	ordtval	$⊢ R^{-1} \in PosetRel \to ordTop (R^{-1}) = topGen (fi (\{ran R\} \cup (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}))))$
30	25 29	syl	$⊢ R \in PosetRel \to ordTop (R^{-1}) = topGen (fi (\{ran R\} \cup (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) \cup ran (x \in ran R ⟼ \{y \in ran R \| \neg x R^{-1} y\}))))$
31		eqid	$⊢ ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\})$
32		eqid	$⊢ ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}) = ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\})$
33	1 31 32	ordtval	$⊢ R \in PosetRel \to ordTop (R) = topGen (fi (\{dom R\} \cup (ran (x \in dom R ⟼ \{y \in dom R \| \neg y R x\}) \cup ran (x \in dom R ⟼ \{y \in dom R \| \neg x R y\}))))$
34	24 30 33	3eqtr4d	$⊢ R \in PosetRel \to ordTop (R^{-1}) = ordTop (R)$

Metamath Proof Explorer

Theorem ordtcnv

Proof