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 V P X x X | ¬ P R x ordTop R

Proof

Step Hyp Ref Expression
1 ordttopon.3 X = dom R
2 eqid ran y X x X | ¬ x R y = ran y X x X | ¬ x R y
3 eqid ran y X x X | ¬ y R x = ran y X x X | ¬ y R x
4 1 2 3 ordtuni R V X = X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
5 4 adantr R V P X X = X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
6 dmexg R V dom R V
7 1 6 eqeltrid R V X V
8 7 adantr R V P X X V
9 5 8 eqeltrrd R V P X X ran y X x X | ¬ x R y ran y X x X | ¬ y R x V
10 uniexb X ran y X x X | ¬ x R y ran y X x X | ¬ y R x V X ran y X x X | ¬ x R y ran y X x X | ¬ y R x V
11 9 10 sylibr R V P X X ran y X x X | ¬ x R y ran y X x X | ¬ y R x V
12 ssfii X ran y X x X | ¬ x R y ran y X x X | ¬ y R x V X ran y X x X | ¬ x R y ran y X x X | ¬ y R x fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
13 11 12 syl R V P X X ran y X x X | ¬ x R y ran y X x X | ¬ y R x fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
14 fibas fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x TopBases
15 bastg fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x TopBases fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x topGen fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
16 14 15 ax-mp fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x topGen fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
17 13 16 sstrdi R V P X X ran y X x X | ¬ x R y ran y X x X | ¬ y R x topGen fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
18 1 2 3 ordtval R V ordTop R = topGen fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
19 18 adantr R V P X ordTop R = topGen fi X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
20 17 19 sseqtrrd R V P X X ran y X x X | ¬ x R y ran y X x X | ¬ y R x ordTop R
21 ssun2 ran y X x X | ¬ x R y ran y X x X | ¬ y R x X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
22 ssun2 ran y X x X | ¬ y R x ran y X x X | ¬ x R y ran y X x X | ¬ y R x
23 simpr R V P X P X
24 eqidd R V P X x X | ¬ P R x = x 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 X | ¬ y R x = x X | ¬ P R x
28 27 rspceeqv P X x X | ¬ P R x = x X | ¬ P R x y X x X | ¬ P R x = x X | ¬ y R x
29 23 24 28 syl2anc R V P X y X x X | ¬ P R x = x X | ¬ y R x
30 rabexg X V x X | ¬ P R x V
31 eqid y X x X | ¬ y R x = y X x X | ¬ y R x
32 31 elrnmpt x X | ¬ P R x V x X | ¬ P R x ran y X x X | ¬ y R x y X x X | ¬ P R x = x X | ¬ y R x
33 8 30 32 3syl R V P X x X | ¬ P R x ran y X x X | ¬ y R x y X x X | ¬ P R x = x X | ¬ y R x
34 29 33 mpbird R V P X x X | ¬ P R x ran y X x X | ¬ y R x
35 22 34 sseldi R V P X x X | ¬ P R x ran y X x X | ¬ x R y ran y X x X | ¬ y R x
36 21 35 sseldi R V P X x X | ¬ P R x X ran y X x X | ¬ x R y ran y X x X | ¬ y R x
37 20 36 sseldd R V P X x X | ¬ P R x ordTop R