MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtopn2 Structured version   Visualization version   GIF version

Theorem ordtopn2 22116
Description: A downward ray (-∞, 𝑃) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypothesis
Ref Expression
ordttopon.3 𝑋 = dom 𝑅
Assertion
Ref Expression
ordtopn2 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅))
Distinct variable groups:   𝑥,𝑃   𝑥,𝑅   𝑥,𝑉   𝑥,𝑋

Proof of Theorem ordtopn2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ordttopon.3 . . . . . . . . 9 𝑋 = dom 𝑅
2 eqid 2738 . . . . . . . . 9 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) = ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦})
3 eqid 2738 . . . . . . . . 9 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) = ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})
41, 2, 3ordtuni 22111 . . . . . . . 8 (𝑅𝑉𝑋 = ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
54adantr 484 . . . . . . 7 ((𝑅𝑉𝑃𝑋) → 𝑋 = ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
6 dmexg 7699 . . . . . . . . 9 (𝑅𝑉 → dom 𝑅 ∈ V)
71, 6eqeltrid 2843 . . . . . . . 8 (𝑅𝑉𝑋 ∈ V)
87adantr 484 . . . . . . 7 ((𝑅𝑉𝑃𝑋) → 𝑋 ∈ V)
95, 8eqeltrrd 2840 . . . . . 6 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
10 uniexb 7567 . . . . . 6 (({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V ↔ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
119, 10sylibr 237 . . . . 5 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
12 ssfii 9059 . . . . 5 (({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))))
1311, 12syl 17 . . . 4 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))))
14 fibas 21898 . . . . 5 (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))) ∈ TopBases
15 bastg 21887 . . . . 5 ((fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))) ∈ TopBases → (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))) ⊆ (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
1614, 15ax-mp 5 . . . 4 (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))) ⊆ (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))))
1713, 16sstrdi 3927 . . 3 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
181, 2, 3ordtval 22110 . . . 4 (𝑅𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
1918adantr 484 . . 3 ((𝑅𝑉𝑃𝑋) → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
2017, 19sseqtrrd 3956 . 2 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (ordTop‘𝑅))
21 ssun2 4101 . . 3 (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})) ⊆ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))
22 ssun2 4101 . . . 4 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))
23 simpr 488 . . . . . 6 ((𝑅𝑉𝑃𝑋) → 𝑃𝑋)
24 eqidd 2739 . . . . . 6 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥})
25 breq1 5070 . . . . . . . . 9 (𝑦 = 𝑃 → (𝑦𝑅𝑥𝑃𝑅𝑥))
2625notbid 321 . . . . . . . 8 (𝑦 = 𝑃 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑃𝑅𝑥))
2726rabbidv 3402 . . . . . . 7 (𝑦 = 𝑃 → {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥})
2827rspceeqv 3564 . . . . . 6 ((𝑃𝑋 ∧ {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥}) → ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})
2923, 24, 28syl2anc 587 . . . . 5 ((𝑅𝑉𝑃𝑋) → ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})
30 rabexg 5238 . . . . . 6 (𝑋 ∈ V → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ V)
31 eqid 2738 . . . . . . 7 (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})
3231elrnmpt 5839 . . . . . 6 ({𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ V → ({𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))
338, 30, 323syl 18 . . . . 5 ((𝑅𝑉𝑃𝑋) → ({𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} = {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))
3429, 33mpbird 260 . . . 4 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))
3522, 34sselid 3912 . . 3 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))
3621, 35sselid 3912 . 2 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
3720, 36sseldd 3916 1 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wrex 3063  {crab 3066  Vcvv 3420  cun 3878  wss 3880  {csn 4555   cuni 4833   class class class wbr 5067  cmpt 5149  dom cdm 5565  ran crn 5566  cfv 6397  ficfi 9050  topGenctg 16966  ordTopcordt 17028  TopBasesctb 21866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-om 7663  df-1o 8222  df-en 8647  df-fin 8650  df-fi 9051  df-topgen 16972  df-ordt 17030  df-bases 21867
This theorem is referenced by:  ordtopn3  22117  ordtcld2  22119  ordtrest  22123  ordthauslem  22304  ordthmeolem  22722  ordtrestNEW  31609
  Copyright terms: Public domain W3C validator