Metamath Proof Explorer


Theorem ordtopn1

Description: An upward ray ( P , +oo ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3
|- X = dom R
Assertion ordtopn1
|- ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ( ordTop ` R ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3
 |-  X = dom R
2 eqid
 |-  ran ( y e. X |-> { x e. X | -. x R y } ) = ran ( y e. X |-> { x e. X | -. x R y } )
3 eqid
 |-  ran ( y e. X |-> { x e. X | -. y R x } ) = ran ( y e. X |-> { x e. X | -. y R x } )
4 1 2 3 ordtuni
 |-  ( R e. V -> X = U. ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) )
5 4 adantr
 |-  ( ( R e. V /\ P e. X ) -> X = U. ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) )
6 dmexg
 |-  ( R e. V -> dom R e. _V )
7 1 6 eqeltrid
 |-  ( R e. V -> X e. _V )
8 7 adantr
 |-  ( ( R e. V /\ P e. X ) -> X e. _V )
9 5 8 eqeltrrd
 |-  ( ( R e. V /\ P e. X ) -> U. ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) e. _V )
10 uniexb
 |-  ( ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) e. _V <-> U. ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) e. _V )
11 9 10 sylibr
 |-  ( ( R e. V /\ P e. X ) -> ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) e. _V )
12 ssfii
 |-  ( ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) e. _V -> ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) C_ ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) )
13 11 12 syl
 |-  ( ( R e. V /\ P e. X ) -> ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) C_ ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) )
14 fibas
 |-  ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) e. TopBases
15 bastg
 |-  ( ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) e. TopBases -> ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) C_ ( topGen ` ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) ) )
16 14 15 ax-mp
 |-  ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) C_ ( topGen ` ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) )
17 13 16 sstrdi
 |-  ( ( R e. V /\ P e. X ) -> ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) C_ ( topGen ` ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) ) )
18 1 2 3 ordtval
 |-  ( R e. V -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) ) )
19 18 adantr
 |-  ( ( R e. V /\ P e. X ) -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) ) ) )
20 17 19 sseqtrrd
 |-  ( ( R e. V /\ P e. X ) -> ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) C_ ( ordTop ` R ) )
21 ssun2
 |-  ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) C_ ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) )
22 ssun1
 |-  ran ( y e. X |-> { x e. X | -. x R y } ) C_ ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) )
23 simpr
 |-  ( ( R e. V /\ P e. X ) -> P e. X )
24 eqidd
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } = { x e. X | -. x R P } )
25 breq2
 |-  ( y = P -> ( x R y <-> x R P ) )
26 25 notbid
 |-  ( y = P -> ( -. x R y <-> -. x R P ) )
27 26 rabbidv
 |-  ( y = P -> { x e. X | -. x R y } = { x e. X | -. x R P } )
28 27 rspceeqv
 |-  ( ( P e. X /\ { x e. X | -. x R P } = { x e. X | -. x R P } ) -> E. y e. X { x e. X | -. x R P } = { x e. X | -. x R y } )
29 23 24 28 syl2anc
 |-  ( ( R e. V /\ P e. X ) -> E. y e. X { x e. X | -. x R P } = { x e. X | -. x R y } )
30 rabexg
 |-  ( X e. _V -> { x e. X | -. x R P } e. _V )
31 eqid
 |-  ( y e. X |-> { x e. X | -. x R y } ) = ( y e. X |-> { x e. X | -. x R y } )
32 31 elrnmpt
 |-  ( { x e. X | -. x R P } e. _V -> ( { x e. X | -. x R P } e. ran ( y e. X |-> { x e. X | -. x R y } ) <-> E. y e. X { x e. X | -. x R P } = { x e. X | -. x R y } ) )
33 8 30 32 3syl
 |-  ( ( R e. V /\ P e. X ) -> ( { x e. X | -. x R P } e. ran ( y e. X |-> { x e. X | -. x R y } ) <-> E. y e. X { x e. X | -. x R P } = { x e. X | -. x R y } ) )
34 29 33 mpbird
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ran ( y e. X |-> { x e. X | -. x R y } ) )
35 22 34 sselid
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) )
36 21 35 sselid
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ( { X } u. ( ran ( y e. X |-> { x e. X | -. x R y } ) u. ran ( y e. X |-> { x e. X | -. y R x } ) ) ) )
37 20 36 sseldd
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ( ordTop ` R ) )