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

Metamath Proof Explorer

Theorem ordttopon

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

Ref Expression
Hypothesis ordttopon.3 
|- X = dom R
Assertion ordttopon 
|- ( R e. V -> ( ordTop ` R ) e. ( TopOn ` X ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3 
 |-  X = dom R
2 eqid 
 |-  ran ( x e. X |-> { y e. X | -. y R x } ) = ran ( x e. X |-> { y e. X | -. y R x } )
3 eqid 
 |-  ran ( x e. X |-> { y e. X | -. x R y } ) = ran ( x e. X |-> { y e. X | -. x R y } )
4 1 2 3 ordtval 
 |-  ( R e. V -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) )
5 fibas 
 |-  ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) e. TopBases
6 tgtopon 
 |-  ( ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) e. TopBases -> ( topGen ` ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) e. ( TopOn ` U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) )
7 5 6 ax-mp 
 |-  ( topGen ` ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) e. ( TopOn ` U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) )
8 4 7 eqeltrdi 
 |-  ( R e. V -> ( ordTop ` R ) e. ( TopOn ` U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) )
9 1 2 3 ordtuni 
 |-  ( R e. V -> X = U. ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) )
10 dmexg 
 |-  ( R e. V -> dom R e. _V )
11 1 10 eqeltrid 
 |-  ( R e. V -> X e. _V )
12 9 11 eqeltrrd 
 |-  ( R e. V -> U. ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) e. _V )
13 uniexb 
 |-  ( ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) e. _V <-> U. ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) e. _V )
14 12 13 sylibr 
 |-  ( R e. V -> ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) e. _V )
15 fiuni 
 |-  ( ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) e. _V -> U. ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) = U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) )
16 14 15 syl 
 |-  ( R e. V -> U. ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) = U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) )
17 9 16 eqtrd 
 |-  ( R e. V -> X = U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) )
18 17 fveq2d 
 |-  ( R e. V -> ( TopOn ` X ) = ( TopOn ` U. ( fi ` ( { X } u. ( ran ( x e. X |-> { y e. X | -. y R x } ) u. ran ( x e. X |-> { y e. X | -. x R y } ) ) ) ) ) )
19 8 18 eleqtrrd 
 |-  ( R e. V -> ( ordTop ` R ) e. ( TopOn ` X ) )