Metamath Proof Explorer

Theorem restntr

Description: An interior in a subspace topology. Willard inGeneral Topology says that there is no analogue of restcls for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypotheses restcls.1 
|- X = U. J
restcls.2 
|- K = ( J |`t Y )
Assertion restntr 
|- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) = ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 restcls.1 
 |-  X = U. J
2 restcls.2 
 |-  K = ( J |`t Y )
3 2 fveq2i 
 |-  ( int ` K ) = ( int ` ( J |`t Y ) )
4 3 fveq1i 
 |-  ( ( int ` K ) ` S ) = ( ( int ` ( J |`t Y ) ) ` S )
5 1 topopn 
 |-  ( J e. Top -> X e. J )
6 ssexg 
 |-  ( ( Y C_ X /\ X e. J ) -> Y e. _V )
7 6 ancoms 
 |-  ( ( X e. J /\ Y C_ X ) -> Y e. _V )
8 5 7 sylan 
 |-  ( ( J e. Top /\ Y C_ X ) -> Y e. _V )
9 resttop 
 |-  ( ( J e. Top /\ Y e. _V ) -> ( J |`t Y ) e. Top )
10 8 9 syldan 
 |-  ( ( J e. Top /\ Y C_ X ) -> ( J |`t Y ) e. Top )
11 10 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( J |`t Y ) e. Top )
12 1 restuni 
 |-  ( ( J e. Top /\ Y C_ X ) -> Y = U. ( J |`t Y ) )
13 12 sseq2d 
 |-  ( ( J e. Top /\ Y C_ X ) -> ( S C_ Y <-> S C_ U. ( J |`t Y ) ) )
14 13 biimp3a 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ U. ( J |`t Y ) )
15 eqid 
 |-  U. ( J |`t Y ) = U. ( J |`t Y )
16 15 ntropn 
 |-  ( ( ( J |`t Y ) e. Top /\ S C_ U. ( J |`t Y ) ) -> ( ( int ` ( J |`t Y ) ) ` S ) e. ( J |`t Y ) )
17 11 14 16 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` ( J |`t Y ) ) ` S ) e. ( J |`t Y ) )
18 4 17 eqeltrid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) e. ( J |`t Y ) )
19 simp1 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> J e. Top )
20 uniexg 
 |-  ( J e. Top -> U. J e. _V )
21 1 20 eqeltrid 
 |-  ( J e. Top -> X e. _V )
22 ssexg 
 |-  ( ( Y C_ X /\ X e. _V ) -> Y e. _V )
23 21 22 sylan2 
 |-  ( ( Y C_ X /\ J e. Top ) -> Y e. _V )
24 23 ancoms 
 |-  ( ( J e. Top /\ Y C_ X ) -> Y e. _V )
25 24 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> Y e. _V )
26 elrest 
 |-  ( ( J e. Top /\ Y e. _V ) -> ( ( ( int ` K ) ` S ) e. ( J |`t Y ) <-> E. o e. J ( ( int ` K ) ` S ) = ( o i^i Y ) ) )
