Theorem restutop 21262

Description: Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.)

Assertion

Ref	Expression
restutop	|- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )

Proof of Theorem restutop

Dummy variables a b u v x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 463	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> ( U e. (UnifOn ` X ) /\ A C_ X ) )
2		fvex 5857	. . . . . . . 8 |- (unifTop ` U ) e. _V
3	2	a1i 11	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> (unifTop ` U ) e. _V )
4		elfvex 5874	. . . . . . . . 9 |- ( U e. (UnifOn ` X ) -> X e. _V )
5	4	adantr 471	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
6		simpr 467	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
7	5, 6	ssexd 4521	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
8		elrest 15336	. . . . . . 7 |- ( ( (unifTop ` U ) e. _V /\ A e. _V ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
9	3, 7, 8	syl2anc 671	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
10	9	biimpa 491	. . . . 5 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> E. a e. (unifTop ` U ) b = ( a i^i A ) )
11		inss2 3620	. . . . . . 7 |- ( a i^i A ) C_ A
12		sseq1 3420	. . . . . . 7 |- ( b = ( a i^i A ) -> ( b C_ A <-> ( a i^i A ) C_ A ) )
13	11, 12	mpbiri 241	. . . . . 6 |- ( b = ( a i^i A ) -> b C_ A )
14	13	rexlimivw 2849	. . . . 5 |- ( E. a e. (unifTop ` U ) b = ( a i^i A ) -> b C_ A )
15	10, 14	syl 17	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> b C_ A )
16		simp-5l 783	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> U e. (UnifOn ` X ) )
17	16	ad2antrr 737	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> U e. (UnifOn ` X ) )
18	7	ad6antr 747	. . . . . . . . . 10 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> A e. _V )
19		xpexg 6580	. . . . . . . . . 10 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
20	18, 18, 19	syl2anc 671	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> ( A X. A ) e. _V )
21		simplr 767	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> u e. U )
22		elrestr 15337	. . . . . . . . 9 |- ( ( U e. (UnifOn ` X ) /\ ( A X. A ) e. _V /\ u e. U ) -> ( u i^i ( A X. A ) ) e. ( U ↾t ( A X. A ) ) )
23	17, 20, 21, 22	syl3anc 1271	. . . . . . . 8 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> ( u i^i ( A X. A ) ) e. ( U ↾t ( A X. A ) ) )
24		inss1 3619	. . . . . . . . . . . . 13 |- ( u i^i ( A X. A ) ) C_ u
25		imass1 5180	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) C_ u -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } ) )
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } )
27		sstr 3407	. . . . . . . . . . . 12 |- ( ( ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } ) /\ ( u " { x } ) C_ a ) -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
28	26, 27	mpan 681	. . . . . . . . . . 11 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
29		imassrn 5156	. . . . . . . . . . . . . . 15 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( u i^i ( A X. A ) )
30		rnin 5222	. . . . . . . . . . . . . . 15 |- ran ( u i^i ( A X. A ) ) C_ ( ran u i^i ran ( A X. A ) )
31	29, 30	sstri 3408	. . . . . . . . . . . . . 14 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ( ran u i^i ran ( A X. A ) )
32		inss2 3620	. . . . . . . . . . . . . 14 |- ( ran u i^i ran ( A X. A ) ) C_ ran ( A X. A )
33	31, 32	sstri 3408	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( A X. A )
34		rnxpid 5247	. . . . . . . . . . . . 13 |- ran ( A X. A ) = A
35	33, 34	sseqtri 3431	. . . . . . . . . . . 12 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ A
36	35	a1i 11	. . . . . . . . . . 11 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ A )
37	28, 36	ssind 3623	. . . . . . . . . 10 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( a i^i A ) )
38	37	adantl 472	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( a i^i A ) )
39		simpllr 774	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> b = ( a i^i A ) )
40	38, 39	sseqtr4d 3436	. . . . . . . 8 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> ( ( u i^i ( A X. A ) ) " { x } ) C_ b )
41		imaeq1 5140	. . . . . . . . . 10 |- ( v = ( u i^i ( A X. A ) ) -> ( v " { x } ) = ( ( u i^i ( A X. A ) ) " { x } ) )
42	41	sseq1d 3426	. . . . . . . . 9 |- ( v = ( u i^i ( A X. A ) ) -> ( ( v " { x } ) C_ b <-> ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) )
43	42	rspcev 3117	. . . . . . . 8 |- ( ( ( u i^i ( A X. A ) ) e. ( U ↾t ( A X. A ) ) /\ ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) -> E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b )
44	23, 40, 43	syl2anc 671	. . . . . . 7 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) /\ u e. U ) /\ ( u " { x } ) C_ a ) -> E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b )
45		simplr 767	. . . . . . . 8 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> a e. (unifTop ` U ) )
46		inss1 3619	. . . . . . . . 9 |- ( a i^i A ) C_ a
47		simpllr 774	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> x e. b )
48		simpr 467	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> b = ( a i^i A ) )
49	47, 48	eleqtrd 2531	. . . . . . . . 9 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> x e. ( a i^i A ) )
50	46, 49	sseldi 3397	. . . . . . . 8 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> x e. a )
51		elutop 21258	. . . . . . . . . 10 |- ( U e. (UnifOn ` X ) -> ( a e. (unifTop ` U ) <-> ( a C_ X /\ A. x e. a E. u e. U ( u " { x } ) C_ a ) ) )
52	51	simplbda 634	. . . . . . . . 9 |- ( ( U e. (UnifOn ` X ) /\ a e. (unifTop ` U ) ) -> A. x e. a E. u e. U ( u " { x } ) C_ a )
53	52	r19.21bi 2756	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ a e. (unifTop ` U ) ) /\ x e. a ) -> E. u e. U ( u " { x } ) C_ a )
54	16, 45, 50, 53	syl21anc 1270	. . . . . . 7 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> E. u e. U ( u " { x } ) C_ a )
55	44, 54	r19.29a 2899	. . . . . 6 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) /\ a e. (unifTop ` U ) ) /\ b = ( a i^i A ) ) -> E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b )
56	10	adantr 471	. . . . . 6 |- ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) -> E. a e. (unifTop ` U ) b = ( a i^i A ) )
57	55, 56	r19.29a 2899	. . . . 5 |- ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) /\ x e. b ) -> E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b )
58	57	ralrimiva 2789	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> A. x e. b E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b )
59		trust 21254	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
60		elutop 21258	. . . . . 6 |- ( ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) -> ( b e. (unifTop ` ( U ↾t ( A X. A ) ) ) <-> ( b C_ A /\ A. x e. b E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b ) ) )
61	59, 60	syl 17	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( b e. (unifTop ` ( U ↾t ( A X. A ) ) ) <-> ( b C_ A /\ A. x e. b E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b ) ) )
62	61	biimpar 492	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ ( b C_ A /\ A. x e. b E. v e. ( U ↾t ( A X. A ) ) ( v " { x } ) C_ b ) ) -> b e. (unifTop ` ( U ↾t ( A X. A ) ) ) )
63	1, 15, 58, 62	syl12anc 1269	. . 3 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> b e. (unifTop ` ( U ↾t ( A X. A ) ) ) )
64	63	ex 440	. 2 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( b e. ( (unifTop ` U ) ↾t A ) -> b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) )
65	64	ssrdv 3405	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1447   e. wcel 1890   A.wral 2736   E.wrex 2737   _Vcvv 3012   i^i cin 3370   C_ wss 3371   {csn 3935   X. cxp 4809   ran crn 4812   "cima 4814   ` cfv 5560  (class class class)co 6275   ↾_t crest 15329  UnifOncust 21224  unifTopcutop 21255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6780  df-2nd 6781  df-rest 15331  df-ust 21225  df-utop 21256

This theorem is referenced by:  restutopopn  21263