Metamath Proof Explorer

Theorem ordtopn2

Description: A downward ray ( -oo , P ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 
|- X = dom R
Assertion ordtopn2 
|- ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } 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 ssun2 
 |-  ran ( y e. X |-> { x e. X | -. y R x } ) 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 | -. P R x } = { x e. X | -. P R x } )
25 breq1 
 |-  ( y = P -> ( y R x <-> P R x ) )
26 25 notbid 
 |-  ( y = P -> ( -. y R x <-> -. P R x ) )
27 26 rabbidv 
 |-  ( y = P -> { x e. X | -. y R x } = { x e. X | -. P R x } )
28 27 rspceeqv 
 |-  ( ( P e. X /\ { x e. X | -. P R x } = { x e. X | -. P R x } ) -> E. y e. X { x e. X | -. P R x } = { x e. X | -. y R x } )
29 23 24 28 syl2anc 
 |-  ( ( R e. V /\ P e. X ) -> E. y e. X { x e. X | -. P R x } = { x e. X | -. y R x } )
30 rabexg 
 |-  ( X e. _V -> { x e. X | -. P R x } e. _V )
31 eqid 
 |-  ( y e. X |-> { x e. X | -. y R x } ) = ( y e. X |-> { x e. X | -. y R x } )
32 31 elrnmpt 
 |-  ( { x e. X | -. P R x } e. _V -> ( { x e. X | -. P R x } e. ran ( y e. X |-> { x e. X | -. y R x } ) <-> E. y e. X { x e. X | -. P R x } = { x e. X | -. y R x } ) )
33 8 30 32 3syl 
 |-  ( ( R e. V /\ P e. X ) -> ( { x e. X | -. P R x } e. ran ( y e. X |-> { x e. X | -. y R x } ) <-> E. y e. X { x e. X | -. P R x } = { x e. X | -. y R x } ) )
34 29 33 mpbird 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } e. ran ( y e. X |-> { x e. X | -. y R x } ) )
35 22 34 sseldi 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } 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 sseldi 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } 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 | -. P R x } e. ( ordTop ` R ) )