Metamath Proof Explorer

Theorem ordtval

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 
|- X = dom R
ordtval.2 
|- A = ran ( x e. X |-> { y e. X | -. y R x } )
ordtval.3 
|- B = ran ( x e. X |-> { y e. X | -. x R y } )
Assertion ordtval 
|- ( R e. V -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 
 |-  X = dom R
2 ordtval.2 
 |-  A = ran ( x e. X |-> { y e. X | -. y R x } )
3 ordtval.3 
 |-  B = ran ( x e. X |-> { y e. X | -. x R y } )
4 elex 
 |-  ( R e. V -> R e. _V )
5 dmeq 
 |-  ( r = R -> dom r = dom R )
6 5 1 eqtr4di 
 |-  ( r = R -> dom r = X )
7 6 sneqd 
 |-  ( r = R -> { dom r } = { X } )
8 rnun 
 |-  ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom 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 } ) )
9 breq 
 |-  ( r = R -> ( y r x <-> y R x ) )
10 9 notbid 
 |-  ( r = R -> ( -. y r x <-> -. y R x ) )
11 6 10 rabeqbidv 
 |-  ( r = R -> { y e. dom r | -. y r x } = { y e. X | -. y R x } )
12 6 11 mpteq12dv 
 |-  ( r = R -> ( x e. dom r |-> { y e. dom r | -. y r x } ) = ( x e. X |-> { y e. X | -. y R x } ) )
13 12 rneqd 
 |-  ( r = R -> ran ( x e. dom r |-> { y e. dom r | -. y r x } ) = ran ( x e. X |-> { y e. X | -. y R x } ) )
14 13 2 eqtr4di 
 |-  ( r = R -> ran ( x e. dom r |-> { y e. dom r | -. y r x } ) = A )
15 breq 
 |-  ( r = R -> ( x r y <-> x R y ) )
16 15 notbid 
 |-  ( r = R -> ( -. x r y <-> -. x R y ) )
17 6 16 rabeqbidv 
 |-  ( r = R -> { y e. dom r | -. x r y } = { y e. X | -. x R y } )
18 6 17 mpteq12dv 
 |-  ( r = R -> ( x e. dom r |-> { y e. dom r | -. x r y } ) = ( x e. X |-> { y e. X | -. x R y } ) )
19 18 rneqd 
 |-  ( r = R -> ran ( x e. dom r |-> { y e. dom r | -. x r y } ) = ran ( x e. X |-> { y e. X | -. x R y } ) )
20 19 3 eqtr4di 
 |-  ( r = R -> ran ( x e. dom r |-> { y e. dom r | -. x r y } ) = B )
21 14 20 uneq12d 
 |-  ( r = R -> ( 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 } ) ) = ( A u. B ) )
22 8 21 syl5eq 
 |-  ( r = R -> ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) = ( A u. B ) )
23 7 22 uneq12d 
 |-  ( r = R -> ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) = ( { X } u. ( A u. B ) ) )
24 23 fveq2d 
 |-  ( r = R -> ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) = ( fi ` ( { X } u. ( A u. B ) ) ) )
25 24 fveq2d 
 |-  ( r = R -> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) = ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) )
26 df-ordt 
 |-  ordTop = ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )
27 fvex 
 |-  ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) e. _V
28 25 26 27 fvmpt 
 |-  ( R e. _V -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) )
29 4 28 syl 
 |-  ( R e. V -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) )