Definition df-ordt 17451

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 17449	. 2 class ordTop
2		vr	. . 3 setvar 𝑟
3		cvv 3474	. . 3 class V
4	2	cv 1540	. . . . . . . 8 class 𝑟
5	4	cdm 5676	. . . . . . 7 class dom 𝑟
6	5	csn 4628	. . . . . 6 class {dom 𝑟}
7		vx	. . . . . . . . 9 setvar 𝑥
8		vy	. . . . . . . . . . . . 13 setvar 𝑦
9	8	cv 1540	. . . . . . . . . . . 12 class 𝑦
10	7	cv 1540	. . . . . . . . . . . 12 class 𝑥
11	9, 10, 4	wbr 5148	. . . . . . . . . . 11 wff 𝑦𝑟𝑥
12	11	wn 3	. . . . . . . . . 10 wff ¬ 𝑦𝑟𝑥
13	12, 8, 5	crab 3432	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}
14	7, 5, 13	cmpt 5231	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥})
15	10, 9, 4	wbr 5148	. . . . . . . . . . 11 wff 𝑥𝑟𝑦
16	15	wn 3	. . . . . . . . . 10 wff ¬ 𝑥𝑟𝑦
17	16, 8, 5	crab 3432	. . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}
18	7, 5, 17	cmpt 5231	. . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})
19	14, 18	cun 3946	. . . . . . 7 class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
20	19	crn 5677	. . . . . 6 class ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
21	6, 20	cun 3946	. . . . 5 class ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))
22		cfi 9407	. . . . 5 class fi
23	21, 22	cfv 6543	. . . 4 class (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))
24		ctg 17387	. . . 4 class topGen
25	23, 24	cfv 6543	. . 3 class (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))
26	2, 3, 25	cmpt 5231	. 2 class (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
27	1, 26	wceq 1541	1 wff ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))

This definition is referenced by:  ordtval  22913