Theorem ordtopn3

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

	Ref	Expression
Hypothesis	ordttopon.3	|- X = dom R
Assertion	ordtopn3	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( -. x R A /\ -. B R x ) } e. ( ordTop ` R ) )

Proof

Step	Hyp	Ref	Expression
1		ordttopon.3	|- X = dom R
2		inrab	|- ( { x e. X | -. x R A } i^i { x e. X | -. B R x } ) = { x e. X | ( -. x R A /\ -. B R x ) }
3	1	ordttopon	|- ( R e. V -> ( ordTop ` R ) e. ( TopOn ` X ) )
4	3	3ad2ant1	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( ordTop ` R ) e. ( TopOn ` X ) )
5		topontop	|- ( ( ordTop ` R ) e. ( TopOn ` X ) -> ( ordTop ` R ) e. Top )
6	4 5	syl	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( ordTop ` R ) e. Top )
7	1	ordtopn1	|- ( ( R e. V /\ A e. X ) -> { x e. X | -. x R A } e. ( ordTop ` R ) )
8	7	3adant3	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | -. x R A } e. ( ordTop ` R ) )
9	1	ordtopn2	|- ( ( R e. V /\ B e. X ) -> { x e. X | -. B R x } e. ( ordTop ` R ) )
10	9	3adant2	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | -. B R x } e. ( ordTop ` R ) )
11		inopn	|- ( ( ( ordTop ` R ) e. Top /\ { x e. X | -. x R A } e. ( ordTop ` R ) /\ { x e. X | -. B R x } e. ( ordTop ` R ) ) -> ( { x e. X | -. x R A } i^i { x e. X | -. B R x } ) e. ( ordTop ` R ) )
12	6 8 10 11	syl3anc	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( { x e. X | -. x R A } i^i { x e. X | -. B R x } ) e. ( ordTop ` R ) )
13	2 12	eqeltrrid	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( -. x R A /\ -. B R x ) } e. ( ordTop ` R ) )