ordtval

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	ordtval.1	$⊢ X = dom R$
	ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
	ordtval.3	$⊢ B = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
Assertion	ordtval	$⊢ R \in V \to ordTop (R) = topGen (fi (\{X\} \cup (A \cup B)))$

Proof

Step	Hyp	Ref	Expression
1		ordtval.1	$⊢ X = dom R$
2		ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
3		ordtval.3	$⊢ B = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
4		elex	$⊢ R \in V \to R \in V$
5		dmeq	$⊢ r = R \to dom r = dom R$
6	5 1	eqtr4di	$⊢ r = R \to dom r = X$
7	6	sneqd	$⊢ r = R \to \{dom r\} = \{X\}$
8		rnun	$⊢ ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r 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\})$
9		breq	$⊢ r = R \to (y r x \leftrightarrow y R x)$
10	9	notbid	$⊢ r = R \to (\neg y r x \leftrightarrow \neg y R x)$
11	6 10	rabeqbidv	$⊢ r = R \to \{y \in dom r \| \neg y r x\} = \{y \in X \| \neg y R x\}$
12	6 11	mpteq12dv	$⊢ r = R \to (x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) = (x \in X ⟼ \{y \in X \| \neg y R x\})$
13	12	rneqd	$⊢ r = R \to ran (x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
14	13 2	eqtr4di	$⊢ r = R \to ran (x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) = A$
15		breq	$⊢ r = R \to (x r y \leftrightarrow x R y)$
16	15	notbid	$⊢ r = R \to (\neg x r y \leftrightarrow \neg x R y)$
17	6 16	rabeqbidv	$⊢ r = R \to \{y \in dom r \| \neg x r y\} = \{y \in X \| \neg x R y\}$
18	6 17	mpteq12dv	$⊢ r = R \to (x \in dom r ⟼ \{y \in dom r \| \neg x r y\}) = (x \in X ⟼ \{y \in X \| \neg x R y\})$
19	18	rneqd	$⊢ r = R \to ran (x \in dom r ⟼ \{y \in dom r \| \neg x r y\}) = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
20	19 3	eqtr4di	$⊢ r = R \to ran (x \in dom r ⟼ \{y \in dom r \| \neg x r y\}) = B$
21	14 20	uneq12d	$⊢ r = R \to 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\}) = A \cup B$
22	8 21	syl5eq	$⊢ r = R \to ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r y\})) = A \cup B$
23	7 22	uneq12d	$⊢ r = R \to \{dom r\} \cup ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r y\})) = \{X\} \cup (A \cup B)$
24	23	fveq2d	$⊢ r = R \to fi (\{dom r\} \cup ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r y\}))) = fi (\{X\} \cup (A \cup B))$
25	24	fveq2d	$⊢ r = R \to topGen (fi (\{dom r\} \cup ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r y\})))) = topGen (fi (\{X\} \cup (A \cup B)))$
26		df-ordt	$⊢ ordTop = (r \in V ⟼ topGen (fi (\{dom r\} \cup ran ((x \in dom r ⟼ \{y \in dom r \| \neg y r x\}) \cup (x \in dom r ⟼ \{y \in dom r \| \neg x r y\})))))$
27		fvex	$⊢ topGen (fi (\{X\} \cup (A \cup B))) \in V$
28	25 26 27	fvmpt	$⊢ R \in V \to ordTop (R) = topGen (fi (\{X\} \cup (A \cup B)))$
29	4 28	syl	$⊢ R \in V \to ordTop (R) = topGen (fi (\{X\} \cup (A \cup B)))$

Metamath Proof Explorer

Theorem ordtval

Proof