Definition df-ordt 17006

Description: Define the order topology, given an order ≤, written as 𝑟 below. A closed subbasis for the order topology is given by the closed rays [𝑦, +∞) = {𝑧 ∈ 𝑋 ∣ 𝑦 ≤ 𝑧} and (-∞, 𝑦] = {𝑧 ∈ 𝑋 ∣ 𝑧 ≤ 𝑦}, along with (-∞, +∞) = 𝑋 itself. (Contributed by Mario Carneiro, 3-Sep-2015.)

Assertion

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

Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-ordt

Step	Hyp	Ref	Expression
1		cordt 17004	. 2 class ordTop
2		vr	. . 3 setvar 𝑟
3		cvv 3408	. . 3 class V
4	2	cv 1542	. . . . . . . 8 class 𝑟
5	4	cdm 5551	. . . . . . 7 class dom 𝑟
6	5	csn 4541	. . . . . 6 class {dom 𝑟}
7		vx	. . . . . . . . 9 setvar 𝑥
8		vy	. . . . . . . . . . . . 13 setvar 𝑦
9	8	cv 1542	. . . . . . . . . . . 12 class 𝑦
10	7	cv 1542	. . . . . . . . . . . 12 class 𝑥
11	9, 10, 4	wbr 5053	. . . . . . . . . . 11 wff 𝑦𝑟𝑥
12	11	wn 3	. . . . . . . . . 10 wff ¬ 𝑦𝑟𝑥
13	12, 8, 5	crab 3065	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}
14	7, 5, 13	cmpt 5135	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥})
15	10, 9, 4	wbr 5053	. . . . . . . . . . 11 wff 𝑥𝑟𝑦
16	15	wn 3	. . . . . . . . . 10 wff ¬ 𝑥𝑟𝑦
17	16, 8, 5	crab 3065	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}
18	7, 5, 17	cmpt 5135	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})
19	14, 18	cun 3864	. . . . . . 7 class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
20	19	crn 5552	. . . . . 6 class ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
21	6, 20	cun 3864	. . . . 5 class ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))
22		cfi 9026	. . . . 5 class fi
23	21, 22	cfv 6380	. . . 4 class (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))
24		ctg 16942	. . . 4 class topGen
25	23, 24	cfv 6380	. . 3 class (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))
26	2, 3, 25	cmpt 5135	. 2 class (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
27	1, 26	wceq 1543	1 wff ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))

This definition is referenced by:  ordtval  22086