Metamath Proof Explorer

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 = r ∈ V ⟼ topGen ⁡ fi ⁡ dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cordt class ordTop
1 vr setvar r
2 cvv class V
3 ctg class topGen
4 cfi class fi
5 1 cv setvar r
6 5 cdm class dom ⁡ r
7 6 csn class dom ⁡ r
8 vx setvar x
9 vy setvar y
10 9 cv setvar y
11 8 cv setvar x
12 10 11 5 wbr wff y r x
13 12 wn wff ¬ y r x
14 13 9 6 crab class y ∈ dom ⁡ r | ¬ y r x
15 8 6 14 cmpt class x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x
16 11 10 5 wbr wff x r y
17 16 wn wff ¬ x r y
18 17 9 6 crab class y ∈ dom ⁡ r | ¬ x r y
19 8 6 18 cmpt class x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
20 15 19 cun class x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
21 20 crn class ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
22 7 21 cun class dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
23 22 4 cfv class fi ⁡ dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
24 23 3 cfv class topGen ⁡ fi ⁡ dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
25 1 2 24 cmpt class r ∈ V ⟼ topGen ⁡ fi ⁡ dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y
26 0 25 wceq wff ordTop = r ∈ V ⟼ topGen ⁡ fi ⁡ dom ⁡ r ∪ ran ⁡ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ y r x ∪ x ∈ dom ⁡ r ⟼ y ∈ dom ⁡ r | ¬ x r y