Theorem ressusp 24400

Description: The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017.)

Hypotheses

Ref	Expression
ressusp.1	⊢ 𝐵 = (Base‘𝑊)
ressusp.2	⊢ 𝐽 = (TopOpen‘𝑊)

Assertion

Ref	Expression
ressusp	⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝑊 ↾s 𝐴) ∈ UnifSp)

Proof of Theorem ressusp

Step	Hyp	Ref	Expression
1		ressuss 24398	. . . . 5 ⊢ (𝐴 ∈ 𝐽 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))
2	1	3ad2ant3 1151	. . . 4 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))
3		simp1 1152	. . . . . . 7 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝑊 ∈ UnifSp)
4		ressusp.1	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
5		eqid 2761	. . . . . . . 8 ⊢ (UnifSt‘𝑊) = (UnifSt‘𝑊)
6		ressusp.2	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝑊)
7	4, 5, 6	isusp 24397	. . . . . . 7 ⊢ (𝑊 ∈ UnifSp ↔ ((UnifSt‘𝑊) ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑊))))
8	3, 7	sylib 221	. . . . . 6 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((UnifSt‘𝑊) ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑊))))
9	8	simpld 499	. . . . 5 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘𝑊) ∈ (UnifOn‘𝐵))
10		simp2 1153	. . . . . . 7 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝑊 ∈ TopSp)
11	4, 6	istps 23070	. . . . . . 7 ⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵))
12	10, 11	sylib 221	. . . . . 6 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝐵))
13		simp3 1154	. . . . . 6 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ 𝐽)
14		toponss 23063	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝐵)
15	12, 13, 14	syl2anc 595	. . . . 5 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝐵)
16		trust 24365	. . . . 5 ⊢ (((UnifSt‘𝑊) ∈ (UnifOn‘𝐵) ∧ 𝐴 ⊆ 𝐵) → ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
17	9, 15, 16	syl2anc 595	. . . 4 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
18	2, 17	eqeltrd 2861	. . 3 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) ∈ (UnifOn‘𝐴))
19		eqid 2761	. . . . . 6 ⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴)
20	19, 4	ressbas2 17297	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝑊 ↾s 𝐴)))
21	15, 20	syl 18	. . . 4 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 = (Base‘(𝑊 ↾s 𝐴)))
22	21	fveq2d 6885	. . 3 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifOn‘𝐴) = (UnifOn‘(Base‘(𝑊 ↾s 𝐴))))
23	18, 22	eleqtrd 2863	. 2 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) ∈ (UnifOn‘(Base‘(𝑊 ↾s 𝐴))))
24	8	simprd 500	. . . . 5 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐽 = (unifTop‘(UnifSt‘𝑊)))
25	13, 24	eleqtrd 2863	. . . 4 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ (unifTop‘(UnifSt‘𝑊)))
26		restutopopn 24374	. . . 4 ⊢ (((UnifSt‘𝑊) ∈ (UnifOn‘𝐵) ∧ 𝐴 ∈ (unifTop‘(UnifSt‘𝑊))) → ((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴) = (unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))))
27	9, 25, 26	syl2anc 595	. . 3 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴) = (unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))))
28	24	oveq1d 7425	. . 3 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝐽 ↾t 𝐴) = ((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴))
29	2	fveq2d 6885	. . 3 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴))) = (unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))))
30	27, 28, 29	3eqtr4d 2806	. 2 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝐽 ↾t 𝐴) = (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴))))
31		eqid 2761	. . 3 ⊢ (Base‘(𝑊 ↾s 𝐴)) = (Base‘(𝑊 ↾s 𝐴))
32		eqid 2761	. . 3 ⊢ (UnifSt‘(𝑊 ↾s 𝐴)) = (UnifSt‘(𝑊 ↾s 𝐴))
33	19, 6	resstopn 23322	. . 3 ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘(𝑊 ↾s 𝐴))
34	31, 32, 33	isusp 24397	. 2 ⊢ ((𝑊 ↾s 𝐴) ∈ UnifSp ↔ ((UnifSt‘(𝑊 ↾s 𝐴)) ∈ (UnifOn‘(Base‘(𝑊 ↾s 𝐴))) ∧ (𝐽 ↾t 𝐴) = (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴)))))
35	23, 30, 34	sylanbrc 594	1 ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝑊 ↾s 𝐴) ∈ UnifSp)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141   ⊆ wss 3904   × cxp 5659  ‘cfv 6536  (class class class)co 7410  Basecbs 17268   ↾_s cress 17289   ↾_t crest 17472  TopOpenctopn 17473  TopOnctopon 23046  TopSpctps 23068  UnifOncust 24336  unifTopcutop 24366  UnifStcuss 24389  UnifSpcusp 24390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-z 12591  df-dec 12711  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-tset 17328  df-unif 17332  df-rest 17474  df-topn 17475  df-top 23030  df-topon 23047  df-topsp 23069  df-ust 24337  df-utop 24367  df-uss 24392  df-usp 24393

This theorem is referenced by: (None)