Theorem resttopon 23184

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 22934	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2		id 22	. . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋)
3		toponmax 22947	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
4		ssexg 5328	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V)
5	2, 3, 4	syl2anr 597	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
6		resttop 23183	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
7	1, 5, 6	syl2an2r 685	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top)
8		simpr 484	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
9		sseqin2 4230	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
10	8, 9	sylib 218	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴)
11		simpl 482	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
12	3	adantr 480	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽)
13		elrestr 17474	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
14	11, 5, 12, 13	syl3anc 1370	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
15	10, 14	eqeltrrd 2839	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴))
16		elssuni 4941	. . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
17	15, 16	syl 17	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
18		restval 17472	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
19	5, 18	syldan 591	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
20		inss2 4245	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
21		vex 3481	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
22	21	inex1 5322	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V
23	22	elpw 4608	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴)
24	20, 23	mpbir 231	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴
25	24	a1i 11	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴)
26	25	fmpttd 7134	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴)
27	26	frnd 6744	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴)
28	19, 27	eqsstrd 4033	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴)
29		sspwuni 5104	. . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
30	28, 29	sylib 218	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
31	17, 30	eqssd 4012	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
32		istopon 22933	. 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴)))
33	7, 31, 32	sylanbrc 583	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962  𝒫 cpw 4604  ∪ cuni 4911   ↦ cmpt 5230  ran crn 5689  ‘cfv 6562  (class class class)co 7430   ↾_t crest 17466  Topctop 22914  TopOnctopon 22931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-en 8984  df-fin 8987  df-fi 9448  df-rest 17468  df-topgen 17489  df-top 22915  df-topon 22932  df-bases 22968

This theorem is referenced by:  restuni  23185  stoig  23186  restsn2  23194  restlp  23206  restperf  23207  perfopn  23208  cnrest  23308  cnrest2  23309  cnrest2r  23310  cnpresti  23311  cnprest  23312  cnprest2  23313  restcnrm  23385  connsuba  23443  kgentopon  23561  1stckgenlem  23576  kgen2ss  23578  kgencn  23579  xkoinjcn  23710  qtoprest  23740  flimrest  24006  fclsrest  24047  flfcntr  24066  efmndtmd  24124  symgtgp  24129  dvrcn  24207  sszcld  24852  divcnOLD  24903  divcn  24905  cncfmptc  24951  cncfmptid  24952  cncfmpt2f  24954  cdivcncf  24960  cnmpopc  24968  icchmeo  24984  icchmeoOLD  24985  htpycc  25025  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  relcmpcmet  25365  mulcncf  25493  limcvallem  25920  ellimc2  25926  limcres  25935  cnplimc  25936  cnlimc  25937  limccnp  25940  limccnp2  25941  dvbss  25950  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmulf  25996  dvmptres2  26014  dvmptcmul  26016  dvmptntr  26023  dvmptfsum  26027  dvcnvlem  26028  dvcnv  26029  lhop1lem  26066  lhop2  26068  lhop  26069  dvcnvrelem2  26071  dvcnvre  26072  ftc1lem3  26093  ftc1cn  26098  taylthlem1  26429  ulmdvlem3  26459  psercn  26484  abelth  26499  logcn  26703  cxpcn  26801  cxpcnOLD  26802  cxpcn2  26803  cxpcn3  26805  resqrtcn  26806  sqrtcn  26807  loglesqrt  26818  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  ftalem3  27132  xrge0pluscn  33900  xrge0mulc1cn  33901  lmlimxrge0  33908  pnfneige0  33911  lmxrge0  33912  esumcvg  34066  cxpcncf1  34588  cvxpconn  35226  cvxsconn  35227  cvmsf1o  35256  cvmliftlem8  35276  cvmlift2lem9a  35287  cvmlift2lem11  35297  cvmlift3lem6  35308  ivthALT  36317  poimir  37639  broucube  37640  cnambfre  37654  ftc1cnnc  37678  areacirclem2  37695  areacirclem4  37697  fsumcncf  45833  ioccncflimc  45840  cncfuni  45841  icccncfext  45842  icocncflimc  45844  cncfiooicclem1  45848  cxpcncf2  45854  dvmptconst  45870  dvmptidg  45872  dvresntr  45873  itgsubsticclem  45930  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem32  46094  fourierdlem33  46095  fourierdlem62  46123  fourierdlem93  46154  fourierdlem101  46162