Description: The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mopnval.1 | |- J = ( MetOpen ` D ) |
|
| Assertion | mopnfss | |- ( D e. ( *Met ` X ) -> J C_ ~P X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mopnval.1 | |- J = ( MetOpen ` D ) |
|
| 2 | pwuni | |- J C_ ~P U. J |
|
| 3 | 1 | mopnuni | |- ( D e. ( *Met ` X ) -> X = U. J ) |
| 4 | 3 | pweqd | |- ( D e. ( *Met ` X ) -> ~P X = ~P U. J ) |
| 5 | 2 4 | sseqtrrid | |- ( D e. ( *Met ` X ) -> J C_ ~P X ) |