Definition df-ordt 14755

Description: Define the order topology, given an order <_, written as r below. A closed subbasis for the order topology is given by the closed rays [ y , +oo ) = { z e. X | y <_ z } and ( -oo , y ] = { z e. X | z <_ y }, along with ( -oo , +oo ) = X itself. (Contributed by Mario Carneiro, 3-Sep-2015.)

Assertion

Ref	Expression
df-ordt	|- ordTop = ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )

Distinct variable group:   x, r, y

Detailed syntax breakdown of Definition df-ordt

Step	Hyp	Ref	Expression
1		cordt 14753	. 2 class ordTop
2		vr	. . 3 setvar r
3		cvv 3113	. . 3 class _V
4	2	cv 1378	. . . . . . . 8 class r
5	4	cdm 4999	. . . . . . 7 class dom r
6	5	csn 4027	. . . . . 6 class { dom r }
7		vx	. . . . . . . . 9 setvar x
8		vy	. . . . . . . . . . . . 13 setvar y
9	8	cv 1378	. . . . . . . . . . . 12 class y
10	7	cv 1378	. . . . . . . . . . . 12 class x
11	9, 10, 4	wbr 4447	. . . . . . . . . . 11 wff y r x
12	11	wn 3	. . . . . . . . . 10 wff -. y r x
13	12, 8, 5	crab 2818	. . . . . . . . 9 class { y e. dom r | -. y r x }
14	7, 5, 13	cmpt 4505	. . . . . . . 8 class ( x e. dom r |-> { y e. dom r | -. y r x } )
15	10, 9, 4	wbr 4447	. . . . . . . . . . 11 wff x r y
16	15	wn 3	. . . . . . . . . 10 wff -. x r y
17	16, 8, 5	crab 2818	. . . . . . . . 9 class { y e. dom r | -. x r y }
18	7, 5, 17	cmpt 4505	. . . . . . . 8 class ( x e. dom r |-> { y e. dom r | -. x r y } )
19	14, 18	cun 3474	. . . . . . 7 class ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) )
20	19	crn 5000	. . . . . 6 class ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) )
21	6, 20	cun 3474	. . . . 5 class ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) )
22		cfi 7869	. . . . 5 class fi
23	21, 22	cfv 5587	. . . 4 class ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) )
24		ctg 14692	. . . 4 class topGen
25	23, 24	cfv 5587	. . 3 class ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) )
26	2, 3, 25	cmpt 4505	. 2 class ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )
27	1, 26	wceq 1379	1 wff ordTop = ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )

This definition is referenced by:  ordtval  19472