Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  restopnb Unicode version

Theorem restopnb 12541
 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 990 . . . . . . 7
2 simpr2 989 . . . . . . 7
31, 2sstrd 3138 . . . . . 6
4 df-ss 3115 . . . . . 6
53, 4sylib 121 . . . . 5
65eqcomd 2163 . . . 4
7 ineq1 3301 . . . . . 6
87rspceeqv 2834 . . . . 5
98expcom 115 . . . 4
106, 9syl 14 . . 3
11 inass 3317 . . . . . 6
12 simprr 522 . . . . . . . 8
1312ineq1d 3307 . . . . . . 7
14 simplr3 1026 . . . . . . . . 9
15 df-ss 3115 . . . . . . . . 9
1614, 15sylib 121 . . . . . . . 8
1716adantrr 471 . . . . . . 7
1813, 17eqtr3d 2192 . . . . . 6
19 simplr2 1025 . . . . . . . . 9
20 sseqin2 3326 . . . . . . . . 9
2119, 20sylib 121 . . . . . . . 8
2221ineq2d 3308 . . . . . . 7
2322adantrr 471 . . . . . 6
2411, 18, 233eqtr3a 2214 . . . . 5
25 simplll 523 . . . . . 6
26 simprl 521 . . . . . 6
27 simplr1 1024 . . . . . 6
28 inopn 12361 . . . . . 6
2925, 26, 27, 28syl3anc 1220 . . . . 5
3024, 29eqeltrd 2234 . . . 4
3130rexlimdvaa 2575 . . 3
3210, 31impbid 128 . 2
33 elrest 12318 . . 3 t