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 
|- ( R e. PosetRel -> ( ordTop ` `' R ) = ( ordTop ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom R = dom R
2 1 psrn 
 |-  ( R e. PosetRel -> dom R = ran R )
3 2 eqcomd 
 |-  ( R e. PosetRel -> ran R = dom R )
4 3 sneqd 
 |-  ( R e. PosetRel -> { ran R } = { dom R } )
5 vex 
 |-  y e. _V
6 vex 
 |-  x e. _V
7 5 6 brcnv 
 |-  ( y `' R x <-> x R y )
8 7 a1i 
 |-  ( R e. PosetRel -> ( y `' R x <-> x R y ) )
9 8 notbid 
 |-  ( R e. PosetRel -> ( -. y `' R x <-> -. x R y ) )
10 3 9 rabeqbidv 
 |-  ( R e. PosetRel -> { y e. ran R | -. y `' R x } = { y e. dom R | -. x R y } )
11 3 10 mpteq12dv 
 |-  ( R e. PosetRel -> ( x e. ran R |-> { y e. ran R | -. y `' R x } ) = ( x e. dom R |-> { y e. dom R | -. x R y } ) )
12 11 rneqd 
 |-  ( R e. PosetRel -> ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) = ran ( x e. dom R |-> { y e. dom R | -. x R y } ) )
13 6 5 brcnv 
 |-  ( x `' R y <-> y R x )
14 13 a1i 
 |-  ( R e. PosetRel -> ( x `' R y <-> y R x ) )
15 14 notbid 
 |-  ( R e. PosetRel -> ( -. x `' R y <-> -. y R x ) )
16 3 15 rabeqbidv 
 |-  ( R e. PosetRel -> { y e. ran R | -. x `' R y } = { y e. dom R | -. y R x } )
17 3 16 mpteq12dv 
 |-  ( R e. PosetRel -> ( x e. ran R |-> { y e. ran R | -. x `' R y } ) = ( x e. dom R |-> { y e. dom R | -. y R x } ) )
18 17 rneqd 
 |-  ( R e. PosetRel -> ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) = ran ( x e. dom R |-> { y e. dom R | -. y R x } ) )
19 12 18 uneq12d 
 |-  ( R e. PosetRel -> ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) = ( ran ( x e. dom R |-> { y e. dom R | -. x R y } ) u. ran ( x e. dom R |-> { y e. dom R | -. y R x } ) ) )
20 uncom 
 |-  ( ran ( x e. dom R |-> { y e. dom R | -. x R y } ) u. ran ( x e. dom R |-> { y e. dom R | -. y R x } ) ) = ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) )
21 19 20 eqtrdi 
 |-  ( R e. PosetRel -> ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) = ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) ) )
22 4 21 uneq12d 
 |-  ( R e. PosetRel -> ( { ran R } u. ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) ) = ( { dom R } u. ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) ) ) )
23 22 fveq2d 
 |-  ( R e. PosetRel -> ( fi ` ( { ran R } u. ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) ) ) = ( fi ` ( { dom R } u. ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) ) ) ) )
24 23 fveq2d 
 |-  ( R e. PosetRel -> ( topGen ` ( fi ` ( { ran R } u. ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) ) ) ) = ( topGen ` ( fi ` ( { dom R } u. ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) ) ) ) ) )
25 cnvps 
 |-  ( R e. PosetRel -> `' R e. PosetRel )
26 df-rn 
 |-  ran R = dom `' R
27 eqid 
 |-  ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } )
28 eqid 
 |-  ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) = ran ( x e. ran R |-> { y e. ran R | -. x `' R y } )
29 26 27 28 ordtval 
 |-  ( `' R e. PosetRel -> ( ordTop ` `' R ) = ( topGen ` ( fi ` ( { ran R } u. ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) ) ) ) )
30 25 29 syl 
 |-  ( R e. PosetRel -> ( ordTop ` `' R ) = ( topGen ` ( fi ` ( { ran R } u. ( ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) u. ran ( x e. ran R |-> { y e. ran R | -. x `' R y } ) ) ) ) ) )
31 eqid 
 |-  ran ( x e. dom R |-> { y e. dom R | -. y R x } ) = ran ( x e. dom R |-> { y e. dom R | -. y R x } )
32 eqid 
 |-  ran ( x e. dom R |-> { y e. dom R | -. x R y } ) = ran ( x e. dom R |-> { y e. dom R | -. x R y } )
33 1 31 32 ordtval 
 |-  ( R e. PosetRel -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { dom R } u. ( ran ( x e. dom R |-> { y e. dom R | -. y R x } ) u. ran ( x e. dom R |-> { y e. dom R | -. x R y } ) ) ) ) ) )
34 24 30 33 3eqtr4d 
 |-  ( R e. PosetRel -> ( ordTop ` `' R ) = ( ordTop ` R ) )