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 𝑋 = dom 𝑅
Assertion ordtopn1 ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ordTop ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3 𝑋 = dom 𝑅
2 eqid ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
3 eqid ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
4 1 2 3 ordtuni ( 𝑅𝑉𝑋 = ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
5 4 adantr ( ( 𝑅𝑉𝑃𝑋 ) → 𝑋 = ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
6 dmexg ( 𝑅𝑉 → dom 𝑅 ∈ V )
7 1 6 eqeltrid ( 𝑅𝑉𝑋 ∈ V )
8 7 adantr ( ( 𝑅𝑉𝑃𝑋 ) → 𝑋 ∈ V )
9 5 8 eqeltrrd ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
10 uniexb ( ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ↔ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
11 9 10 sylibr ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
12 ssfii ( ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
13 11 12 syl ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
14 fibas ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases
15 bastg ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases → ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
16 14 15 ax-mp ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
17 13 16 sstrdi ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
18 1 2 3 ordtval ( 𝑅𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
19 18 adantr ( ( 𝑅𝑉𝑃𝑋 ) → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
20 17 19 sseqtrrd ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( ordTop ‘ 𝑅 ) )
21 ssun2 ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ⊆ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
22 ssun1 ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ⊆ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
23 simpr ( ( 𝑅𝑉𝑃𝑋 ) → 𝑃𝑋 )
24 eqidd ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } )
25 breq2 ( 𝑦 = 𝑃 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑃 ) )
26 25 notbid ( 𝑦 = 𝑃 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝑃 ) )
27 26 rabbidv ( 𝑦 = 𝑃 → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } )
28 27 rspceeqv ( ( 𝑃𝑋 ∧ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ) → ∃ 𝑦𝑋 { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
29 23 24 28 syl2anc ( ( 𝑅𝑉𝑃𝑋 ) → ∃ 𝑦𝑋 { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
30 rabexg ( 𝑋 ∈ V → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ V )
31 eqid ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
32 31 elrnmpt ( { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ V → ( { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑦𝑋 { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
33 8 30 32 3syl ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑦𝑋 { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
34 29 33 mpbird ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
35 22 34 sselid ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
36 21 35 sselid ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( { 𝑋 } ∪ ( ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦𝑋 ↦ { 𝑥𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
37 20 36 sseldd ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ordTop ‘ 𝑅 ) )