Metamath Proof Explorer

Theorem restutop

Description: Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ b e. ( ( unifTop ` U ) |`t A ) ) -> ( U e. ( UnifOn ` X ) /\ A C_ X ) )
2 fvexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( unifTop ` U ) e. _V )
3 elfvex 
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
4 3 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> X e. _V )
5 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A C_ X )
6 4 5 ssexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A e. _V )
7 elrest 
 |-  ( ( ( unifTop ` U ) e. _V /\ A e. _V ) -> ( b e. ( ( unifTop ` U ) |`t A ) <-> E. a e. ( unifTop ` U ) b = ( a i^i A ) ) )
8 2 6 7 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( b e. ( ( unifTop ` U ) |`t A ) <-> E. a e. ( unifTop ` U ) b = ( a i^i A ) ) )
9 8 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ b e. ( ( unifTop ` U ) |`t A ) ) -> E. a e. ( unifTop ` U ) b = ( a i^i A ) )
10 inss2 
 |-  ( a i^i A ) C_ A
11 sseq1 
 |-  ( b = ( a i^i A ) -> ( b C_ A <-> ( a i^i A ) C_ A ) )
12 10 11 mpbiri 
 |-  ( b = ( a i^i A ) -> b C_ A )
13 12 rexlimivw 
 |-  ( E. a e. ( unifTop ` U ) b = ( a i^i A ) -> b C_ A )
14 9 13 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ b e. ( ( unifTop ` U ) |`t A ) ) -> b C_ A )
15 simp-5l 
 |-  ( ( ( ( ( ( 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 ) )
16 15 ad2antrr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
17 6 ad6antr 
 |-  ( ( ( ( ( ( ( ( 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 )
18 17 17 xpexd 
 |-  ( ( ( ( ( ( ( ( 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 )
19 simplr 
 |-  ( ( ( ( ( ( ( ( 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 )
20 elrestr 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V /\ u e. U ) -> ( u i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
21 16 18 19 20 syl3anc 
 |-  ( ( ( ( ( ( ( ( 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 ) ) )
22 inss1 
 |-  ( u i^i ( A X. A ) ) C_ u
23 imass1 
 |-  ( ( u i^i ( A X. A ) ) C_ u -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } ) )
24 22 23 ax-mp 
 |-  ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } )
25 sstr 
 |-  ( ( ( ( u i^i ( A X. A ) ) " { x } ) C_ ( u " { x } ) /\ ( u " { x } ) C_ a ) -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
26 24 25 mpan 
 |-  ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ a )
27 imassrn 
 |-  ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( u i^i ( A X. A ) )
28 rnin 
 |-  ran ( u i^i ( A X. A ) ) C_ ( ran u i^i ran ( A X. A ) )
29 27 28 sstri 
 |-  ( ( u i^i ( A X. A ) ) " { x } ) C_ ( ran u i^i ran ( A X. A ) )
30 inss2 
 |-  ( ran u i^i ran ( A X. A ) ) C_ ran ( A X. A )
31 29 30 sstri 
 |-  ( ( u i^i ( A X. A ) ) " { x } ) C_ ran ( A X. A )
32 rnxpid 
 |-  ran ( A X. A ) = A
33 31 32 sseqtri 
 |-  ( ( u i^i ( A X. A ) ) " { x } ) C_ A
34 33 a1i 
 |-  ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ A )
35 26 34 ssind 
 |-  ( ( u " { x } ) C_ a -> ( ( u i^i ( A X. A ) ) " { x } ) C_ ( a i^i A ) )
36 35 adantl 
 |-  ( ( ( ( ( ( ( ( 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 ) )
37 simpllr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
38 36 37 sseqtrrd 
 |-  ( ( ( ( ( ( ( ( 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 )
39 imaeq1 
 |-  ( v = ( u i^i ( A X. A ) ) -> ( v " { x } ) = ( ( u i^i ( A X. A ) ) " { x } ) )
40 39 sseq1d 
 |-  ( v = ( u i^i ( A X. A ) ) -> ( ( v " { x } ) C_ b <-> ( ( u i^i ( A X. A ) ) " { x } ) C_ b ) )
41 40 rspcev 
 |-  ( ( ( 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 )
42 21 38 41 syl2anc 
 |-  ( ( ( ( ( ( ( ( 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 )
43 simplr 
 |-  ( ( ( ( ( ( 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 ) )
44 simpllr 
 |-  ( ( ( ( ( ( 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 )
45 simpr 
 |-  ( ( ( ( ( ( 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 ) )
46 44 45 eleqtrd 
 |-  ( ( ( ( ( ( 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 ) )
47 46 elin1d 
 |-  ( ( ( ( ( ( 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 )
48 elutop 
 |-  ( U e. ( UnifOn ` X ) -> ( a e. ( unifTop ` U ) <-> ( a C_ X /\ A. x e. a E. u e. U ( u " { x } ) C_ a ) ) )
49 48 simplbda 
 |-  ( ( U e. ( UnifOn ` X ) /\ a e. ( unifTop ` U ) ) -> A. x e. a E. u e. U ( u " { x } ) C_ a )
50 49 r19.21bi 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ( unifTop ` U ) ) /\ x e. a ) -> E. u e. U ( u " { x } ) C_ a )
51 15 43 47 50 syl21anc 
 |-  ( ( ( ( ( ( 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 )
52 42 51 r19.29a 
 |-  ( ( ( ( ( ( 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 )
53 9 adantr 
 |-  ( ( ( ( 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 ) )
54 52 53 r19.29a 
 |-  ( ( ( ( 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 )
55 54 ralrimiva 
 |-  ( ( ( 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 )
56 trust 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
57 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. v e. ( U |`t ( A X. A ) ) ( v " { x } ) C_ b ) ) )
58 56 57 syl 
 |-  ( ( 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 ) ) )
59 58 biimpar 
 |-  ( ( ( 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 ) ) ) )
60 1 14 55 59 syl12anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ b e. ( ( unifTop ` U ) |`t A ) ) -> b e. ( unifTop ` ( U |`t ( A X. A ) ) ) )
61 60 ex 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( b e. ( ( unifTop ` U ) |`t A ) -> b e. ( unifTop ` ( U |`t ( A X. A ) ) ) ) )
62 61 ssrdv 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( unifTop ` U ) |`t A ) C_ ( unifTop ` ( U |`t ( A X. A ) ) ) )