Metamath Proof Explorer

Theorem ordtprsval

Description: Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtposval.e 
|- E = ran ( x e. B |-> { y e. B | -. y .<_ x } )
ordtposval.f 
|- F = ran ( x e. B |-> { y e. B | -. x .<_ y } )
Assertion ordtprsval 
|- ( K e. Proset -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( E u. F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 ordtposval.e 
 |-  E = ran ( x e. B |-> { y e. B | -. y .<_ x } )
4 ordtposval.f 
 |-  F = ran ( x e. B |-> { y e. B | -. x .<_ y } )
5 fvex 
 |-  ( le ` K ) e. _V
6 5 inex1 
 |-  ( ( le ` K ) i^i ( B X. B ) ) e. _V
7 2 6 eqeltri 
 |-  .<_ e. _V
8 eqid 
 |-  dom .<_ = dom .<_
9 eqid 
 |-  ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } )
10 eqid 
 |-  ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } )
11 8 9 10 ordtval 
 |-  ( .<_ e. _V -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) ) ) )
12 7 11 ax-mp 
 |-  ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) ) )
13 1 2 prsdm 
 |-  ( K e. Proset -> dom .<_ = B )
14 13 sneqd 
 |-  ( K e. Proset -> { dom .<_ } = { B } )
15 13 rabeqdv 
 |-  ( K e. Proset -> { y e. dom .<_ | -. y .<_ x } = { y e. B | -. y .<_ x } )
16 13 15 mpteq12dv 
 |-  ( K e. Proset -> ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ( x e. B |-> { y e. B | -. y .<_ x } ) )
17 16 rneqd 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
18 17 3 eqtr4di 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = E )
19 13 rabeqdv 
 |-  ( K e. Proset -> { y e. dom .<_ | -. x .<_ y } = { y e. B | -. x .<_ y } )
20 13 19 mpteq12dv 
 |-  ( K e. Proset -> ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ( x e. B |-> { y e. B | -. x .<_ y } ) )
21 20 rneqd 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
22 21 4 eqtr4di 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = F )
23 18 22 uneq12d 
 |-  ( K e. Proset -> ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) = ( E u. F ) )
24 14 23 uneq12d 
 |-  ( K e. Proset -> ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) = ( { B } u. ( E u. F ) ) )
25 24 fveq2d 
 |-  ( K e. Proset -> ( fi ` ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) ) = ( fi ` ( { B } u. ( E u. F ) ) ) )
26 25 fveq2d 
 |-  ( K e. Proset -> ( topGen ` ( fi ` ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) ) ) = ( topGen ` ( fi ` ( { B } u. ( E u. F ) ) ) ) )
27 12 26 syl5eq 
 |-  ( K e. Proset -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( E u. F ) ) ) ) )