# Metamath Proof Explorer

## Theorem ordtopn3

Description: An open interval ( A , B ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 ordttopon.3 ${⊢}{X}=\mathrm{dom}{R}$
2 inrab ${⊢}\left\{{x}\in {X}|¬{x}{R}{A}\right\}\cap \left\{{x}\in {X}|¬{B}{R}{x}\right\}=\left\{{x}\in {X}|\left(¬{x}{R}{A}\wedge ¬{B}{R}{x}\right)\right\}$
3 1 ordttopon ${⊢}{R}\in {V}\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
4 3 3ad2ant1 ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
5 topontop ${⊢}\mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{Top}$
6 4 5 syl ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{Top}$
7 1 ordtopn1 ${⊢}\left({R}\in {V}\wedge {A}\in {X}\right)\to \left\{{x}\in {X}|¬{x}{R}{A}\right\}\in \mathrm{ordTop}\left({R}\right)$
8 7 3adant3 ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left\{{x}\in {X}|¬{x}{R}{A}\right\}\in \mathrm{ordTop}\left({R}\right)$
9 1 ordtopn2 ${⊢}\left({R}\in {V}\wedge {B}\in {X}\right)\to \left\{{x}\in {X}|¬{B}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$
10 9 3adant2 ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left\{{x}\in {X}|¬{B}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$
11 inopn ${⊢}\left(\mathrm{ordTop}\left({R}\right)\in \mathrm{Top}\wedge \left\{{x}\in {X}|¬{x}{R}{A}\right\}\in \mathrm{ordTop}\left({R}\right)\wedge \left\{{x}\in {X}|¬{B}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)\right)\to \left\{{x}\in {X}|¬{x}{R}{A}\right\}\cap \left\{{x}\in {X}|¬{B}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$
12 6 8 10 11 syl3anc ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left\{{x}\in {X}|¬{x}{R}{A}\right\}\cap \left\{{x}\in {X}|¬{B}{R}{x}\right\}\in \mathrm{ordTop}\left({R}\right)$
13 2 12 eqeltrrid ${⊢}\left({R}\in {V}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left\{{x}\in {X}|\left(¬{x}{R}{A}\wedge ¬{B}{R}{x}\right)\right\}\in \mathrm{ordTop}\left({R}\right)$