# Metamath Proof Explorer

## Theorem ordtcld2

Description: An upward ray [ P , +oo ) is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 ordttopon.3 ${⊢}{X}=\mathrm{dom}{R}$
2 ssrab2 ${⊢}\left\{{x}\in {X}|{P}{R}{x}\right\}\subseteq {X}$
3 1 ordttopon ${⊢}{R}\in {V}\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
4 3 adantr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
5 toponuni ${⊢}\mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup \mathrm{ordTop}\left({R}\right)$
6 4 5 syl ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to {X}=\bigcup \mathrm{ordTop}\left({R}\right)$
7 2 6 sseqtrid ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|{P}{R}{x}\right\}\subseteq \bigcup \mathrm{ordTop}\left({R}\right)$
8 notrab ${⊢}{X}\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}=\left\{{x}\in {X}|¬{P}{R}{x}\right\}$
9 6 difeq1d ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to {X}\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}=\bigcup \mathrm{ordTop}\left({R}\right)\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}$
10 8 9 syl5eqr ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|¬{P}{R}{x}\right\}=\bigcup \mathrm{ordTop}\left({R}\right)\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}$
11 1 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)$
12 10 11 eqeltrrd ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \bigcup \mathrm{ordTop}\left({R}\right)\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$
13 topontop ${⊢}\mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{Top}$
14 eqid ${⊢}\bigcup \mathrm{ordTop}\left({R}\right)=\bigcup \mathrm{ordTop}\left({R}\right)$
15 14 iscld ${⊢}\mathrm{ordTop}\left({R}\right)\in \mathrm{Top}\to \left(\left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{Clsd}\left(\mathrm{ordTop}\left({R}\right)\right)↔\left(\left\{{x}\in {X}|{P}{R}{x}\right\}\subseteq \bigcup \mathrm{ordTop}\left({R}\right)\wedge \bigcup \mathrm{ordTop}\left({R}\right)\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)\right)\right)$
16 4 13 15 3syl ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left(\left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{Clsd}\left(\mathrm{ordTop}\left({R}\right)\right)↔\left(\left\{{x}\in {X}|{P}{R}{x}\right\}\subseteq \bigcup \mathrm{ordTop}\left({R}\right)\wedge \bigcup \mathrm{ordTop}\left({R}\right)\setminus \left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)\right)\right)$
17 7 12 16 mpbir2and ${⊢}\left({R}\in {V}\wedge {P}\in {X}\right)\to \left\{{x}\in {X}|{P}{R}{x}\right\}\in \mathrm{Clsd}\left(\mathrm{ordTop}\left({R}\right)\right)$