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