Theorem restutopopn 19772

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 19767	. . . 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 620	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> A C_ X )
3		restutop 19771	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )
4	2, 3	syldan 467	. 2 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )
5		trust 19763	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
6	2, 5	syldan 467	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
7		elutop 19767	. . . . . . . . . 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 620	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b C_ A )
10	2	adantr 462	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> A C_ X )
11	9, 10	sstrd 3363	. . . . . . 7 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b C_ X )
12		simp-9l 770	. . . . . . . . . . . . 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 749	. . . . . . . . . . . . 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 761	. . . . . . . . . . . . 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 19741	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ t e. U /\ w e. U ) -> ( t i^i w ) e. U )
16	12, 13, 14, 15	syl3anc 1213	. . . . . . . . . . . 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 5250	. . . . . . . . . . . . 13 |- ( ( t i^i w ) " { x } ) C_ ( ( t " { x } ) i^i ( w " { x } ) )
18		ssrin 3572	. . . . . . . . . . . . . . . 16 |- ( ( t " { x } ) C_ A -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ ( A i^i ( w " { x } ) ) )
19	18	adantl 463	. . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . . . . 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 5165	. . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . . . . . . 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 3354	. . . . . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . . . . . 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 2973	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
27		inimasn 5251	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. _V -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) )
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) )
29		disjsn 3933	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A i^i { x } ) = (/) <-> -. x e. A )
30	29	bicomi 202	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x e. A <-> ( A i^i { x } ) = (/) )
31	30	necon1abii 2660	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A i^i { x } ) =/= (/) <-> x e. A )
32		xpima2 5279	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A i^i { x } ) =/= (/) -> ( ( A X. A ) " { x } ) = A )
33	31, 32	sylbir 213	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. A -> ( ( A X. A ) " { x } ) = A )
34	33	ineq2d 3549	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) = ( ( w " { x } ) i^i A ) )
35	28, 34	syl5eq 2485	. . . . . . . . . . . . . . . . . 18 |- ( x e. A -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i A ) )
36		incom 3540	. . . . . . . . . . . . . . . . . 18 |- ( ( w " { x } ) i^i A ) = ( A i^i ( w " { x } ) )
37	35, 36	syl6eq 2489	. . . . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . 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 3390	. . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . 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 3363	. . . . . . . . . . . . 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 3364	. . . . . . . . . . . 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 5161	. . . . . . . . . . . . . 14 |- ( v = ( t i^i w ) -> ( v " { x } ) = ( ( t i^i w ) " { x } ) )
45	44	sseq1d 3380	. . . . . . . . . . . . 13 |- ( v = ( t i^i w ) -> ( ( v " { x } ) C_ b <-> ( ( t i^i w ) " { x } ) C_ b ) )
46	45	rspcev 3070	. . . . . . . . . . . 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 656	. . . . . . . . . . 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 760	. . . . . . . . . . . . 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 720	. . . . . . . . . . . 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 621	. . . . . . . . . . . . 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 2812	. . . . . . . . . . . 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 656	. . . . . . . . . . 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 2860	. . . . . . . . . 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 749	. . . . . . . . . . 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 6506	. . . . . . . . . . . . . 14 |- ( ( A e. (unifTop ` U ) /\ A e. (unifTop ` U ) ) -> ( A X. A ) e. _V )
56	55	anidms 640	. . . . . . . . . . . . 13 |- ( A e. (unifTop ` U ) -> ( A X. A ) e. _V )
57		elrest 14362	. . . . . . . . . . . . 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 471	. . . . . . . . . . . 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 481	. . . . . . . . . . 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 656	. . . . . . . . . 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 2860	. . . . . . . . 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 621	. . . . . . . . . 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 2812	. . . . . . . . 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 2860	. . . . . . . 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 2797	. . . . . . 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 19767	. . . . . . . 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 720	. . . . . . 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 908	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b e. (unifTop ` U ) )
69		df-ss 3339	. . . . . . . 8 |- ( b C_ A <-> ( b i^i A ) = b )
70	9, 69	sylib 196	. . . . . . 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 2446	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) /\ b e. (unifTop ` ( U ↾t ( A X. A ) ) ) ) -> b = ( b i^i A ) )
72		ineq1 3542	. . . . . . . 8 |- ( a = b -> ( a i^i A ) = ( b i^i A ) )
73	72	eqeq2d 2452	. . . . . . 7 |- ( a = b -> ( b = ( a i^i A ) <-> b = ( b i^i A ) ) )
74	73	rspcev 3070	. . . . . 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 656	. . . . 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 5698	. . . . . . 7 |- (unifTop ` U ) e. _V
77		elrest 14362	. . . . . . 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 665	. . . . . 6 |- ( A e. (unifTop ` U ) -> ( b e. ( (unifTop ` U ) ↾t A ) <-> E. a e. (unifTop ` U ) b = ( a i^i A ) ) )
79	78	ad2antlr 721	. . . . 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 232	. . . 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 434	. . 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 3359	. 2 |- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> (unifTop ` ( U ↾t ( A X. A ) ) ) C_ ( (unifTop ` U ) ↾t A ) )
83	4, 82	eqssd 3370	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 184   /\ wa 369   = wceq 1364   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   _Vcvv 2970   i^i cin 3324   C_ wss 3325   (/)c0 3634   {csn 3874   X. cxp 4834   "cima 4839   ` cfv 5415  (class class class)co 6090   ↾_t crest 14355  UnifOncust 19733  unifTopcutop 19764

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-1st 6576  df-2nd 6577  df-rest 14357  df-ust 19734  df-utop 19765

This theorem is referenced by:  ressusp  19799