Definition df-ordt 17221

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 17219	. 2 class ordTop
2		vr	. . 3 setvar 𝑟
3		cvv 3433	. . 3 class V
4	2	cv 1538	. . . . . . . 8 class 𝑟
5	4	cdm 5590	. . . . . . 7 class dom 𝑟
6	5	csn 4562	. . . . . 6 class {dom 𝑟}
7		vx	. . . . . . . . 9 setvar 𝑥
8		vy	. . . . . . . . . . . . 13 setvar 𝑦
9	8	cv 1538	. . . . . . . . . . . 12 class 𝑦
10	7	cv 1538	. . . . . . . . . . . 12 class 𝑥
11	9, 10, 4	wbr 5075	. . . . . . . . . . 11 wff 𝑦𝑟𝑥
12	11	wn 3	. . . . . . . . . 10 wff ¬ 𝑦𝑟𝑥
13	12, 8, 5	crab 3069	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}
14	7, 5, 13	cmpt 5158	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥})
15	10, 9, 4	wbr 5075	. . . . . . . . . . 11 wff 𝑥𝑟𝑦
16	15	wn 3	. . . . . . . . . 10 wff ¬ 𝑥𝑟𝑦
17	16, 8, 5	crab 3069	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}
18	7, 5, 17	cmpt 5158	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})
19	14, 18	cun 3886	. . . . . . 7 class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
20	19	crn 5591	. . . . . 6 class ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
21	6, 20	cun 3886	. . . . 5 class ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))
22		cfi 9178	. . . . 5 class fi
23	21, 22	cfv 6437	. . . 4 class (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))
24		ctg 17157	. . . 4 class topGen
25	23, 24	cfv 6437	. . 3 class (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))
26	2, 3, 25	cmpt 5158	. 2 class (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
27	1, 26	wceq 1539	1 wff ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))

This definition is referenced by:  ordtval  22349