Metamath Proof Explorer

Theorem ordtcnvNEW

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

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion ordtcnvNEW 
|- ( K e. Proset -> ( ordTop ` `' .<_ ) = ( ordTop ` .<_ ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 vex 
 |-  y e. _V
4 vex 
 |-  x e. _V
5 3 4 brcnv 
 |-  ( y `' .<_ x <-> x .<_ y )
6 5 a1i 
 |-  ( K e. Proset -> ( y `' .<_ x <-> x .<_ y ) )
7 6 notbid 
 |-  ( K e. Proset -> ( -. y `' .<_ x <-> -. x .<_ y ) )
8 7 rabbidv 
 |-  ( K e. Proset -> { y e. B | -. y `' .<_ x } = { y e. B | -. x .<_ y } )
9 8 mpteq2dv 
 |-  ( K e. Proset -> ( x e. B |-> { y e. B | -. y `' .<_ x } ) = ( x e. B |-> { y e. B | -. x .<_ y } ) )
10 9 rneqd 
 |-  ( K e. Proset -> ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
11 4 3 brcnv 
 |-  ( x `' .<_ y <-> y .<_ x )
12 11 a1i 
 |-  ( K e. Proset -> ( x `' .<_ y <-> y .<_ x ) )
13 12 notbid 
 |-  ( K e. Proset -> ( -. x `' .<_ y <-> -. y .<_ x ) )
14 13 rabbidv 
 |-  ( K e. Proset -> { y e. B | -. x `' .<_ y } = { y e. B | -. y .<_ x } )
15 14 mpteq2dv 
 |-  ( K e. Proset -> ( x e. B |-> { y e. B | -. x `' .<_ y } ) = ( x e. B |-> { y e. B | -. y .<_ x } ) )
16 15 rneqd 
 |-  ( K e. Proset -> ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
17 10 16 uneq12d 
 |-  ( K e. Proset -> ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) = ( ran ( x e. B |-> { y e. B | -. x .<_ y } ) u. ran ( x e. B |-> { y e. B | -. y .<_ x } ) ) )
18 uncom 
 |-  ( ran ( x e. B |-> { y e. B | -. x .<_ y } ) u. ran ( x e. B |-> { y e. B | -. y .<_ x } ) ) = ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
19 17 18 eqtrdi 
 |-  ( K e. Proset -> ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) = ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) )
20 19 uneq2d 
 |-  ( K e. Proset -> ( { B } u. ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) ) = ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
21 20 fveq2d 
 |-  ( K e. Proset -> ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) ) ) = ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) )
22 21 fveq2d 
 |-  ( K e. Proset -> ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) ) ) ) = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) ) )
23 eqid 
 |-  ( ODual ` K ) = ( ODual ` K )
24 23 oduprs 
 |-  ( K e. Proset -> ( ODual ` K ) e. Proset )
25 23 1 odubas 
 |-  B = ( Base ` ( ODual ` K ) )
26 2 cnveqi 
 |-  `' .<_ = `' ( ( le ` K ) i^i ( B X. B ) )
27 cnvin 
 |-  `' ( ( le ` K ) i^i ( B X. B ) ) = ( `' ( le ` K ) i^i `' ( B X. B ) )
28 eqid 
 |-  ( le ` K ) = ( le ` K )
29 23 28 oduleval 
 |-  `' ( le ` K ) = ( le ` ( ODual ` K ) )
30 cnvxp 
 |-  `' ( B X. B ) = ( B X. B )
31 29 30 ineq12i 
 |-  ( `' ( le ` K ) i^i `' ( B X. B ) ) = ( ( le ` ( ODual ` K ) ) i^i ( B X. B ) )
32 26 27 31 3eqtri 
 |-  `' .<_ = ( ( le ` ( ODual ` K ) ) i^i ( B X. B ) )
33 eqid 
 |-  ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) = ran ( x e. B |-> { y e. B | -. y `' .<_ x } )
34 eqid 
 |-  ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) = ran ( x e. B |-> { y e. B | -. x `' .<_ y } )
35 25 32 33 34 ordtprsval 
 |-  ( ( ODual ` K ) e. Proset -> ( ordTop ` `' .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) ) ) ) )
36 24 35 syl 
 |-  ( K e. Proset -> ( ordTop ` `' .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y `' .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x `' .<_ y } ) ) ) ) ) )
37 eqid 
 |-  ran ( x e. B |-> { y e. B | -. y .<_ x } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } )
38 eqid 
 |-  ran ( x e. B |-> { y e. B | -. x .<_ y } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } )
39 1 2 37 38 ordtprsval 
 |-  ( K e. Proset -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) ) )
40 22 36 39 3eqtr4d 
 |-  ( K e. Proset -> ( ordTop ` `' .<_ ) = ( ordTop ` .<_ ) )