Definition df-ordt

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)

	Ref	Expression
Assertion	df-ordt	⊢ ordTop = ( 𝑟 ∈ V ↦ ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cordt	⊢ ordTop
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		ctg	⊢ topGen
4		cfi	⊢ fi
5	1	cv	⊢ 𝑟
6	5	cdm	⊢ dom 𝑟
7	6	csn	⊢ { dom 𝑟 }
8		vx	⊢ 𝑥
9		vy	⊢ 𝑦
10	9	cv	⊢ 𝑦
11	8	cv	⊢ 𝑥
12	10 11 5	wbr	⊢ 𝑦 𝑟 𝑥
13	12	wn	⊢ ¬ 𝑦 𝑟 𝑥
14	13 9 6	crab	⊢ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 }
15	8 6 14	cmpt	⊢ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } )
16	11 10 5	wbr	⊢ 𝑥 𝑟 𝑦
17	16	wn	⊢ ¬ 𝑥 𝑟 𝑦
18	17 9 6	crab	⊢ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 }
19	8 6 18	cmpt	⊢ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } )
20	15 19	cun	⊢ ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) )
21	20	crn	⊢ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) )
22	7 21	cun	⊢ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) )
23	22 4	cfv	⊢ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) )
24	23 3	cfv	⊢ ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) )
25	1 2 24	cmpt	⊢ ( 𝑟 ∈ V ↦ ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) )
26	0 25	wceq	⊢ ordTop = ( 𝑟 ∈ V ↦ ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) )