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 ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P ∈ 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 ssun1 ⊢ ran ⁡ y ∈ X ⟼ x ∈ X | ¬ x R y ⊆ 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 | ¬ x R P = x ∈ 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 ∈ X | ¬ x R y = x ∈ X | ¬ x R P
28 27 rspceeqv ⊢ P ∈ X ∧ x ∈ X | ¬ x R P = x ∈ X | ¬ x R P → ∃ y ∈ X x ∈ X | ¬ x R P = x ∈ X | ¬ x R y
29 23 24 28 syl2anc ⊢ R ∈ V ∧ P ∈ X → ∃ y ∈ X x ∈ X | ¬ x R P = x ∈ X | ¬ x R y
30 rabexg ⊢ X ∈ V → x ∈ X | ¬ x R P ∈ V
31 eqid ⊢ y ∈ X ⟼ x ∈ X | ¬ x R y = y ∈ X ⟼ x ∈ X | ¬ x R y
32 31 elrnmpt ⊢ x ∈ X | ¬ x R P ∈ V → x ∈ X | ¬ x R P ∈ ran ⁡ y ∈ X ⟼ x ∈ X | ¬ x R y ↔ ∃ y ∈ X x ∈ X | ¬ x R P = x ∈ X | ¬ x R y
33 8 30 32 3syl ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P ∈ ran ⁡ y ∈ X ⟼ x ∈ X | ¬ x R y ↔ ∃ y ∈ X x ∈ X | ¬ x R P = x ∈ X | ¬ x R y
34 29 33 mpbird ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P ∈ ran ⁡ y ∈ X ⟼ x ∈ X | ¬ x R y
35 22 34 sseldi ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P ∈ 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 | ¬ x R P ∈ 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 | ¬ x R P ∈ ordTop ⁡ R