Description: A subspace of a T_1 topology is T_1. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | restt1 | |- ( ( J e. Fre /\ A e. V ) -> ( J |`t A ) e. Fre ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | t1top | |- ( J e. Fre -> J e. Top ) |
|
2 | cnt1 | |- ( ( J e. Fre /\ ( _I |` ( A i^i U. J ) ) : ( A i^i U. J ) -1-1-> ( A i^i U. J ) /\ ( _I |` ( A i^i U. J ) ) e. ( ( J |`t A ) Cn J ) ) -> ( J |`t A ) e. Fre ) |
|
3 | 1 2 | resthauslem | |- ( ( J e. Fre /\ A e. V ) -> ( J |`t A ) e. Fre ) |