# Metamath Proof Explorer

## Theorem ordtval

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

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

### Proof

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