Theorem restutop 19815

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 5704	. . . . . . . 8 |- (unifTop ` U ) e. _V
3	2	a1i 11	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> (unifTop ` U ) e. _V )
4		elfvex 5720	. . . . . . . . 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 4442	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
8		elrest 14369	. . . . . . 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 3574	. . . . . . 7 |- ( a i^i A ) C_ A
12		sseq1 3380	. . . . . . 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 2840	. . . . 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 6510	. . . . . . . . . 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 14370	. . . . . . . . 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 1218	. . . . . . . 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 3573	. . . . . . . . . . . . 13 |- ( u i^i ( A X. A ) ) C_ u
25		imass1 5206	. . . . . . . . . . . . 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 3367	. . . . . . . . . . . 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 5183	. . . . . . . . . . . . . . 15 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( u i^i ( A X. A ) )
30		rnin 5249	. . . . . . . . . . . . . . 15 |- ran ( u i^i ( A X. A ) ) C_ ( ran u i^i ran ( A X. A ) )
31	29, 30	sstri 3368	. . . . . . . . . . . . . 14 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ( ran u i^i ran ( A X. A ) )
32		inss2 3574	. . . . . . . . . . . . . 14 |- ( ran u i^i ran ( A X. A ) ) C_ ran ( A X. A )
33	31, 32	sstri 3368	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( A X. A )
34		rnxpid 5274	. . . . . . . . . . . . 13 |- ran ( A X. A ) = A
35	33, 34	sseqtri 3391	. . . . . . . . . . . 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 3577	. . . . . . . . . 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 3396	. . . . . . . 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 5167	. . . . . . . . . 10 |- ( v = ( u i^i ( A X. A ) ) -> ( v " { x } ) = ( ( u i^i ( A X. A ) ) " { x } ) )
42	41	sseq1d 3386	. . . . . . . . 9 |- ( v = ( u i^i ( A X. A ) ) -> ( ( v " { x } ) C_ b <-> ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) )
43	42	rspcev 3076	. . . . . . . 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 3573	. . . . . . . . 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 2519	. . . . . . . . 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 3357	. . . . . . . 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 19811	. . . . . . . . . 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 2817	. . . . . . . 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 1217	. . . . . . 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 2865	. . . . . 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 2865	. . . . 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 2802	. . . 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 19807	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
60		elutop 19811	. . . . . 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 1216	. . 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 3365	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 1369   e. wcel 1756   A.wral 2718   E.wrex 2719   _Vcvv 2975   i^i cin 3330   C_ wss 3331   {csn 3880   X. cxp 4841   ran crn 4844   "cima 4846   ` cfv 5421  (class class class)co 6094   ↾_t crest 14362  UnifOncust 19777  unifTopcutop 19808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-reu 2725  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-1st 6580  df-2nd 6581  df-rest 14364  df-ust 19778  df-utop 19809

This theorem is referenced by:  restutopopn  19816