Theorem restid 16010

Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)

Hypothesis

Ref	Expression
restid.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
restid	⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽)

Proof of Theorem restid

Step	Hyp	Ref	Expression
1		restid.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2		uniexg 6909	. . 3 ⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V)
3	1, 2	syl5eqel 2708	. 2 ⊢ (𝐽 ∈ 𝑉 → 𝑋 ∈ V)
4	1	eqimss2i 3644	. . 3 ⊢ ∪ 𝐽 ⊆ 𝑋
5		sspwuni 4582	. . 3 ⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋)
6	4, 5	mpbir 221	. 2 ⊢ 𝐽 ⊆ 𝒫 𝑋
7		restid2 16007	. 2 ⊢ ((𝑋 ∈ V ∧ 𝐽 ⊆ 𝒫 𝑋) → (𝐽 ↾t 𝑋) = 𝐽)
8	3, 6, 7	sylancl 693	1 ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽)

Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1992  Vcvv 3191   ⊆ wss 3560  𝒫 cpw 4135  ∪ cuni 4407  (class class class)co 6605   ↾_t crest 15997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-rest 15999

This theorem is referenced by:  restin  20875  cnrmnrm  21070  cmpkgen  21259  xkopt  21363  xkoinjcn  21395  ussid  21969  tuslem  21976  cnperf  22526  retopconn  22535  cncfcn1  22616  cncfmpt2f  22620  cdivcncf  22623  abscncfALT  22626  cnmpt2pc  22630  cnrehmeo  22655  cnlimc  23553  recnperf  23570  dvidlem  23580  dvcnp2  23584  dvcn  23585  dvnres  23595  dvaddbr  23602  dvmulbr  23603  dvcobr  23610  dvcjbr  23613  dvrec  23619  dvexp3  23640  dveflem  23641  dvlipcn  23656  lhop1lem  23675  ftc1cn  23705  dvply1  23938  dvtaylp  24023  taylthlem2  24027  psercn  24079  pserdvlem2  24081  pserdv  24082  abelth  24094  logcn  24288  dvloglem  24289  dvlog  24292  dvlog2  24294  efopnlem2  24298  logtayl  24301  cxpcn  24381  cxpcn2  24382  cxpcn3  24384  resqrtcn  24385  sqrtcn  24386  dvatan  24557  ftalem3  24696  retopsconn  30931  ivthALT  31964  knoppcnlem10  32126  knoppcnlem11  32127  dvtan  33078  ftc1cnnc  33102  dvasin  33114  dvacos  33115  binomcxplemdvbinom  38020  binomcxplemnotnn0  38023  fsumcncf  39381  ioccncflimc  39389  cncfuni  39390  icocncflimc  39393  cncfiooicclem1  39397  cxpcncf2  39404  itgsubsticclem  39485  dirkercncflem2  39615  dirkercncflem4  39617  fourierdlem32  39650  fourierdlem33  39651  fourierdlem62  39679  fourierdlem93  39710  fourierdlem101  39718