Metamath Proof Explorer

Theorem restutopopn

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

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

Proof

Step Hyp Ref Expression
1 elutop 
 |-  ( 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 
 |-  ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) -> A C_ X )
3 restutop 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( unifTop ` U ) |`t A ) C_ ( unifTop ` ( U |`t ( A X. A ) ) ) )
4 2 3 syldan 
 |-  ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) -> ( ( unifTop ` U ) |`t A ) C_ ( unifTop ` ( U |`t ( A X. A ) ) ) )
5 trust 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
6 2 5 syldan 
 |-  ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
7 elutop 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> b C_ A )
10 2 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> A C_ X )
11 9 10 sstrd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> b C_ X )
12 simp-9l 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( U e. ( UnifOn ` X ) /\ t e. U /\ w e. U ) -> ( t i^i w ) e. U )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( t i^i w ) " { x } ) C_ ( ( t " { x } ) i^i ( w " { x } ) )
18 ssrin 
 |-  ( ( t " { x } ) C_ A -> ( ( t " { x } ) i^i ( w " { x } ) ) C_ ( A i^i ( w " { x } ) ) )
19 18 adantl 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( ( ( 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 inimasn 
 |-  ( x e. _V -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) )
27 26 elv 
 |-  ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) )
28 xpimasn 
 |-  ( x e. A -> ( ( A X. A ) " { x } ) = A )
29 28 ineq2d 
 |-  ( x e. A -> ( ( w " { x } ) i^i ( ( A X. A ) " { x } ) ) = ( ( w " { x } ) i^i A ) )
30 27 29 syl5eq 
 |-  ( x e. A -> ( ( w i^i ( A X. A ) ) " { x } ) = ( ( w " { x } ) i^i A ) )
31 incom 
 |-  ( ( w " { x } ) i^i A ) = ( A i^i ( w " { x } ) )
32 30 31 eqtrdi 
 |-  ( x e. A -> ( ( w i^i ( A X. A ) ) " { x } ) = ( A i^i ( w " { x } ) ) )
33 25 32 syl 
 |-  ( ( ( ( ( ( ( ( ( ( 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 } ) ) )
34 21 33 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( 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 } ) ) )
35 19 34 sseqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( 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 } ) )
36 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( 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 )
37 35 36 sstrd 
 |-  ( ( ( ( ( ( ( ( ( ( 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 )
38 17 37 sstrid 
 |-  ( ( ( ( ( ( ( ( ( ( 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 )
39 imaeq1 
 |-  ( v = ( t i^i w ) -> ( v " { x } ) = ( ( t i^i w ) " { x } ) )
40 39 sseq1d 
 |-  ( v = ( t i^i w ) -> ( ( v " { x } ) C_ b <-> ( ( t i^i w ) " { x } ) C_ b ) )
41 40 rspcev 
 |-  ( ( ( t i^i w ) e. U /\ ( ( t i^i w ) " { x } ) C_ b ) -> E. v e. U ( v " { x } ) C_ b )
42 16 38 41 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( 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 )
43 simp-4l 
 |-  ( ( ( ( ( ( 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 ) ) )
44 43 ad2antrr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) )
45 1 simplbda 
 |-  ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) -> A. x e. A E. t e. U ( t " { x } ) C_ A )
46 45 r19.21bi 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ x e. A ) -> E. t e. U ( t " { x } ) C_ A )
47 44 24 46 syl2anc 
 |-  ( ( ( ( ( ( ( ( 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 )
48 42 47 r19.29a 
 |-  ( ( ( ( ( ( ( ( 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 )
49 simplr 
 |-  ( ( ( ( ( ( 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 ) ) )
50 sqxpexg 
 |-  ( A e. ( unifTop ` U ) -> ( A X. A ) e. _V )
51 elrest 
 |-  ( ( 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 ) ) ) )
52 50 51 sylan2 
 |-  ( ( 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 ) ) ) )
53 52 biimpa 
 |-  ( ( ( 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 ) ) )
54 43 49 53 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) )
55 48 54 r19.29a 
 |-  ( ( ( ( ( ( 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 )
56 8 simplbda 
 |-  ( ( ( 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 )
57 56 r19.21bi 
 |-  ( ( ( ( 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 )
58 55 57 r19.29a 
 |-  ( ( ( ( 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 )
59 58 ralrimiva 
 |-  ( ( ( 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 )
60 elutop 
 |-  ( U e. ( UnifOn ` X ) -> ( b e. ( unifTop ` U ) <-> ( b C_ X /\ A. x e. b E. v e. U ( v " { x } ) C_ b ) ) )
61 60 ad2antrr 
 |-  ( ( ( 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 ) ) )
62 11 59 61 mpbir2and 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> b e. ( unifTop ` U ) )
63 df-ss 
 |-  ( b C_ A <-> ( b i^i A ) = b )
64 9 63 sylib 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> ( b i^i A ) = b )
65 64 eqcomd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> b = ( b i^i A ) )
66 ineq1 
 |-  ( a = b -> ( a i^i A ) = ( b i^i A ) )
67 66 rspceeqv 
 |-  ( ( b e. ( unifTop ` U ) /\ b = ( b i^i A ) ) -> E. a e. ( unifTop ` U ) b = ( a i^i A ) )
68 62 65 67 syl2anc 
 |-  ( ( ( 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 ) )
69 fvex 
 |-  ( unifTop ` U ) e. _V
70 elrest 
 |-  ( ( ( unifTop ` U ) e. _V /\ A e. ( unifTop ` U ) ) -> ( b e. ( ( unifTop ` U ) |`t A ) <-> E. a e. ( unifTop ` U ) b = ( a i^i A ) ) )
71 69 70 mpan 
 |-  ( A e. ( unifTop ` U ) -> ( b e. ( ( unifTop ` U ) |`t A ) <-> E. a e. ( unifTop ` U ) b = ( a i^i A ) ) )
72 71 ad2antlr 
 |-  ( ( ( 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 ) ) )
73 68 72 mpbird 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) /\ b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) -> b e. ( ( unifTop ` U ) |`t A ) )
74 4 73 eqelssd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A e. ( unifTop ` U ) ) -> ( ( unifTop ` U ) |`t A ) = ( unifTop ` ( U |`t ( A X. A ) ) ) )