Theorem resttopon 23151

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
resttopon	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))

Proof of Theorem resttopon

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		topontop 22903	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2		id 22	. . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋)
3		toponmax 22916	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
4		ssexg 5258	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V)
5	2, 3, 4	syl2anr 603	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
6		resttop 23150	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
7	1, 5, 6	syl2an2r 691	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top)
8		sseqin2 4159	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
9	8	bilani 505	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴)
10		simpl 483	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
11	3	adantr 481	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽)
12		elrestr 17389	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
13	10, 5, 11, 12	syl3anc 1379	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
14	9, 13	eqeltrrd 2841	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴))
15		elssuni 4876	. . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
16	14, 15	syl 17	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
17		restval 17387	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
18	5, 17	syldan 597	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
19		inss2 4173	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
20		vex 3436	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
21	20	inex1 5252	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V
22	21	elpw 4540	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴)
23	19, 22	mpbir 232	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴
24	23	a1i 11	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴)
25	24	fmpttd 7063	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴)
26	25	frnd 6670	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴)
27	18, 26	eqsstrd 3956	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴)
28		sspwuni 5036	. . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
29	27, 28	sylib 219	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
30	16, 29	eqssd 3939	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
31		istopon 22902	. 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴)))
32	7, 30, 31	sylanbrc 589	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3432   ∩ cin 3889   ⊆ wss 3890  𝒫 cpw 4536  ∪ cuni 4845   ↦ cmpt 5160  ran crn 5626  ‘cfv 6492  (class class class)co 7363   ↾_t crest 17381  Topctop 22883  TopOnctopon 22900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-en 8891  df-fin 8894  df-fi 9321  df-rest 17383  df-topgen 17404  df-top 22884  df-topon 22901  df-bases 22936

This theorem is referenced by:  restuni  23152  stoig  23153  restsn2  23161  restlp  23173  restperf  23174  perfopn  23175  cnrest  23275  cnrest2  23276  cnrest2r  23277  cnpresti  23278  cnprest  23279  cnprest2  23280  restcnrm  23352  connsuba  23410  kgentopon  23528  1stckgenlem  23543  kgen2ss  23545  kgencn  23546  xkoinjcn  23677  qtoprest  23707  flimrest  23973  fclsrest  24014  flfcntr  24033  efmndtmd  24091  symgtgp  24096  dvrcn  24174  sszcld  24808  divcn  24860  cncfmptc  24904  cncfmptid  24905  cncfmpt2f  24907  cdivcncf  24913  cnmpopc  24920  icchmeo  24933  htpycc  24972  pcocn  25009  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  relcmpcmet  25310  mulcncf  25438  limcvallem  25863  ellimc2  25869  limcres  25878  cnplimc  25879  cnlimc  25880  limccnp  25883  limccnp2  25884  dvbss  25893  perfdvf  25895  dvreslem  25901  dvres2lem  25902  dvcnp2  25912  dvcn  25913  dvaddbr  25930  dvmulbr  25931  dvcmulf  25937  dvmptres2  25954  dvmptcmul  25956  dvmptntr  25963  dvmptfsum  25967  dvcnvlem  25968  dvcnv  25969  lhop1lem  26005  lhop2  26007  lhop  26008  dvcnvrelem2  26010  dvcnvre  26011  ftc1lem3  26030  ftc1cn  26035  taylthlem1  26363  ulmdvlem3  26392  psercn  26416  abelth  26431  logcn  26636  cxpcn  26734  cxpcn2  26735  cxpcn3  26737  resqrtcn  26738  sqrtcn  26739  loglesqrt  26750  xrlimcnp  26957  efrlim  26958  ftalem3  27063  xrge0pluscn  34131  xrge0mulc1cn  34132  lmlimxrge0  34139  pnfneige0  34142  lmxrge0  34143  esumcvg  34277  cxpcncf1  34786  cvxpconn  35477  cvxsconn  35478  cvmsf1o  35507  cvmliftlem8  35527  cvmlift2lem9a  35538  cvmlift2lem11  35548  cvmlift3lem6  35559  ivthALT  36570  poimir  38027  broucube  38028  cnambfre  38042  ftc1cnnc  38066  areacirclem2  38083  areacirclem4  38085  fsumcncf  46328  ioccncflimc  46335  cncfuni  46336  icccncfext  46337  icocncflimc  46339  cncfiooicclem1  46343  cxpcncf2  46349  dvmptconst  46365  dvmptidg  46367  dvresntr  46368  itgsubsticclem  46425  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem32  46589  fourierdlem33  46590  fourierdlem62  46618  fourierdlem93  46649  fourierdlem101  46657