Metamath Proof Explorer

Theorem ordttopon

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 ⊢ X = dom ⁡ R
Assertion ordttopon ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ X

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ X = dom ⁡ R
2 eqid ⊢ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x
3 eqid ⊢ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
4 1 2 3 ordtval ⊢ R ∈ V → ordTop ⁡ R = topGen ⁡ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
5 fibas ⊢ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ TopBases
6 tgtopon ⊢ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ TopBases → topGen ⁡ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ TopOn ⁡ ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
7 5 6 ax-mp ⊢ topGen ⁡ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ TopOn ⁡ ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
8 4 7 eqeltrdi ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
9 1 2 3 ordtuni ⊢ R ∈ V → X = ⋃ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
10 dmexg ⊢ R ∈ V → dom ⁡ R ∈ V
11 1 10 eqeltrid ⊢ R ∈ V → X ∈ V
12 9 11 eqeltrrd ⊢ R ∈ V → ⋃ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ V
13 uniexb ⊢ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ V ↔ ⋃ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ V
14 12 13 sylibr ⊢ R ∈ V → X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ V
15 fiuni ⊢ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ∈ V → ⋃ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y = ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
16 14 15 syl ⊢ R ∈ V → ⋃ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y = ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
17 9 16 eqtrd ⊢ R ∈ V → X = ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
18 17 fveq2d ⊢ R ∈ V → TopOn ⁡ X = TopOn ⁡ ⋃ fi ⁡ X ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ∪ ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
19 8 18 eleqtrrd ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ X