Theorem restutopopn 18221

Description: The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)

Assertion

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

Proof of Theorem restutopopn

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

Step	Hyp	Ref	Expression
1		elutop 18216	. . . 4 |- ( U e. (UnifOn ` X ) -> ( A e. (unifTop ` U ) <-> ( A C_ X /\ A. x e. A E. t e. U ( t " { x } ) C_ A ) ) )
2	1	simprbda 607	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> A C_ X )
3		restutop 18220	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )
4	2, 3	syldan 457	. 2 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )
5		trust 18212	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
6	2, 5	syldan 457	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
7		elutop 18216	. . . . . . . . . 10 |- ( ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) -> ( b e. (unifTop ` ( U ↾t ( A X. A ) ) ) <-> ( b C_ A /\ A. x e. b E. u e. ( U ↾t ( A X. A ) ) ( u " { x } ) C_ b ) ) )
8	6, 7	syl 16	. . . . . . . . 9 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( b e. (unifTop ` ( U ↾t ( A X. A ) ) ) <-> ( b C_ A /\ A. x e. b E. u e. ( U ↾t ( A X. A ) ) ( u " { x } ) C_ b ) ) )
9	8	simprbda 607	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b C_ A )
10	2	adantr 452	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> A C_ X )
11	9, 10	sstrd 3318	. . . . . . 7 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b C_ X )
12		simp-9l 753	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> U e. (UnifOn ` X ) )
13		simplr 732	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> t e. U )
14		simp-4r 744	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> w e. U )
15		ustincl 18190	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ t e. U /\ w e. U ) -> ( t i^i w ) e. U )
16	12, 13, 14, 15	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( t i^i w ) e. U )
17		inimass 5247	. . . . . . . . . . . . 13 |- ( ( t i^i w ) " { x } ) C_ ( ( t " { x } ) i^i ( w " { x } ) )
18		ssrin 3526	. . . . . . . . . . . . . . . 16 |- ( ( t " { x } ) C_ A -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ ( A i^i ( w " { x } ) ) )
19	18	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ ( A i^i ( w " { x } ) ) )
20		simpllr 736	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> u = ( w i^i ( A X. A ) ) )
21	20	imaeq1d 5161	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( u " { x } ) = ( ( w i^i ( A X. A ) ) " { x } ) )
22	9	ad5antr 715	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> b C_ A )
23		simp-5r 746	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> x e. b )
24	22, 23	sseldd 3309	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> x e. A )
25	24	ad2antrr 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> x e. A )
26		vex 2919	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
27		inimasn 5248	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. _V -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) )
28	26, 27	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 |- ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) )
29		disjsn 3828	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A i^i { x } ) = (/) <-> -. x e. A )
30	29	bicomi 194	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x e. A <-> ( A i^i { x } ) = (/) )
31	30	necon1abii 2618	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A i^i { x } ) =/= (/) <-> x e. A )
32		xpima2 5274	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A i^i { x } ) =/= (/) -> ( ( A X. A ) " { x } ) = A )
33	31, 32	sylbir 205	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. A -> ( ( A X. A ) " { x } ) = A )
34	33	ineq2d 3502	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) = ( ( w " { x } ) i^i A ) )
35	28, 34	syl5eq 2448	. . . . . . . . . . . . . . . . . 18 |- ( x e. A -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i A ) )
36		incom 3493	. . . . . . . . . . . . . . . . . 18 |- ( ( w " { x } ) i^i A ) = ( A i^i ( w " { x } ) )
37	35, 36	syl6eq 2452	. . . . . . . . . . . . . . . . 17 |- ( x e. A -> ( ( w i^i ( A X. A ) ) " { x } ) = ( A i^i ( w " { x } ) ) )
38	25, 37	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( ( w i^i ( A X. A ) ) " { x } ) = ( A i^i ( w " { x } ) ) )
39	21, 38	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( u " { x } ) = ( A i^i ( w " { x } ) ) )
40	19, 39	sseqtr4d 3345	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ ( u " { x } ) )
41		simp-5r 746	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( u " { x } ) C_ b )
42	40, 41	sstrd 3318	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ b )
43	17, 42	syl5ss 3319	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> ( ( t i^i w ) " { x } ) C_ b )
44		imaeq1 5157	. . . . . . . . . . . . . 14 |- ( v = ( t i^i w ) -> ( v " { x } ) = ( ( t i^i w ) " { x } ) )
45	44	sseq1d 3335	. . . . . . . . . . . . 13 |- ( v = ( t i^i w ) -> ( ( v " { x } ) C_ b <-> ( ( t i^i w ) " { x } ) C_ b ) )
46	45	rspcev 3012	. . . . . . . . . . . 12 |- ( ( ( t i^i w ) e. U /\ ( ( t i^i w ) " { x } ) C_ b ) -> E. v e. U ( v " { x } ) C_ b )
47	16, 43, 46	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) /\ t e. U ) /\ ( t " { x } ) C_ A ) -> E. v e. U ( v " { x } ) C_ b )
48		simp-4l 743	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) -> ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) )
49	48	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) )
50	1	simplbda 608	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> A. x e. A E. t e. U ( t " { x } ) C_ A )
51	50	r19.21bi 2764	. . . . . . . . . . . 12 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ x e. A ) -> E. t e. U ( t " { x } ) C_ A )
52	49, 24, 51	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> E. t e. U ( t " { x } ) C_ A )
53	47, 52	r19.29a 2810	. . . . . . . . . 10 |- ( ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) /\ w e. U ) /\ u = ( w i^i ( A X. A ) ) ) -> E. v e. U ( v " { x } ) C_ b )
54		simplr 732	. . . . . . . . . . 11 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) -> u e. ( U ↾t ( A X. A ) ) )
55		xpexg 4948	. . . . . . . . . . . . . 14 |- ( ( A e. (unifTop ` U ) /\ A e. (unifTop ` U ) ) -> ( A X. A ) e. _V )
56	55	anidms 627	. . . . . . . . . . . . 13 |- ( A e. (unifTop ` U ) -> ( A X. A ) e. _V )
57		elrest 13610	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( u e. ( U ↾t ( A X. A ) ) <-> E. w e. U u = ( w i^i ( A X. A ) ) ) )
58	56, 57	sylan2 461	. . . . . . . . . . . 12 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( u e. ( U ↾t ( A X. A ) ) <-> E. w e. U u = ( w i^i ( A X. A ) ) ) )
59	58	biimpa 471	. . . . . . . . . . 11 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ u e. ( U ↾t ( A X. A ) ) ) -> E. w e. U u = ( w i^i ( A X. A ) ) )
60	48, 54, 59	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) -> E. w e. U u = ( w i^i ( A X. A ) ) )
61	53, 60	r19.29a 2810	. . . . . . . . 9 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) /\ u e. ( U ↾t ( A X. A ) ) ) /\ ( u " { x } ) C_ b ) -> E. v e. U ( v " { x } ) C_ b )
62	8	simplbda 608	. . . . . . . . . 10 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> A. x e. b E. u e. ( U ↾t ( A X. A ) ) ( u " { x } ) C_ b )
63	62	r19.21bi 2764	. . . . . . . . 9 |- ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) -> E. u e. ( U ↾t ( A X. A ) ) ( u " { x } ) C_ b )
64	61, 63	r19.29a 2810	. . . . . . . 8 |- ( ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) /\ x e. b ) -> E. v e. U ( v " { x } ) C_ b )
65	64	ralrimiva 2749	. . . . . . 7 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> A. x e. b E. v e. U ( v " { x } ) C_ b )
66		elutop 18216	. . . . . . . 8 |- ( U e. (UnifOn ` X ) -> ( b e. (unifTop ` U ) <-> ( b C_ X /\ A. x e. b E. v e. U ( v " { x } ) C_ b ) ) )
67	66	ad2antrr 707	. . . . . . 7 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> ( b e. (unifTop ` U ) <-> ( b C_ X /\ A. x e. b E. v e. U ( v " { x } ) C_ b ) ) )
68	11, 65, 67	mpbir2and 889	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b e. (unifTop ` U ) )
69		df-ss 3294	. . . . . . . 8 |- ( b C_ A <-> ( b i^i A ) = b )
70	9, 69	sylib 189	. . . . . . 7 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> ( b i^i A ) = b )
71	70	eqcomd 2409	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b = ( b i^i A ) )
72		ineq1 3495	. . . . . . . 8 |- ( a = b -> ( a i^i A ) = ( b i^i A ) )
73	72	eqeq2d 2415	. . . . . . 7 |- ( a = b -> ( b = ( a i^i A ) <-> b = ( b i^i A ) ) )
74	73	rspcev 3012	. . . . . 6 |- ( ( b e. (unifTop ` U ) /\ b = ( b i^i A ) ) -> E. a e. (unifTop ` U ) b = ( a i^i A ) )
75	68, 71, 74	syl2anc 643	. . . . 5 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> E. a e. (unifTop ` U ) b = ( a i^i A ) )
76		fvex 5701	. . . . . . 7 |- (unifTop ` U ) e. _V
77		elrest 13610	. . . . . . 7 |- ( ( (unifTop ` U ) e. _V /\ A e. (unifTop ` U ) ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
78	76, 77	mpan 652	. . . . . 6 |- ( A e. (unifTop ` U ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
79	78	ad2antlr 708	. . . . 5 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
80	75, 79	mpbird 224	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b e. ( (unifTop ` U ) ↾t A ) )
81	80	ex 424	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( b e. (unifTop ` ( U ↾t ( A X. A ) ) ) -> b e. ( (unifTop ` U ) ↾t A ) ) )
82	81	ssrdv 3314	. 2 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> (unifTop ` ( U ↾t ( A X. A ) ) ) C_ ( (unifTop ` U ) ↾t A ) )
83	4, 82	eqssd 3325	1 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( (unifTop ` U ) ↾t A ) = (unifTop ` ( U ↾t ( A X. A ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   i^i cin 3279   C_ wss 3280   (/)c0 3588   {csn 3774   X. cxp 4835   "cima 4840   ` cfv 5413  (class class class)co 6040   ↾_t crest 13603  UnifOncust 18182  unifTopcutop 18213

This theorem is referenced by:  ressusp  18248

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-rest 13605  df-ust 18183  df-utop 18214