# Metamath Proof Explorer

## Theorem ordtopn2

Description: A downward ray ( -oo , P ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 ${⊢}{X}=\mathrm{dom}{R}$
Assertion ordtopn2 ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 ordttopon.3 ${⊢}{X}=\mathrm{dom}{R}$
2 eqid ${⊢}\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)=\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)$
3 eqid ${⊢}\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)=\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
4 1 2 3 ordtuni ${⊢}{R}\in {V}\to {X}=\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)$
5 4 adantr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to {X}=\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)$
6 dmexg ${⊢}{R}\in {V}\to \mathrm{dom}{R}\in \mathrm{V}$
7 1 6 eqeltrid ${⊢}{R}\in {V}\to {X}\in \mathrm{V}$
8 7 adantr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to {X}\in \mathrm{V}$
9 5 8 eqeltrrd ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\in \mathrm{V}$
10 uniexb ${⊢}\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\in \mathrm{V}↔\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\in \mathrm{V}$
11 9 10 sylibr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\in \mathrm{V}$
12 ssfii ${⊢}\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\in \mathrm{V}\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\subseteq \mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)$
13 11 12 syl ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\subseteq \mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)$
14 fibas ${⊢}\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\in \mathrm{TopBases}$
15 bastg ${⊢}\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\in \mathrm{TopBases}\to \mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\right)$
16 14 15 ax-mp ${⊢}\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\right)$
17 13 16 sstrdi ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\right)$
18 1 2 3 ordtval ${⊢}{R}\in {V}\to \mathrm{ordTop}\left({R}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\right)$
19 18 adantr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \mathrm{ordTop}\left({R}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)\right)$
20 17 19 sseqtrrd ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\subseteq \mathrm{ordTop}\left({R}\right)$
21 ssun2 ${⊢}\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\subseteq \left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)$
22 ssun2 ${⊢}\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\subseteq \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
23 simpr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to {P}\in {X}$
24 eqidd ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{P}{R}{x}\right\}$
25 breq1 ${⊢}{y}={P}\to \left({y}{R}{x}↔{P}{R}{x}\right)$
26 25 notbid ${⊢}{y}={P}\to \left(¬{y}{R}{x}↔¬{P}{R}{x}\right)$
27 26 rabbidv ${⊢}{y}={P}\to \left\{{x}\in {X}|¬{y}{R}{x}\right\}=\left\{{x}\in {X}|¬{P}{R}{x}\right\}$
28 27 rspceeqv ${⊢}\left({P}\in {X}\wedge \left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{P}{R}{x}\right\}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{y}{R}{x}\right\}$
29 23 24 28 syl2anc ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{y}{R}{x}\right\}$
30 rabexg ${⊢}{X}\in \mathrm{V}\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{V}$
31 eqid ${⊢}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)=\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
32 31 elrnmpt ${⊢}\left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{V}\to \left(\left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
33 8 30 32 3syl ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left(\left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|¬{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
34 29 33 mpbird ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)$
35 22 34 sseldi ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)$
36 21 35 sseldi ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{x}{R}{y}\right\}\right)\cup \mathrm{ran}\left({y}\in {X}⟼\left\{{x}\in {X}|¬{y}{R}{x}\right\}\right)\right)\right)$
37 20 36 sseldd ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$