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

Metamath Proof Explorer

Theorem ordtcnv

Description: The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion ordtcnv ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( ordTop ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom 𝑅 = dom 𝑅
2 1 psrn ⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ran 𝑅 )
3 2 eqcomd ⊢ ( 𝑅 ∈ PosetRel → ran 𝑅 = dom 𝑅 )
4 3 sneqd ⊢ ( 𝑅 ∈ PosetRel → { ran 𝑅 } = { dom 𝑅 } )
5 vex ⊢ 𝑦 ∈ V
6 vex ⊢ 𝑥 ∈ V
7 5 6 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
8 7 a1i ⊢ ( 𝑅 ∈ PosetRel → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
9 8 notbid ⊢ ( 𝑅 ∈ PosetRel → ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 ) )
10 3 9 rabeqbidv ⊢ ( 𝑅 ∈ PosetRel → { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } = { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } )
11 3 10 mpteq12dv ⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
12 11 rneqd ⊢ ( 𝑅 ∈ PosetRel → ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
13 6 5 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
14 13 a1i ⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
15 14 notbid ⊢ ( 𝑅 ∈ PosetRel → ( ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑥 ) )
16 3 15 rabeqbidv ⊢ ( 𝑅 ∈ PosetRel → { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } = { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } )
17 3 16 mpteq12dv ⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
18 17 rneqd ⊢ ( 𝑅 ∈ PosetRel → ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
19 12 18 uneq12d ⊢ ( 𝑅 ∈ PosetRel → ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
20 uncom ⊢ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
21 19 20 eqtrdi ⊢ ( 𝑅 ∈ PosetRel → ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) )
22 4 21 uneq12d ⊢ ( 𝑅 ∈ PosetRel → ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) = ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) )
23 22 fveq2d ⊢ ( 𝑅 ∈ PosetRel → ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) = ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
24 23 fveq2d ⊢ ( 𝑅 ∈ PosetRel → ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) = ( topGen ‘ ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
25 cnvps ⊢ ( 𝑅 ∈ PosetRel → ◡ 𝑅 ∈ PosetRel )
26 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
27 eqid ⊢ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } )
28 eqid ⊢ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } )
29 26 27 28 ordtval ⊢ ( ◡ 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) )
30 25 29 syl ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) )
31 eqid ⊢ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } )
32 eqid ⊢ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } )
33 1 31 32 ordtval ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
34 24 30 33 3eqtr4d ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( ordTop ‘ 𝑅 ) )