This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑟 ∈ 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 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) )