Theorem resttopon 23156

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 22906	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2		id 22	. . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋)
3		toponmax 22919	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
4		ssexg 5328	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V)
5	2, 3, 4	syl2anr 595	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
6		resttop 23155	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
7	1, 5, 6	syl2an2r 683	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top)
8		simpr 483	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
9		sseqin2 4216	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
10	8, 9	sylib 217	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴)
11		simpl 481	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
12	3	adantr 479	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽)
13		elrestr 17443	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
14	11, 5, 12, 13	syl3anc 1368	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
15	10, 14	eqeltrrd 2827	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴))
16		elssuni 4945	. . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
17	15, 16	syl 17	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
18		restval 17441	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
19	5, 18	syldan 589	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
20		inss2 4231	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
21		vex 3466	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
22	21	inex1 5322	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V
23	22	elpw 4611	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴)
24	20, 23	mpbir 230	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴
25	24	a1i 11	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴)
26	25	fmpttd 7129	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴)
27	26	frnd 6736	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴)
28	19, 27	eqsstrd 4018	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴)
29		sspwuni 5108	. . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
30	28, 29	sylib 217	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
31	17, 30	eqssd 3997	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
32		istopon 22905	. 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴)))
33	7, 31, 32	sylanbrc 581	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  Vcvv 3462   ∩ cin 3946   ⊆ wss 3947  𝒫 cpw 4607  ∪ cuni 4913   ↦ cmpt 5236  ran crn 5683  ‘cfv 6554  (class class class)co 7424   ↾_t crest 17435  Topctop 22886  TopOnctopon 22903

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 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-en 8975  df-fin 8978  df-fi 9454  df-rest 17437  df-topgen 17458  df-top 22887  df-topon 22904  df-bases 22940

This theorem is referenced by:  restuni  23157  stoig  23158  restsn2  23166  restlp  23178  restperf  23179  perfopn  23180  cnrest  23280  cnrest2  23281  cnrest2r  23282  cnpresti  23283  cnprest  23284  cnprest2  23285  restcnrm  23357  connsuba  23415  kgentopon  23533  1stckgenlem  23548  kgen2ss  23550  kgencn  23551  xkoinjcn  23682  qtoprest  23712  flimrest  23978  fclsrest  24019  flfcntr  24038  efmndtmd  24096  symgtgp  24101  dvrcn  24179  sszcld  24824  divcnOLD  24875  divcn  24877  cncfmptc  24923  cncfmptid  24924  cncfmpt2f  24926  cdivcncf  24932  cnmpopc  24940  icchmeo  24956  icchmeoOLD  24957  htpycc  24997  pcocn  25035  pcohtpylem  25037  pcopt  25040  pcopt2  25041  pcoass  25042  pcorevlem  25044  relcmpcmet  25337  mulcncf  25465  limcvallem  25891  ellimc2  25897  limcres  25906  cnplimc  25907  cnlimc  25908  limccnp  25911  limccnp2  25912  dvbss  25921  perfdvf  25923  dvreslem  25929  dvres2lem  25930  dvcnp2  25940  dvcnp2OLD  25941  dvcn  25942  dvaddbr  25959  dvmulbr  25960  dvmulbrOLD  25961  dvcmulf  25967  dvmptres2  25985  dvmptcmul  25987  dvmptntr  25994  dvmptfsum  25998  dvcnvlem  25999  dvcnv  26000  lhop1lem  26037  lhop2  26039  lhop  26040  dvcnvrelem2  26042  dvcnvre  26043  ftc1lem3  26064  ftc1cn  26069  taylthlem1  26401  ulmdvlem3  26431  psercn  26456  abelth  26471  logcn  26674  cxpcn  26772  cxpcnOLD  26773  cxpcn2  26774  cxpcn3  26776  resqrtcn  26777  sqrtcn  26778  loglesqrt  26789  xrlimcnp  26996  efrlim  26997  efrlimOLD  26998  ftalem3  27103  xrge0pluscn  33755  xrge0mulc1cn  33756  lmlimxrge0  33763  pnfneige0  33766  lmxrge0  33767  esumcvg  33919  cxpcncf1  34441  cvxpconn  35070  cvxsconn  35071  cvmsf1o  35100  cvmliftlem8  35120  cvmlift2lem9a  35131  cvmlift2lem11  35141  cvmlift3lem6  35152  ivthALT  36047  poimir  37354  broucube  37355  cnambfre  37369  ftc1cnnc  37393  areacirclem2  37410  areacirclem4  37412  fsumcncf  45499  ioccncflimc  45506  cncfuni  45507  icccncfext  45508  icocncflimc  45510  cncfiooicclem1  45514  cxpcncf2  45520  dvmptconst  45536  dvmptidg  45538  dvresntr  45539  itgsubsticclem  45596  dirkercncflem2  45725  dirkercncflem4  45727  fourierdlem32  45760  fourierdlem33  45761  fourierdlem62  45789  fourierdlem93  45820  fourierdlem101  45828