Theorem restutop 20567

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 457	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> ( U e. (UnifOn ` X ) /\ A C_ X ) )
2		fvex 5876	. . . . . . . 8 |- (unifTop ` U ) e. _V
3	2	a1i 11	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> (unifTop ` U ) e. _V )
4		elfvex 5893	. . . . . . . . 9 |- ( U e. (UnifOn ` X ) -> X e. _V )
5	4	adantr 465	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
6		simpr 461	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
7	5, 6	ssexd 4594	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
8		elrest 14686	. . . . . . 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 661	. . . . . 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 484	. . . . 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 3719	. . . . . . 7 |- ( a i^i A ) C_ A
12		sseq1 3525	. . . . . . 7 |- ( b = ( a i^i A ) -> ( b C_ A <-> ( a i^i A ) C_ A ) )
13	11, 12	mpbiri 233	. . . . . 6 |- ( b = ( a i^i A ) -> b C_ A )
14	13	rexlimivw 2952	. . . . 5 |- ( E. a e. (unifTop ` U ) b = ( a i^i A ) -> b C_ A )
15	10, 14	syl 16	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> b C_ A )
16		simp-5l 767	. . . . . . . . . 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 725	. . . . . . . . 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 735	. . . . . . . . . 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 6587	. . . . . . . . . 10 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
20	18, 18, 19	syl2anc 661	. . . . . . . . 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 754	. . . . . . . . 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 14687	. . . . . . . . 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 1228	. . . . . . . 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 3718	. . . . . . . . . . . . 13 |- ( u i^i ( A X. A ) ) C_ u
25		imass1 5371	. . . . . . . . . . . . 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 3512	. . . . . . . . . . . 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 670	. . . . . . . . . . 11 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
29		imassrn 5348	. . . . . . . . . . . . . . 15 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( u i^i ( A X. A ) )
30		rnin 5415	. . . . . . . . . . . . . . 15 |- ran ( u i^i ( A X. A ) ) C_ ( ran u i^i ran ( A X. A ) )
31	29, 30	sstri 3513	. . . . . . . . . . . . . 14 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ( ran u i^i ran ( A X. A ) )
32		inss2 3719	. . . . . . . . . . . . . 14 |- ( ran u i^i ran ( A X. A ) ) C_ ran ( A X. A )
33	31, 32	sstri 3513	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( A X. A )
34		rnxpid 5440	. . . . . . . . . . . . 13 |- ran ( A X. A ) = A
35	33, 34	sseqtri 3536	. . . . . . . . . . . 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 3722	. . . . . . . . . 10 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( a i^i A ) )
38	37	adantl 466	. . . . . . . . 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 758	. . . . . . . . 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 3541	. . . . . . . 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 5332	. . . . . . . . . 10 |- ( v = ( u i^i ( A X. A ) ) -> ( v " { x } ) = ( ( u i^i ( A X. A ) ) " { x } ) )
42	41	sseq1d 3531	. . . . . . . . 9 |- ( v = ( u i^i ( A X. A ) ) -> ( ( v " { x } ) C_ b <-> ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) )
43	42	rspcev 3214	. . . . . . . 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 661	. . . . . . 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 754	. . . . . . . 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 3718	. . . . . . . . 9 |- ( a i^i A ) C_ a
47		simpllr 758	. . . . . . . . . 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 461	. . . . . . . . . 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 2557	. . . . . . . . 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 3502	. . . . . . . 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 20563	. . . . . . . . . 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 624	. . . . . . . . 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 2833	. . . . . . . 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 1227	. . . . . . 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 3003	. . . . . 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 465	. . . . . 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 3003	. . . . 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 2878	. . . 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 20559	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
60		elutop 20563	. . . . . 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 16	. . . . 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 485	. . . 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 1226	. . 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 434	. 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 3510	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   A.wral 2814   E.wrex 2815   _Vcvv 3113   i^i cin 3475   C_ wss 3476   {csn 4027   X. cxp 4997   ran crn 5000   "cima 5002   ` cfv 5588  (class class class)co 6285   ↾_t crest 14679  UnifOncust 20529  unifTopcutop 20560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-1st 6785  df-2nd 6786  df-rest 14681  df-ust 20530  df-utop 20561

This theorem is referenced by:  restutopopn  20568