Theorem resttopon 23484

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 23236	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2		id 23	. . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋)
3		toponmax 23249	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
4		ssexg 5280	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V)
5	2, 3, 4	syl2anr 609	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
6		resttop 23483	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
7	1, 5, 6	syl2an2r 698	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top)
8		sseqin2 4120	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
9	8	bilani 510	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴)
10		simpl 488	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
11	3	adantr 486	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽)
12		elrestr 17604	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
13	10, 5, 11, 12	syl3anc 1398	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
14	9, 13	eqeltrrd 2861	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴))
15		elssuni 4898	. . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
16	14, 15	syl 18	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴))
17		restval 17602	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
18	5, 17	syldan 603	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
19		inss2 4134	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
20		vex 3454	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
21	20	inex1 5276	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V
22	21	elpw 4560	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴)
23	19, 22	mpbir 234	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴
24	23	a1i 11	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴)
25	24	fmpttd 7115	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴)
26	25	frnd 6718	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴)
27	18, 26	eqsstrd 3942	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴)
28		sspwuni 5059	. . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
29	27, 28	sylib 221	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴)
30	16, 29	eqssd 3925	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
31		istopon 23235	. 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴)))
32	7, 30, 31	sylanbrc 595	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556  ∪ cuni 4866   ↦ cmpt 5185  ran crn 5651  ‘cfv 6538  (class class class)co 7420   ↾_t crest 17596  Topctop 23216  TopOnctopon 23233

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-en 8977  df-fin 8980  df-fi 9406  df-rest 17598  df-topgen 17619  df-top 23217  df-topon 23234  df-bases 23269

This theorem is used by:  restuni  23485  stoig  23486  restsn2  23494  restlp  23506  restperf  23507  perfopn  23508  cnrest  23608  cnrest2  23609  cnrest2r  23610  cnpresti  23611  cnprest  23612  cnprest2  23613  restcnrm  23685  connsuba  23743  kgentopon  23862  1stckgenlem  23877  kgen2ss  23879  kgencn  23880  xkoinjcn  24011  qtoprest  24041  flimrest  24307  fclsrest  24348  flfcntr  24367  efmndtmd  24425  symgtgp  24430  dvrcn  24508  sszcld  25142  divcn  25194  cncfmptc  25238  cncfmptid  25239  cncfmpt2f  25241  cdivcncf  25247  cnmpopc  25254  icchmeo  25267  htpycc  25306  pcocn  25343  pcohtpylem  25345  pcopt  25348  pcopt2  25349  pcoass  25350  pcorevlem  25352  relcmpcmet  25644  mulcncf  25772  limcvallem  26196  ellimc2  26202  limcres  26211  cnplimc  26212  cnlimc  26213  limccnp  26216  limccnp2  26217  dvbss  26226  perfdvf  26228  dvreslem  26234  dvres2lem  26235  dvcnp2  26245  dvcn  26246  dvaddbr  26263  dvmulbr  26264  dvcmulf  26270  dvmptres2  26287  dvmptcmul  26289  dvmptntr  26296  dvmptfsum  26300  dvcnvlem  26301  dvcnv  26302  lhop1lem  26338  lhop2  26340  lhop  26341  dvcnvrelem2  26343  dvcnvre  26344  ftc1lem3  26363  ftc1cn  26368  taylthlem1  26705  ulmdvlem3  26734  psercn  26758  abelth  26773  logcn  26980  cxpcn  27078  cxpcn2  27079  cxpcn3  27081  resqrtcn  27082  sqrtcn  27083  loglesqrt  27094  xrlimcnp  27301  efrlim  27302  ftalem3  27407  xrge0pluscn  34618  xrge0mulc1cn  34619  lmlimxrge0  34626  pnfneige0  34629  lmxrge0  34630  esumcvg  34764  cxpcncf1  35270  cvxpconn  36093  cvxsconn  36094  cvmsf1o  36123  cvmliftlem8  36143  cvmlift2lem9a  36154  cvmlift2lem11  36164  cvmlift3lem6  36175  ivthALT  37215  poimir  38664  broucube  38665  cnambfre  38679  ftc1cnnc  38703  areacirclem2  38720  areacirclem4  38722  fsumcncf  46981  ioccncflimc  46988  cncfuni  46989  icccncfext  46990  icocncflimc  46992  cncfiooicclem1  46996  cxpcncf2  47002  dvmptconst  47018  dvmptidg  47020  dvresntr  47021  itgsubsticclem  47078  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem32  47242  fourierdlem33  47243  fourierdlem62  47271  fourierdlem93  47302  fourierdlem101  47310