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

Theorem restopnb 19521
 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 1004 . . . . . . 7
2 simpr2 1003 . . . . . . 7
31, 2sstrd 3519 . . . . . 6
4 df-ss 3495 . . . . . 6
53, 4sylib 196 . . . . 5
65eqcomd 2475 . . . 4
7 ineq1 3698 . . . . . . 7
87eqeq2d 2481 . . . . . 6
98rspcev 3219 . . . . 5
109expcom 435 . . . 4
116, 10syl 16 . . 3
12 inass 3713 . . . . . 6
13 simprr 756 . . . . . . . 8
1413ineq1d 3704 . . . . . . 7
15 simplr3 1040 . . . . . . . . 9
16 df-ss 3495 . . . . . . . . 9
1715, 16sylib 196 . . . . . . . 8
1817adantrr 716 . . . . . . 7
1914, 18eqtr3d 2510 . . . . . 6
20 simplr2 1039 . . . . . . . . 9
21 dfss1 3708 . . . . . . . . 9
2220, 21sylib 196 . . . . . . . 8
2322ineq2d 3705 . . . . . . 7
2423adantrr 716 . . . . . 6
2512, 19, 243eqtr3a 2532 . . . . 5
26 simplll 757 . . . . . 6
27 simprl 755 . . . . . 6
28 simplr1 1038 . . . . . 6
29 inopn 19254 . . . . . 6
3026, 27, 28, 29syl3anc 1228 . . . . 5
3125, 30eqeltrd 2555 . . . 4
3231rexlimdvaa 2960 . . 3
3311, 32impbid 191 . 2
34 elrest 14695 . . 3 t