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|¬yRx=ran⁡x∈X⟼y∈X|¬yRx
3 eqid ⊢ran⁡x∈X⟼y∈X|¬xRy=ran⁡x∈X⟼y∈X|¬xRy
4 1 2 3 ordtval ⊢R∈V→ordTop⁡R=topGen⁡fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
5 fibas ⊢fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈TopBases
6 tgtopon ⊢fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈TopBases→topGen⁡fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈TopOn⁡⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
7 5 6 ax-mp ⊢topGen⁡fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈TopOn⁡⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
8 4 7 eqeltrdi ⊢R∈V→ordTop⁡R∈TopOn⁡⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
9 1 2 3 ordtuni ⊢R∈V→X=⋃X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
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|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈V
13 uniexb ⊢X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈V↔⋃X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈V
14 12 13 sylibr ⊢R∈V→X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈V
15 fiuni ⊢X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy∈V→⋃X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy=⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
16 14 15 syl ⊢R∈V→⋃X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy=⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
17 9 16 eqtrd ⊢R∈V→X=⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
18 17 fveq2d ⊢R∈V→TopOn⁡X=TopOn⁡⋃fi⁡X∪ran⁡x∈X⟼y∈X|¬yRx∪ran⁡x∈X⟼y∈X|¬xRy
19 8 18 eleqtrrd ⊢R∈V→ordTop⁡R∈TopOn⁡X