Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  restopnb Unicode version

Theorem restopnb 16922
 Description: If is an open subset of the subspace base set , then any subset of is open iff it is open in . (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
restopnb t

Proof of Theorem restopnb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr3 963 . . . . . . 7
2 simpr2 962 . . . . . . 7
31, 2sstrd 3202 . . . . . 6
4 df-ss 3179 . . . . . 6
53, 4sylib 188 . . . . 5
65eqcomd 2301 . . . 4
7 ineq1 3376 . . . . . . 7
87eqeq2d 2307 . . . . . 6
98rspcev 2897 . . . . 5
109expcom 424 . . . 4
116, 10syl 15 . . 3
12 inass 3392 . . . . . . 7
13 simprr 733 . . . . . . . . 9
1413ineq1d 3382 . . . . . . . 8
15 simplr3 999 . . . . . . . . . 10
16 df-ss 3179 . . . . . . . . . 10
1715, 16sylib 188 . . . . . . . . 9
1817adantrr 697 . . . . . . . 8
1914, 18eqtr3d 2330 . . . . . . 7
20 simplr2 998 . . . . . . . . . 10
21 dfss1 3386 . . . . . . . . . 10
2220, 21sylib 188 . . . . . . . . 9
2322ineq2d 3383 . . . . . . . 8
2423adantrr 697 . . . . . . 7
2512, 19, 243eqtr3a 2352 . . . . . 6
26 simplll 734 . . . . . . 7
27 simprl 732 . . . . . . 7
28 simplr1 997 . . . . . . 7
29 inopn 16661 . . . . . . 7
3026, 27, 28, 29syl3anc 1182 . . . . . 6
3125, 30eqeltrd 2370 . . . . 5
3231expr 598 . . . 4
3332rexlimdva 2680 . . 3
3411, 33impbid 183 . 2
35 elrest 13348 . . 3 t