27 19 25 26 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` K ) ` S ) e. ( J |`t Y ) <-> E. o e. J ( ( int ` K ) ` S ) = ( o i^i Y ) ) )
28 18 27 mpbid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> E. o e. J ( ( int ` K ) ` S ) = ( o i^i Y ) )
29 1 eltopss 
 |-  ( ( J e. Top /\ o e. J ) -> o C_ X )
30 29 sseld 
 |-  ( ( J e. Top /\ o e. J ) -> ( x e. o -> x e. X ) )
31 30 adantrr 
 |-  ( ( J e. Top /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. o -> x e. X ) )
32 31 3ad2antl1 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. o -> x e. X ) )
33 eldif 
 |-  ( x e. ( X \ Y ) <-> ( x e. X /\ -. x e. Y ) )
34 33 simplbi2 
 |-  ( x e. X -> ( -. x e. Y -> x e. ( X \ Y ) ) )
35 34 orrd 
 |-  ( x e. X -> ( x e. Y \/ x e. ( X \ Y ) ) )
36 32 35 syl6 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. o -> ( x e. Y \/ x e. ( X \ Y ) ) ) )
37 elin 
 |-  ( x e. ( o i^i Y ) <-> ( x e. o /\ x e. Y ) )
38 eleq2 
 |-  ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( x e. ( ( int ` K ) ` S ) <-> x e. ( o i^i Y ) ) )
39 elun1 
 |-  ( x e. ( ( int ` K ) ` S ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) )
40 38 39 syl6bir 
 |-  ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( x e. ( o i^i Y ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
41 40 ad2antll 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. ( o i^i Y ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
42 37 41 syl5bir 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( ( x e. o /\ x e. Y ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
43 42 expdimp 
 |-  ( ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) /\ x e. o ) -> ( x e. Y -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
44 elun2 
 |-  ( x e. ( X \ Y ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) )
45 44 a1i 
 |-  ( ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) /\ x e. o ) -> ( x e. ( X \ Y ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
46 43 45 jaod 
 |-  ( ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) /\ x e. o ) -> ( ( x e. Y \/ x e. ( X \ Y ) ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
47 46 ex 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. o -> ( ( x e. Y \/ x e. ( X \ Y ) ) -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) ) )
48 36 47 mpdd 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( x e. o -> x e. ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) ) )
49 48 ssrdv 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> o C_ ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) )
50 11 adantr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( J |`t Y ) e. Top )
51 2 50 eqeltrid 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> K e. Top )
52 14 adantr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> S C_ U. ( J |`t Y ) )
53 2 unieqi 
 |-  U. K = U. ( J |`t Y )
54 53 eqcomi 
 |-  U. ( J |`t Y ) = U. K
55 54 ntrss2 
 |-  ( ( K e. Top /\ S C_ U. ( J |`t Y ) ) -> ( ( int ` K ) ` S ) C_ S )
56 51 52 55 syl2anc 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( ( int ` K ) ` S ) C_ S )
57 unss1 
 |-  ( ( ( int ` K ) ` S ) C_ S -> ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) C_ ( S u. ( X \ Y ) ) )
58 56 57 syl 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( ( ( int ` K ) ` S ) u. ( X \ Y ) ) C_ ( S u. ( X \ Y ) ) )
59 49 58 sstrd 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> o C_ ( S u. ( X \ Y ) ) )
60 simpl1 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> J e. Top )
61 sstr 
 |-  ( ( S C_ Y /\ Y C_ X ) -> S C_ X )
62 61 ancoms 
 |-  ( ( Y C_ X /\ S C_ Y ) -> S C_ X )
63 62 3adant1 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ X )
64 63 adantr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> S C_ X )
65 difss 
 |-  ( X \ Y ) C_ X
66 unss 
 |-  ( ( S C_ X /\ ( X \ Y ) C_ X ) <-> ( S u. ( X \ Y ) ) C_ X )
67 64 65 66 sylanblc 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> ( S u. ( X \ Y ) ) C_ X )
68 simprl 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> o e. J )
69 simprr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> o C_ ( S u. ( X \ Y ) ) )
70 1 ssntr 
 |-  ( ( ( J e. Top /\ ( S u. ( X \ Y ) ) C_ X ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> o C_ ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) )
71 60 67 68 69 70 syl22anc 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> o C_ ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) )
72 71 ssrind 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> ( o i^i Y ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )
73 sseq1 
 |-  ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) <-> ( o i^i Y ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) ) )
