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

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

Proof of Theorem ordtopn1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ordttopon.3 . . . . . . . . 9 𝑋 = dom 𝑅
2 eqid 2728 . . . . . . . . 9 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) = ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦})
3 eqid 2728 . . . . . . . . 9 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}) = ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})
41, 2, 3ordtuni 23107 . . . . . . . 8 (𝑅𝑉𝑋 = ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
54adantr 480 . . . . . . 7 ((𝑅𝑉𝑃𝑋) → 𝑋 = ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
6 dmexg 7909 . . . . . . . . 9 (𝑅𝑉 → dom 𝑅 ∈ V)
71, 6eqeltrid 2833 . . . . . . . 8 (𝑅𝑉𝑋 ∈ V)
87adantr 480 . . . . . . 7 ((𝑅𝑉𝑃𝑋) → 𝑋 ∈ V)
95, 8eqeltrrd 2830 . . . . . 6 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
10 uniexb 7766 . . . . . 6 (({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V ↔ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
119, 10sylibr 233 . . . . 5 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V)
12 ssfii 9443 . . . . 5 (({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ∈ V → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))))
1311, 12syl 17 . . . 4 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))))
14 fibas 22893 . . . . 5 (fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))) ∈ TopBases
15 bastg 22882 . . . . 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 3992 . . 3 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
181, 2, 3ordtval 23106 . . . 4 (𝑅𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
1918adantr 480 . . 3 ((𝑅𝑉𝑃𝑋) → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))))
2017, 19sseqtrrd 4021 . 2 ((𝑅𝑉𝑃𝑋) → ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))) ⊆ (ordTop‘𝑅))
21 ssun2 4173 . . 3 (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})) ⊆ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))
22 ssun1 4172 . . . 4 ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⊆ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))
23 simpr 484 . . . . . 6 ((𝑅𝑉𝑃𝑋) → 𝑃𝑋)
24 eqidd 2729 . . . . . 6 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃})
25 breq2 5152 . . . . . . . . 9 (𝑦 = 𝑃 → (𝑥𝑅𝑦𝑥𝑅𝑃))
2625notbid 318 . . . . . . . 8 (𝑦 = 𝑃 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑃))
2726rabbidv 3437 . . . . . . 7 (𝑦 = 𝑃 → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃})
2827rspceeqv 3631 . . . . . 6 ((𝑃𝑋 ∧ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃}) → ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦})
2923, 24, 28syl2anc 583 . . . . 5 ((𝑅𝑉𝑃𝑋) → ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦})
30 rabexg 5333 . . . . . 6 (𝑋 ∈ V → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ V)
31 eqid 2728 . . . . . . 7 (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) = (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦})
3231elrnmpt 5958 . . . . . 6 ({𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ V → ({𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}))
338, 30, 323syl 18 . . . . 5 ((𝑅𝑉𝑃𝑋) → ({𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑦𝑋 {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} = {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}))
3429, 33mpbird 257 . . . 4 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}))
3522, 34sselid 3978 . . 3 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥})))
3621, 35sselid 3978 . 2 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ ({𝑋} ∪ (ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑦𝑋 ↦ {𝑥𝑋 ∣ ¬ 𝑦𝑅𝑥}))))
3720, 36sseldd 3981 1 ((𝑅𝑉𝑃𝑋) → {𝑥𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ordTop‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  wrex 3067  {crab 3429  Vcvv 3471  cun 3945  wss 3947  {csn 4629   cuni 4908   class class class wbr 5148  cmpt 5231  dom cdm 5678  ran crn 5679  cfv 6548  ficfi 9434  topGenctg 17419  ordTopcordt 17481  TopBasesctb 22861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-om 7871  df-1o 8487  df-en 8965  df-fin 8968  df-fi 9435  df-topgen 17425  df-ordt 17483  df-bases 22862
This theorem is referenced by:  ordtopn3  23113  ordtcld1  23114  ordtrest  23119  ordtrest2lem  23120  ordthauslem  23300  ordthmeolem  23718  ordtrestNEW  33522  ordtrest2NEWlem  33523
  Copyright terms: Public domain W3C validator