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

Metamath Proof Explorer

Theorem ordttopon

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

Ref Expression
Hypothesis ordttopon.3 ⊢ 𝑋 = dom 𝑅
Assertion ordttopon ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ 𝑋 = dom 𝑅
2 eqid ⊢ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 eqid ⊢ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
4 1 2 3 ordtval ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
5 fibas ⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ∈ TopBases
6 tgtopon ⊢ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ∈ TopBases → ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
7 5 6 ax-mp ⊢ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
8 4 7 eqeltrdi ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
9 1 2 3 ordtuni ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) )
10 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
11 1 10 eqeltrid ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 ∈ V )
12 9 11 eqeltrrd ⊢ ( 𝑅 ∈ 𝑉 → ∪ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ∈ V )
13 uniexb ⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ∈ V )
14 12 13 sylibr ⊢ ( 𝑅 ∈ 𝑉 → ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ∈ V )
15 fiuni ⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ∈ V → ∪ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) = ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
16 14 15 syl ⊢ ( 𝑅 ∈ 𝑉 → ∪ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) = ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
17 9 16 eqtrd ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
18 17 fveq2d ⊢ ( 𝑅 ∈ 𝑉 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
19 8 18 eleqtrrd ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )