Theorem restutop 20906

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 455	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ b e. ( (unifTop ` U ) ↾t A ) ) -> ( U e. (UnifOn ` X ) /\ A C_ X ) )
2		fvex 5858	. . . . . . . 8 |- (unifTop ` U ) e. _V
3	2	a1i 11	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> (unifTop ` U ) e. _V )
4		elfvex 5875	. . . . . . . . 9 |- ( U e. (UnifOn ` X ) -> X e. _V )
5	4	adantr 463	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
6		simpr 459	. . . . . . . 8 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
7	5, 6	ssexd 4584	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
8		elrest 14917	. . . . . . 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 659	. . . . . 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 482	. . . . 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 3705	. . . . . . 7 |- ( a i^i A ) C_ A
12		sseq1 3510	. . . . . . 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 2943	. . . . 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 723	. . . . . . . . 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 733	. . . . . . . . . 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 6575	. . . . . . . . . 10 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
20	18, 18, 19	syl2anc 659	. . . . . . . . 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 753	. . . . . . . . 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 14918	. . . . . . . . 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 1226	. . . . . . . 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 3704	. . . . . . . . . . . . 13 |- ( u i^i ( A X. A ) ) C_ u
25		imass1 5359	. . . . . . . . . . . . 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 3497	. . . . . . . . . . . 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 668	. . . . . . . . . . 11 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
29		imassrn 5336	. . . . . . . . . . . . . . 15 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( u i^i ( A X. A ) )
30		rnin 5400	. . . . . . . . . . . . . . 15 |- ran ( u i^i ( A X. A ) ) C_ ( ran u i^i ran ( A X. A ) )
31	29, 30	sstri 3498	. . . . . . . . . . . . . 14 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ( ran u i^i ran ( A X. A ) )
32		inss2 3705	. . . . . . . . . . . . . 14 |- ( ran u i^i ran ( A X. A ) ) C_ ran ( A X. A )
33	31, 32	sstri 3498	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( A X. A )
34		rnxpid 5425	. . . . . . . . . . . . 13 |- ran ( A X. A ) = A
35	33, 34	sseqtri 3521	. . . . . . . . . . . 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 3708	. . . . . . . . . 10 |- ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( a i^i A ) )
38	37	adantl 464	. . . . . . . . 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 3526	. . . . . . . 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 5320	. . . . . . . . . 10 |- ( v = ( u i^i ( A X. A ) ) -> ( v " { x } ) = ( ( u i^i ( A X. A ) ) " { x } ) )
42	41	sseq1d 3516	. . . . . . . . 9 |- ( v = ( u i^i ( A X. A ) ) -> ( ( v " { x } ) C_ b <-> ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) )
43	42	rspcev 3207	. . . . . . . 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 659	. . . . . . 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 753	. . . . . . . 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 3704	. . . . . . . . 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 459	. . . . . . . . . 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 2544	. . . . . . . . 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 3487	. . . . . . . 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 20902	. . . . . . . . . 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 622	. . . . . . . . 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 2823	. . . . . . . 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 1225	. . . . . . 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 2996	. . . . . 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 463	. . . . . 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 2996	. . . . 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 2868	. . . 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 20898	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
60		elutop 20902	. . . . . 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 483	. . . 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 1224	. . 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 432	. 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 3495	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 367   = wceq 1398   e. wcel 1823   A.wral 2804   E.wrex 2805   _Vcvv 3106   i^i cin 3460   C_ wss 3461   {csn 4016   X. cxp 4986   ran crn 4989   "cima 4991   ` cfv 5570  (class class class)co 6270   ↾_t crest 14910  UnifOncust 20868  unifTopcutop 20899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-rest 14912  df-ust 20869  df-utop 20900

This theorem is referenced by:  restutopopn  20907