74 72 73 syl5ibrcom 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ o C_ ( S u. ( X \ Y ) ) ) ) -> ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) ) )
75 74 expr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ o e. J ) -> ( o C_ ( S u. ( X \ Y ) ) -> ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) ) ) )
76 75 com23 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ o e. J ) -> ( ( ( int ` K ) ` S ) = ( o i^i Y ) -> ( o C_ ( S u. ( X \ Y ) ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) ) ) )
77 76 impr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( o C_ ( S u. ( X \ Y ) ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) ) )
78 59 77 mpd 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( o e. J /\ ( ( int ` K ) ` S ) = ( o i^i Y ) ) ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )
79 28 78 rexlimddv 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) C_ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )
80 2 11 eqeltrid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> K e. Top )
81 8 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> Y e. _V )
82 63 65 66 sylanblc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( S u. ( X \ Y ) ) C_ X )
83 1 ntropn 
 |-  ( ( J e. Top /\ ( S u. ( X \ Y ) ) C_ X ) -> ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) e. J )
84 19 82 83 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) e. J )
85 elrestr 
 |-  ( ( J e. Top /\ Y e. _V /\ ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) e. J ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) e. ( J |`t Y ) )
86 19 81 84 85 syl3anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) e. ( J |`t Y ) )
87 86 2 eleqtrrdi 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) e. K )
88 1 ntrss2 
 |-  ( ( J e. Top /\ ( S u. ( X \ Y ) ) C_ X ) -> ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) C_ ( S u. ( X \ Y ) ) )
89 19 82 88 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) C_ ( S u. ( X \ Y ) ) )
90 89 ssrind 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) C_ ( ( S u. ( X \ Y ) ) i^i Y ) )
91 elin 
 |-  ( x e. ( ( S u. ( X \ Y ) ) i^i Y ) <-> ( x e. ( S u. ( X \ Y ) ) /\ x e. Y ) )
92 elun 
 |-  ( x e. ( S u. ( X \ Y ) ) <-> ( x e. S \/ x e. ( X \ Y ) ) )
93 orcom 
 |-  ( ( x e. S \/ x e. ( X \ Y ) ) <-> ( x e. ( X \ Y ) \/ x e. S ) )
94 df-or 
 |-  ( ( x e. ( X \ Y ) \/ x e. S ) <-> ( -. x e. ( X \ Y ) -> x e. S ) )
95 93 94 bitri 
 |-  ( ( x e. S \/ x e. ( X \ Y ) ) <-> ( -. x e. ( X \ Y ) -> x e. S ) )
96 92 95 bitri 
 |-  ( x e. ( S u. ( X \ Y ) ) <-> ( -. x e. ( X \ Y ) -> x e. S ) )
97 96 anbi1i 
 |-  ( ( x e. ( S u. ( X \ Y ) ) /\ x e. Y ) <-> ( ( -. x e. ( X \ Y ) -> x e. S ) /\ x e. Y ) )
98 91 97 bitri 
 |-  ( x e. ( ( S u. ( X \ Y ) ) i^i Y ) <-> ( ( -. x e. ( X \ Y ) -> x e. S ) /\ x e. Y ) )
99 elndif 
 |-  ( x e. Y -> -. x e. ( X \ Y ) )
100 pm2.27 
 |-  ( -. x e. ( X \ Y ) -> ( ( -. x e. ( X \ Y ) -> x e. S ) -> x e. S ) )
101 99 100 syl 
 |-  ( x e. Y -> ( ( -. x e. ( X \ Y ) -> x e. S ) -> x e. S ) )
102 101 impcom 
 |-  ( ( ( -. x e. ( X \ Y ) -> x e. S ) /\ x e. Y ) -> x e. S )
103 102 a1i 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( -. x e. ( X \ Y ) -> x e. S ) /\ x e. Y ) -> x e. S ) )
104 98 103 syl5bi 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( S u. ( X \ Y ) ) i^i Y ) -> x e. S ) )
105 104 ssrdv 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( S u. ( X \ Y ) ) i^i Y ) C_ S )
106 90 105 sstrd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) C_ S )
107 54 ssntr 
 |-  ( ( ( K e. Top /\ S C_ U. ( J |`t Y ) ) /\ ( ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) e. K /\ ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) C_ S ) ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) C_ ( ( int ` K ) ` S ) )
108 80 14 87 106 107 syl22anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) C_ ( ( int ` K ) ` S ) )
109 79 108 eqssd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) = ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )