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 ‘ 𝑋 ) )