Theorem restuni 23097

Description: The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)

Hypothesis

Ref	Expression
restuni.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
restuni	⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))

Proof of Theorem restuni

Step	Hyp	Ref	Expression
1		restuni.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
2	1	toptopon 22850	. . 3 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
3		resttopon 23096	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
4	2, 3	sylanb 579	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
5		toponuni 22847	. 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
6	4, 5	syl 17	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ⊆ wss 3945  ∪ cuni 4908  ‘cfv 6547  (class class class)co 7417   ↾_t crest 17402  Topctop 22826  TopOnctopon 22843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  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-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-en 8963  df-fin 8966  df-fi 9434  df-rest 17404  df-topgen 17425  df-top 22827  df-topon 22844  df-bases 22880

This theorem is referenced by:  restuni2  23102  restcld  23107  restopn2  23112  neitr  23115  restcls  23116  restntr  23117  rncmp  23331  cmpsublem  23334  cmpsub  23335  fiuncmp  23339  connsubclo  23359  connima  23360  conncn  23361  nllyrest  23421  cldllycmp  23430  lly1stc  23431  llycmpkgen2  23485  1stckgen  23489  txkgen  23587  xkopjcn  23591  xkococnlem  23594  cnextfres1  24003  cnextfres  24004  cncfcnvcn  24877  cnheibor  24912  evthicc  25419  psercn  26394  abelth  26409  zarmxt1  33568  connpconn  34932  cvmscld  34970  cvmsss2  34971  cvmliftmolem1  34978  cvmliftlem10  34991  cvmlift2lem9  35008  cvmlift2lem11  35010  cvmlift2lem12  35011  cvmlift3lem7  35022  ivthALT  35906  ptrest  37179  poimirlem29  37209  poimirlem30  37210  poimirlem31  37211  poimir  37213  cncfuni  45354  cncfiooicclem1  45361  stoweidlem28  45496  dirkercncflem4  45574  fourierdlem42  45617  restcls2lem  48059  iscnrm3rlem7  48093